Theorem hashf1lem1 11285

Description: Lemma for hashf1 11287. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.)

Hypotheses

Ref	Expression
hashf1lem2.1	|- ( ph -> A e. Fin )
hashf1lem2.2	|- ( ph -> B e. Fin )
hashf1lem2.3	|- ( ph -> -. z e. A )
hashf1lem2.4	|- ( ph -> ( (♯ ` A ) + 1 ) <_ (♯ ` B ) )
hashf1lem1.5	|- ( ph -> F : A -1-1-> B )

Assertion

Ref	Expression
hashf1lem1	|- ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } ~~ ( B \ ran F ) )

Distinct variable groups:   z, f   A, f   B, f   ph, f   f, F

Allowed substitution hints:   ph( z)   A( z)   B( z)   F( z)

Proof of Theorem hashf1lem1

Dummy variables g x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		hashf1lem2.1	. . . . 5 |- ( ph -> A e. Fin )
2		vex 2824	. . . . . 6 |- z e. _V
3	2	a1i 9	. . . . 5 |- ( ph -> z e. _V )
4		hashf1lem2.3	. . . . 5 |- ( ph -> -. z e. A )
5		unsnfi 7226	. . . . 5 |- ( ( A e. Fin /\ z e. _V /\ -. z e. A ) -> ( A u. { z } ) e. Fin )
6	1, 3, 4, 5	syl3anc 1278	. . . 4 |- ( ph -> ( A u. { z } ) e. Fin )
7		hashf1lem2.2	. . . 4 |- ( ph -> B e. Fin )
8		f1setexg 6951	. . . 4 |- ( ( ( A u. { z } ) e. Fin /\ B e. Fin ) -> { f | f : ( A u. { z } ) -1-1-> B } e. _V )
9	6, 7, 8	syl2anc 415	. . 3 |- ( ph -> { f | f : ( A u. { z } ) -1-1-> B } e. _V )
10		abanssr 3502	. . . 4 |- { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } C_ { f | f : ( A u. { z } ) -1-1-> B }
11	10	a1i 9	. . 3 |- ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } C_ { f | f : ( A u. { z } ) -1-1-> B } )
12	9, 11	ssexd 4273	. 2 |- ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } e. _V )
13	7	difexd 4277	. 2 |- ( ph -> ( B \ ran F ) e. _V )
14		vex 2824	. . . 4 |- g e. _V
15		reseq1 5057	. . . . . 6 |- ( f = g -> ( f |` A ) = ( g |` A ) )
16	15	eqeq1d 2247	. . . . 5 |- ( f = g -> ( ( f |` A ) = F <-> ( g |` A ) = F ) )
17		f1eq1 5593	. . . . 5 |- ( f = g -> ( f : ( A u. { z } ) -1-1-> B <-> g : ( A u. { z } ) -1-1-> B ) )
18	16, 17	anbi12d 477	. . . 4 |- ( f = g -> ( ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) )
19	14, 18	elab 2970	. . 3 |- ( g e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } <-> ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) )
20		f1f 5598	. . . . . . 7 |- ( g : ( A u. { z } ) -1-1-> B -> g : ( A u. { z } ) --> B )
21	20	ad2antll 495	. . . . . 6 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> g : ( A u. { z } ) --> B )
22		ssun2 3393	. . . . . . 7 |- { z } C_ ( A u. { z } )
23	2	snss 3850	. . . . . . 7 |- ( z e. ( A u. { z } ) <-> { z } C_ ( A u. { z } ) )
24	22, 23	mpbir 146	. . . . . 6 |- z e. ( A u. { z } )
25		ffvelcdm 5841	. . . . . 6 |- ( ( g : ( A u. { z } ) --> B /\ z e. ( A u. { z } ) ) -> ( g ` z ) e. B )
26	21, 24, 25	sylancl 417	. . . . 5 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( g ` z ) e. B )
27	4	adantr 276	. . . . . 6 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> -. z e. A )
28		df-ima 4787	. . . . . . . . 9 |- ( g " A ) = ran ( g |` A )
29		simprl 535	. . . . . . . . . 10 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( g |` A ) = F )
30	29	rneqd 5011	. . . . . . . . 9 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ran ( g |` A ) = ran F )
31	28, 30	eqtrid 2283	. . . . . . . 8 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( g " A ) = ran F )
32	31	eleq2d 2308	. . . . . . 7 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( ( g ` z ) e. ( g " A ) <-> ( g ` z ) e. ran F ) )
33		simprr 537	. . . . . . . 8 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> g : ( A u. { z } ) -1-1-> B )
34	24	a1i 9	. . . . . . . 8 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> z e. ( A u. { z } ) )
35		ssun1 3392	. . . . . . . . 9 |- A C_ ( A u. { z } )
36	35	a1i 9	. . . . . . . 8 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> A C_ ( A u. { z } ) )
37		f1elima 5979	. . . . . . . 8 |- ( ( g : ( A u. { z } ) -1-1-> B /\ z e. ( A u. { z } ) /\ A C_ ( A u. { z } ) ) -> ( ( g ` z ) e. ( g " A ) <-> z e. A ) )
38	33, 34, 36, 37	syl3anc 1278	. . . . . . 7 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( ( g ` z ) e. ( g " A ) <-> z e. A ) )
39	32, 38	bitr3d 190	. . . . . 6 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( ( g ` z ) e. ran F <-> z e. A ) )
40	27, 39	mtbird 684	. . . . 5 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> -. ( g ` z ) e. ran F )
41	26, 40	eldifd 3230	. . . 4 |- ( ( ph /\ ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) ) -> ( g ` z ) e. ( B \ ran F ) )
42	41	ex 115	. . 3 |- ( ph -> ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) -> ( g ` z ) e. ( B \ ran F ) ) )
43	19, 42	biimtrid 152	. 2 |- ( ph -> ( g e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } -> ( g ` z ) e. ( B \ ran F ) ) )
44		hashf1lem1.5	. . . . . . 7 |- ( ph -> F : A -1-1-> B )
45		f1f 5598	. . . . . . 7 |- ( F : A -1-1-> B -> F : A --> B )
46	44, 45	syl 14	. . . . . 6 |- ( ph -> F : A --> B )
47	46	adantr 276	. . . . 5 |- ( ( ph /\ x e. ( B \ ran F ) ) -> F : A --> B )
48		vex 2824	. . . . . . . 8 |- x e. _V
49	2, 48	f1osn 5681	. . . . . . 7 |- { <. z , x >. } : { z } -1-1-onto-> { x }
50		f1of 5639	. . . . . . 7 |- ( { <. z , x >. } : { z } -1-1-onto-> { x } -> { <. z , x >. } : { z } --> { x } )
51	49, 50	ax-mp 5	. . . . . 6 |- { <. z , x >. } : { z } --> { x }
52		eldifi 3351	. . . . . . . 8 |- ( x e. ( B \ ran F ) -> x e. B )
53	52	adantl 277	. . . . . . 7 |- ( ( ph /\ x e. ( B \ ran F ) ) -> x e. B )
54	53	snssd 3860	. . . . . 6 |- ( ( ph /\ x e. ( B \ ran F ) ) -> { x } C_ B )
55		fss 5546	. . . . . 6 |- ( ( { <. z , x >. } : { z } --> { x } /\ { x } C_ B ) -> { <. z , x >. } : { z } --> B )
56	51, 54, 55	sylancr 418	. . . . 5 |- ( ( ph /\ x e. ( B \ ran F ) ) -> { <. z , x >. } : { z } --> B )
57		disjsn 3771	. . . . . . 7 |- ( ( A i^i { z } ) = (/) <-> -. z e. A )
58	4, 57	sylibr 134	. . . . . 6 |- ( ph -> ( A i^i { z } ) = (/) )
59	58	adantr 276	. . . . 5 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( A i^i { z } ) = (/) )
60		fresaunres1disj 5571	. . . . 5 |- ( ( F : A --> B /\ { <. z , x >. } : { z } --> B /\ ( A i^i { z } ) = (/) ) -> ( ( F u. { <. z , x >. } ) |` A ) = F )
61	47, 56, 59, 60	syl3anc 1278	. . . 4 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( ( F u. { <. z , x >. } ) |` A ) = F )
62		f1f1orn 5650	. . . . . . . . 9 |- ( F : A -1-1-> B -> F : A -1-1-onto-> ran F )
63	44, 62	syl 14	. . . . . . . 8 |- ( ph -> F : A -1-1-onto-> ran F )
64	63	adantr 276	. . . . . . 7 |- ( ( ph /\ x e. ( B \ ran F ) ) -> F : A -1-1-onto-> ran F )
65	49	a1i 9	. . . . . . 7 |- ( ( ph /\ x e. ( B \ ran F ) ) -> { <. z , x >. } : { z } -1-1-onto-> { x } )
66		eldifn 3352	. . . . . . . . 9 |- ( x e. ( B \ ran F ) -> -. x e. ran F )
67	66	adantl 277	. . . . . . . 8 |- ( ( ph /\ x e. ( B \ ran F ) ) -> -. x e. ran F )
68		disjsn 3771	. . . . . . . 8 |- ( ( ran F i^i { x } ) = (/) <-> -. x e. ran F )
69	67, 68	sylibr 134	. . . . . . 7 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( ran F i^i { x } ) = (/) )
70		f1oun 5659	. . . . . . 7 |- ( ( ( F : A -1-1-onto-> ran F /\ { <. z , x >. } : { z } -1-1-onto-> { x } ) /\ ( ( A i^i { z } ) = (/) /\ ( ran F i^i { x } ) = (/) ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) )
71	64, 65, 59, 69, 70	syl22anc 1279	. . . . . 6 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) )
72		f1of1 5638	. . . . . 6 |- ( ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> ( ran F u. { x } ) )
73	71, 72	syl 14	. . . . 5 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> ( ran F u. { x } ) )
74	47	frnd 5543	. . . . . 6 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ran F C_ B )
75	74, 54	unssd 3405	. . . . 5 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( ran F u. { x } ) C_ B )
76		f1ss 5604	. . . . 5 |- ( ( ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> ( ran F u. { x } ) /\ ( ran F u. { x } ) C_ B ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B )
77	73, 75, 76	syl2anc 415	. . . 4 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B )
78	46, 1	fexd 5948	. . . . . . 7 |- ( ph -> F e. _V )
79	78	adantr 276	. . . . . 6 |- ( ( ph /\ x e. ( B \ ran F ) ) -> F e. _V )
80	2, 48	opex 4369	. . . . . . 7 |- <. z , x >. e. _V
81	80	snex 4322	. . . . . 6 |- { <. z , x >. } e. _V
82		unexg 4589	. . . . . 6 |- ( ( F e. _V /\ { <. z , x >. } e. _V ) -> ( F u. { <. z , x >. } ) e. _V )
83	79, 81, 82	sylancl 417	. . . . 5 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) e. _V )
84		reseq1 5057	. . . . . . . 8 |- ( f = ( F u. { <. z , x >. } ) -> ( f |` A ) = ( ( F u. { <. z , x >. } ) |` A ) )
85	84	eqeq1d 2247	. . . . . . 7 |- ( f = ( F u. { <. z , x >. } ) -> ( ( f |` A ) = F <-> ( ( F u. { <. z , x >. } ) |` A ) = F ) )
86		f1eq1 5593	. . . . . . 7 |- ( f = ( F u. { <. z , x >. } ) -> ( f : ( A u. { z } ) -1-1-> B <-> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B ) )
87	85, 86	anbi12d 477	. . . . . 6 |- ( f = ( F u. { <. z , x >. } ) -> ( ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) <-> ( ( ( F u. { <. z , x >. } ) |` A ) = F /\ ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B ) ) )
88	87	elabg 2972	. . . . 5 |- ( ( F u. { <. z , x >. } ) e. _V -> ( ( F u. { <. z , x >. } ) e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } <-> ( ( ( F u. { <. z , x >. } ) |` A ) = F /\ ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B ) ) )
89	83, 88	syl 14	. . . 4 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( ( F u. { <. z , x >. } ) e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } <-> ( ( ( F u. { <. z , x >. } ) |` A ) = F /\ ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-> B ) ) )
90	61, 77, 89	mpbir2and 957	. . 3 |- ( ( ph /\ x e. ( B \ ran F ) ) -> ( F u. { <. z , x >. } ) e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } )
91	90	ex 115	. 2 |- ( ph -> ( x e. ( B \ ran F ) -> ( F u. { <. z , x >. } ) e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } ) )
92	19	anbi1i 462	. . 3 |- ( ( g e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } /\ x e. ( B \ ran F ) ) <-> ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) )
93		simprlr 544	. . . . . . 7 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> g : ( A u. { z } ) -1-1-> B )
94		f1fn 5600	. . . . . . 7 |- ( g : ( A u. { z } ) -1-1-> B -> g Fn ( A u. { z } ) )
95	93, 94	syl 14	. . . . . 6 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> g Fn ( A u. { z } ) )
96	71	adantrl 482	. . . . . . 7 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) )
97		f1ofn 5640	. . . . . . 7 |- ( ( F u. { <. z , x >. } ) : ( A u. { z } ) -1-1-onto-> ( ran F u. { x } ) -> ( F u. { <. z , x >. } ) Fn ( A u. { z } ) )
98	96, 97	syl 14	. . . . . 6 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( F u. { <. z , x >. } ) Fn ( A u. { z } ) )
99		eqfnfv 5806	. . . . . 6 |- ( ( g Fn ( A u. { z } ) /\ ( F u. { <. z , x >. } ) Fn ( A u. { z } ) ) -> ( g = ( F u. { <. z , x >. } ) <-> A. y e. ( A u. { z } ) ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) )
100	95, 98, 99	syl2anc 415	. . . . 5 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( g = ( F u. { <. z , x >. } ) <-> A. y e. ( A u. { z } ) ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) )
101		fvres 5719	. . . . . . . . . . 11 |- ( y e. A -> ( ( g |` A ) ` y ) = ( g ` y ) )
102	101	eqcomd 2244	. . . . . . . . . 10 |- ( y e. A -> ( g ` y ) = ( ( g |` A ) ` y ) )
103		simprll 543	. . . . . . . . . . 11 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( g |` A ) = F )
104	103	fveq1d 5697	. . . . . . . . . 10 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( ( g |` A ) ` y ) = ( F ` y ) )
105	102, 104	sylan9eqr 2293	. . . . . . . . 9 |- ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> ( g ` y ) = ( F ` y ) )
106	44	ad2antrr 492	. . . . . . . . . . 11 |- ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> F : A -1-1-> B )
107		f1fn 5600	. . . . . . . . . . 11 |- ( F : A -1-1-> B -> F Fn A )
108	106, 107	syl 14	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> F Fn A )
109	2, 48	fnsn 5435	. . . . . . . . . . 11 |- { <. z , x >. } Fn { z }
110	109	a1i 9	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> { <. z , x >. } Fn { z } )
111	58	ad2antrr 492	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> ( A i^i { z } ) = (/) )
112		simpr 110	. . . . . . . . . 10 |- ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> y e. A )
113	108, 110, 111, 112	fvun1d 5771	. . . . . . . . 9 |- ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> ( ( F u. { <. z , x >. } ) ` y ) = ( F ` y ) )
114	105, 113	eqtr4d 2274	. . . . . . . 8 |- ( ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) /\ y e. A ) -> ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) )
115	114	ralrimiva 2623	. . . . . . 7 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> A. y e. A ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) )
116	115	biantrurd 305	. . . . . 6 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> ( A. y e. A ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) /\ A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) ) )
117		ralunb 3410	. . . . . 6 |- ( A. y e. ( A u. { z } ) ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> ( A. y e. A ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) /\ A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) )
118	116, 117	bitr4di 198	. . . . 5 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> A. y e. ( A u. { z } ) ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) ) )
119	46	fdmd 5540	. . . . . . . . . . 11 |- ( ph -> dom F = A )
120	119	eleq2d 2308	. . . . . . . . . 10 |- ( ph -> ( z e. dom F <-> z e. A ) )
121	4, 120	mtbird 684	. . . . . . . . 9 |- ( ph -> -. z e. dom F )
122	121	adantr 276	. . . . . . . 8 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> -. z e. dom F )
123		fsnunfv 5916	. . . . . . . 8 |- ( ( z e. _V /\ x e. _V /\ -. z e. dom F ) -> ( ( F u. { <. z , x >. } ) ` z ) = x )
124	2, 48, 122, 123	mp3an12i 1382	. . . . . . 7 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( ( F u. { <. z , x >. } ) ` z ) = x )
125	124	eqeq2d 2250	. . . . . 6 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( ( g ` z ) = ( ( F u. { <. z , x >. } ) ` z ) <-> ( g ` z ) = x ) )
126		fveq2 5695	. . . . . . . 8 |- ( y = z -> ( g ` y ) = ( g ` z ) )
127		fveq2 5695	. . . . . . . 8 |- ( y = z -> ( ( F u. { <. z , x >. } ) ` y ) = ( ( F u. { <. z , x >. } ) ` z ) )
128	126, 127	eqeq12d 2253	. . . . . . 7 |- ( y = z -> ( ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> ( g ` z ) = ( ( F u. { <. z , x >. } ) ` z ) ) )
129	2, 128	ralsn 3752	. . . . . 6 |- ( A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> ( g ` z ) = ( ( F u. { <. z , x >. } ) ` z ) )
130		eqcom 2240	. . . . . 6 |- ( x = ( g ` z ) <-> ( g ` z ) = x )
131	125, 129, 130	3bitr4g 223	. . . . 5 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( A. y e. { z } ( g ` y ) = ( ( F u. { <. z , x >. } ) ` y ) <-> x = ( g ` z ) ) )
132	100, 118, 131	3bitr2d 216	. . . 4 |- ( ( ph /\ ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) ) -> ( g = ( F u. { <. z , x >. } ) <-> x = ( g ` z ) ) )
133	132	ex 115	. . 3 |- ( ph -> ( ( ( ( g |` A ) = F /\ g : ( A u. { z } ) -1-1-> B ) /\ x e. ( B \ ran F ) ) -> ( g = ( F u. { <. z , x >. } ) <-> x = ( g ` z ) ) ) )
134	92, 133	biimtrid 152	. 2 |- ( ph -> ( ( g e. { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } /\ x e. ( B \ ran F ) ) -> ( g = ( F u. { <. z , x >. } ) <-> x = ( g ` z ) ) ) )
135	12, 13, 43, 91, 134	en3d 7055	1 |- ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } ~~ ( B \ ran F ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   e. wcel 2209   {cab 2224   A.wral 2528   _Vcvv 2821   \ cdif 3217   u. cun 3218   i^i cin 3219   C_ wss 3220   (/)c0 3520   {csn 3709   <.cop 3712   class class class wbr 4130   dom cdm 4774   ran crn 4775   |` cres 4776   "cima 4777   Fn wfn 5372   -->wf 5373   -1-1->wf1 5374   -1-1-onto->wf1o 5376   ` cfv 5377  (class class class)co 6085   ~~ cen 7020   Fincfn 7022   1c1 8180   + caddc 8182   <_ cle 8361  ♯chash 11214

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-iord 4511  df-on 4513  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-1o 6687  df-er 6807  df-en 7023  df-fin 7025

This theorem is used by:  hashf1lem2  11286