Theorem hashf1lem1 11263

Description: Lemma for hashf1 11265. (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 7216	. . . . 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 6941	. . . 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 4268	. 2 |- ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } e. _V )
13	7	difexd 4272	. 2 |- ( ph -> ( B \ ran F ) e. _V )
14		vex 2824	. . . 4 |- g e. _V
15		reseq1 5052	. . . . . 6 |- ( f = g -> ( f |` A ) = ( g |` A ) )
16	15	eqeq1d 2247	. . . . 5 |- ( f = g -> ( ( f |` A ) = F <-> ( g |` A ) = F ) )
17		f1eq1 5588	. . . . 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 5593	. . . . . . 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 3845	. . . . . . 7 |- ( z e. ( A u. { z } ) <-> { z } C_ ( A u. { z } ) )
24	22, 23	mpbir 146	. . . . . 6 |- z e. ( A u. { z } )
25		ffvelcdm 5832	. . . . . 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 4782	. . . . . . . . 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 5006	. . . . . . . . 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 5969	. . . . . . . 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 5593	. . . . . . 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 5676	. . . . . . 7 |- { <. z , x >. } : { z } -1-1-onto-> { x }
50		f1of 5634	. . . . . . 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 3855	. . . . . 6 |- ( ( ph /\ x e. ( B \ ran F ) ) -> { x } C_ B )
55		fss 5541	. . . . . 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 3767	. . . . . . 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 5566	. . . . 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 5645	. . . . . . . . 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 3767	. . . . . . . 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 5654	. . . . . . 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 5633	. . . . . 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 5538	. . . . . 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 5599	. . . . 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 5938	. . . . . . 7 |- ( ph -> F e. _V )
79	78	adantr 276	. . . . . 6 |- ( ( ph /\ x e. ( B \ ran F ) ) -> F e. _V )
80	2, 48	opex 4364	. . . . . . 7 |- <. z , x >. e. _V
81	80	snex 4317	. . . . . 6 |- { <. z , x >. } e. _V
82		unexg 4584	. . . . . 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 5052	. . . . . . . 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 5588	. . . . . . 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 5595	. . . . . . 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 5635	. . . . . . 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 5797	. . . . . 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 5714	. . . . . . . . . . 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 5692	. . . . . . . . . 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 5595	. . . . . . . . . . 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 5430	. . . . . . . . . . 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 5765	. . . . . . . . 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 5535	. . . . . . . . . . 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 5907	. . . . . . . 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 5690	. . . . . . . 8 |- ( y = z -> ( g ` y ) = ( g ` z ) )
127		fveq2 5690	. . . . . . . 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 3748	. . . . . 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 7045	1 |- ( ph -> { f | ( ( f |` A ) = F /\ f : ( A u. { z } ) -1-1-> B ) } ~~ ( B \ ran F ) )

Syntax hints:   -. 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 3705   <.cop 3708   class class class wbr 4125   dom cdm 4769   ran crn 4770   |` cres 4771   "cima 4772   Fn wfn 5367   -->wf 5368   -1-1->wf1 5369   -1-1-onto->wf1o 5371   ` cfv 5372  (class class class)co 6075   ~~ cen 7010   Fincfn 7012   1c1 8170   + caddc 8172   <_ cle 8351  ♯chash 11192

This theorem was proved from 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 4241  ax-sep 4244  ax-nul 4254  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679  ax-iinf 4730

This theorem 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 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-int 3966  df-iun 4009  df-br 4126  df-opab 4188  df-mpt 4189  df-tr 4225  df-id 4433  df-iord 4506  df-on 4508  df-suc 4511  df-iom 4733  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-ima 4782  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379  df-fv 5380  df-1o 6677  df-er 6797  df-en 7013  df-fin 7015

This theorem is referenced by:  hashf1lem2  11264