Theorem appelima ≪ | index | src | ≫

theorem appelima (A F: set) (G: wff) (a: nat):
  $ G -> isfun F $ >
  $ G -> a e. Dom F $ >
  $ G -> a e. A $ >
  $ G -> F @ a e. F '' A $;

Step	Hyp	Ref	Expression
1		eleq2	Ran (F \|` A) == F '' A -> (F @ a e. Ran (F \|` A) <-> F @ a e. F '' A)
2		rnres	Ran (F \|` A) == F '' A
3	1, 2	ax_mp	F @ a e. Ran (F \|` A) <-> F @ a e. F '' A
4		resapp	a e. A -> (F \|` A) @ a = F @ a
5		hyp h3	G -> a e. A
6	4, 5	syl	G -> (F \|` A) @ a = F @ a
7	6	eleq1d	G -> ((F \|` A) @ a e. Ran (F \|` A) <-> F @ a e. Ran (F \|` A))
8		appelrn	isfun (F \|` A) -> a e. Dom (F \|` A) -> (F \|` A) @ a e. Ran (F \|` A)
9		resisf	isfun F -> isfun (F \|` A)
10		hyp h1	G -> isfun F
11	9, 10	syl	G -> isfun (F \|` A)
12		eleq2	Dom (F \|` A) == Dom F i^i A -> (a e. Dom (F \|` A) <-> a e. Dom F i^i A)
13		dmres	Dom (F \|` A) == Dom F i^i A
14	12, 13	ax_mp	a e. Dom (F \|` A) <-> a e. Dom F i^i A
15		elin	a e. Dom F i^i A <-> a e. Dom F /\ a e. A
16		hyp h2	G -> a e. Dom F
17	16, 5	iand	G -> a e. Dom F /\ a e. A
18	15, 17	sylibr	G -> a e. Dom F i^i A
19	14, 18	sylibr	G -> a e. Dom (F \|` A)
20	8, 11, 19	sylc	G -> (F \|` A) @ a e. Ran (F \|` A)
21	7, 20	mpbid	G -> F @ a e. Ran (F \|` A)
22	3, 21	sylib	G -> F @ a e. F '' A

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)