Theorem fnwe2lem2 37621

Description: Lemma for fnwe2 37623. An element which is in a minimal fiber and minimal within its fiber is minimal globally; thus T is well-founded. (Contributed by Stefan O'Rear, 19-Jan-2015.)

Hypotheses

Ref	Expression
fnwe2.su	|- ( z = ( F ` x ) -> S = U )
fnwe2.t	|- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
fnwe2.s	|- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
fnwe2.f	|- ( ph -> ( F |` A ) : A --> B )
fnwe2.r	|- ( ph -> R We B )
fnwe2lem2.a	|- ( ph -> a C_ A )
fnwe2lem2.n0	|- ( ph -> a =/= (/) )

Assertion

Ref	Expression
fnwe2lem2	|- ( ph -> E. b e. a A. c e. a -. c T b )

Distinct variable groups:   y, U, z, a, b, c   x, S, y, a, b, c   x, R, y, a, b, c   ph, x, y, z, c   x, A, y, z, a, b, c   x, F, y, z, a, b, c   T, a, b, c   B, a, b, c   ph, b

Allowed substitution hints:   ph( a)   B( x, y, z)   R( z)   S( z)   T( x, y, z)   U( x)

Proof of Theorem fnwe2lem2

Dummy variables d e f g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnwe2.f	. . . 4 |- ( ph -> ( F |` A ) : A --> B )
2		ffun 6048	. . . 4 |- ( ( F |` A ) : A --> B -> Fun ( F |` A ) )
3		vex 3203	. . . . 5 |- a e. _V
4	3	funimaex 5976	. . . 4 |- ( Fun ( F |` A ) -> ( ( F |` A ) " a ) e. _V )
5	1, 2, 4	3syl 18	. . 3 |- ( ph -> ( ( F |` A ) " a ) e. _V )
6		fnwe2.r	. . . 4 |- ( ph -> R We B )
7		wefr 5104	. . . 4 |- ( R We B -> R Fr B )
8	6, 7	syl 17	. . 3 |- ( ph -> R Fr B )
9		imassrn 5477	. . . 4 |- ( ( F |` A ) " a ) C_ ran ( F |` A )
10		frn 6053	. . . . 5 |- ( ( F |` A ) : A --> B -> ran ( F |` A ) C_ B )
11	1, 10	syl 17	. . . 4 |- ( ph -> ran ( F |` A ) C_ B )
12	9, 11	syl5ss 3614	. . 3 |- ( ph -> ( ( F |` A ) " a ) C_ B )
13		incom 3805	. . . . . 6 |- ( dom ( F |` A ) i^i a ) = ( a i^i dom ( F |` A ) )
14		fnwe2lem2.a	. . . . . . . 8 |- ( ph -> a C_ A )
15		fdm 6051	. . . . . . . . 9 |- ( ( F |` A ) : A --> B -> dom ( F |` A ) = A )
16	1, 15	syl 17	. . . . . . . 8 |- ( ph -> dom ( F |` A ) = A )
17	14, 16	sseqtr4d 3642	. . . . . . 7 |- ( ph -> a C_ dom ( F |` A ) )
18		df-ss 3588	. . . . . . 7 |- ( a C_ dom ( F |` A ) <-> ( a i^i dom ( F |` A ) ) = a )
19	17, 18	sylib 208	. . . . . 6 |- ( ph -> ( a i^i dom ( F |` A ) ) = a )
20	13, 19	syl5eq 2668	. . . . 5 |- ( ph -> ( dom ( F |` A ) i^i a ) = a )
21		fnwe2lem2.n0	. . . . 5 |- ( ph -> a =/= (/) )
22	20, 21	eqnetrd 2861	. . . 4 |- ( ph -> ( dom ( F |` A ) i^i a ) =/= (/) )
23		imadisj 5484	. . . . 5 |- ( ( ( F |` A ) " a ) = (/) <-> ( dom ( F |` A ) i^i a ) = (/) )
24	23	necon3bii 2846	. . . 4 |- ( ( ( F |` A ) " a ) =/= (/) <-> ( dom ( F |` A ) i^i a ) =/= (/) )
25	22, 24	sylibr 224	. . 3 |- ( ph -> ( ( F |` A ) " a ) =/= (/) )
26		fri 5076	. . 3 |- ( ( ( ( ( F |` A ) " a ) e. _V /\ R Fr B ) /\ ( ( ( F |` A ) " a ) C_ B /\ ( ( F |` A ) " a ) =/= (/) ) ) -> E. d e. ( ( F |` A ) " a ) A. e e. ( ( F |` A ) " a ) -. e R d )
27	5, 8, 12, 25, 26	syl22anc 1327	. 2 |- ( ph -> E. d e. ( ( F |` A ) " a ) A. e e. ( ( F |` A ) " a ) -. e R d )
28		df-ima 5127	. . . . . 6 |- ( ( F |` A ) " a ) = ran ( ( F |` A ) |` a )
29	28	rexeqi 3143	. . . . 5 |- ( E. d e. ( ( F |` A ) " a ) A. e e. ( ( F |` A ) " a ) -. e R d <-> E. d e. ran ( ( F |` A ) |` a ) A. e e. ( ( F |` A ) " a ) -. e R d )
30		ffn 6045	. . . . . . . 8 |- ( ( F |` A ) : A --> B -> ( F |` A ) Fn A )
31	1, 30	syl 17	. . . . . . 7 |- ( ph -> ( F |` A ) Fn A )
32		fnssres 6004	. . . . . . 7 |- ( ( ( F |` A ) Fn A /\ a C_ A ) -> ( ( F |` A ) |` a ) Fn a )
33	31, 14, 32	syl2anc 693	. . . . . 6 |- ( ph -> ( ( F |` A ) |` a ) Fn a )
34		breq2 4657	. . . . . . . . 9 |- ( d = ( ( ( F |` A ) |` a ) ` f ) -> ( e R d <-> e R ( ( ( F |` A ) |` a ) ` f ) ) )
35	34	notbid 308	. . . . . . . 8 |- ( d = ( ( ( F |` A ) |` a ) ` f ) -> ( -. e R d <-> -. e R ( ( ( F |` A ) |` a ) ` f ) ) )
36	35	ralbidv 2986	. . . . . . 7 |- ( d = ( ( ( F |` A ) |` a ) ` f ) -> ( A. e e. ( ( F |` A ) " a ) -. e R d <-> A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) ) )
37	36	rexrn 6361	. . . . . 6 |- ( ( ( F |` A ) |` a ) Fn a -> ( E. d e. ran ( ( F |` A ) |` a ) A. e e. ( ( F |` A ) " a ) -. e R d <-> E. f e. a A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) ) )
38	33, 37	syl 17	. . . . 5 |- ( ph -> ( E. d e. ran ( ( F |` A ) |` a ) A. e e. ( ( F |` A ) " a ) -. e R d <-> E. f e. a A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) ) )
39	29, 38	syl5bb 272	. . . 4 |- ( ph -> ( E. d e. ( ( F |` A ) " a ) A. e e. ( ( F |` A ) " a ) -. e R d <-> E. f e. a A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) ) )
40	28	raleqi 3142	. . . . . . . 8 |- ( A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) <-> A. e e. ran ( ( F |` A ) |` a ) -. e R ( ( ( F |` A ) |` a ) ` f ) )
41		breq1 4656	. . . . . . . . . . 11 |- ( e = ( ( ( F |` A ) |` a ) ` d ) -> ( e R ( ( ( F |` A ) |` a ) ` f ) <-> ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
42	41	notbid 308	. . . . . . . . . 10 |- ( e = ( ( ( F |` A ) |` a ) ` d ) -> ( -. e R ( ( ( F |` A ) |` a ) ` f ) <-> -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
43	42	ralrn 6362	. . . . . . . . 9 |- ( ( ( F |` A ) |` a ) Fn a -> ( A. e e. ran ( ( F |` A ) |` a ) -. e R ( ( ( F |` A ) |` a ) ` f ) <-> A. d e. a -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
44	33, 43	syl 17	. . . . . . . 8 |- ( ph -> ( A. e e. ran ( ( F |` A ) |` a ) -. e R ( ( ( F |` A ) |` a ) ` f ) <-> A. d e. a -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
45	40, 44	syl5bb 272	. . . . . . 7 |- ( ph -> ( A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) <-> A. d e. a -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
46	45	adantr 481	. . . . . 6 |- ( ( ph /\ f e. a ) -> ( A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) <-> A. d e. a -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
47	14	resabs1d 5428	. . . . . . . . . . . 12 |- ( ph -> ( ( F |` A ) |` a ) = ( F |` a ) )
48	47	ad2antrr 762	. . . . . . . . . . 11 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` A ) |` a ) = ( F |` a ) )
49	48	fveq1d 6193	. . . . . . . . . 10 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` d ) = ( ( F |` a ) ` d ) )
50		fvres 6207	. . . . . . . . . . 11 |- ( d e. a -> ( ( F |` a ) ` d ) = ( F ` d ) )
51	50	adantl 482	. . . . . . . . . 10 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` a ) ` d ) = ( F ` d ) )
52	49, 51	eqtrd 2656	. . . . . . . . 9 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` d ) = ( F ` d ) )
53	48	fveq1d 6193	. . . . . . . . . 10 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` f ) = ( ( F |` a ) ` f ) )
54		fvres 6207	. . . . . . . . . . 11 |- ( f e. a -> ( ( F |` a ) ` f ) = ( F ` f ) )
55	54	ad2antlr 763	. . . . . . . . . 10 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` a ) ` f ) = ( F ` f ) )
56	53, 55	eqtrd 2656	. . . . . . . . 9 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` f ) = ( F ` f ) )
57	52, 56	breq12d 4666	. . . . . . . 8 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) <-> ( F ` d ) R ( F ` f ) ) )
58	57	notbid 308	. . . . . . 7 |- ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) <-> -. ( F ` d ) R ( F ` f ) ) )
59	58	ralbidva 2985	. . . . . 6 |- ( ( ph /\ f e. a ) -> ( A. d e. a -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) <-> A. d e. a -. ( F ` d ) R ( F ` f ) ) )
60	46, 59	bitrd 268	. . . . 5 |- ( ( ph /\ f e. a ) -> ( A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) <-> A. d e. a -. ( F ` d ) R ( F ` f ) ) )
61	60	rexbidva 3049	. . . 4 |- ( ph -> ( E. f e. a A. e e. ( ( F |` A ) " a ) -. e R ( ( ( F |` A ) |` a ) ` f ) <-> E. f e. a A. d e. a -. ( F ` d ) R ( F ` f ) ) )
62	39, 61	bitrd 268	. . 3 |- ( ph -> ( E. d e. ( ( F |` A ) " a ) A. e e. ( ( F |` A ) " a ) -. e R d <-> E. f e. a A. d e. a -. ( F ` d ) R ( F ` f ) ) )
63	3	inex1 4799	. . . . . . 7 |- ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) e. _V
64	63	a1i 11	. . . . . 6 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) e. _V )
65	14	sselda 3603	. . . . . . . 8 |- ( ( ph /\ f e. a ) -> f e. A )
66		fnwe2.su	. . . . . . . . . 10 |- ( z = ( F ` x ) -> S = U )
67		fnwe2.t	. . . . . . . . . 10 |- T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
68		fnwe2.s	. . . . . . . . . 10 |- ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
69	66, 67, 68	fnwe2lem1 37620	. . . . . . . . 9 |- ( ( ph /\ f e. A ) -> [_ ( F ` f ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` f ) } )
70		wefr 5104	. . . . . . . . 9 |- ( [_ ( F ` f ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` f ) } -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
71	69, 70	syl 17	. . . . . . . 8 |- ( ( ph /\ f e. A ) -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
72	65, 71	syldan 487	. . . . . . 7 |- ( ( ph /\ f e. a ) -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
73	72	adantrr 753	. . . . . 6 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
74		inss2 3834	. . . . . . 7 |- ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) C_ { y e. A | ( F ` y ) = ( F ` f ) }
75	74	a1i 11	. . . . . 6 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) C_ { y e. A | ( F ` y ) = ( F ` f ) } )
76		simprl 794	. . . . . . . 8 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. a )
77	65	adantrr 753	. . . . . . . . 9 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. A )
78		eqidd 2623	. . . . . . . . 9 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( F ` f ) = ( F ` f ) )
79		fveq2 6191	. . . . . . . . . . 11 |- ( y = f -> ( F ` y ) = ( F ` f ) )
80	79	eqeq1d 2624	. . . . . . . . . 10 |- ( y = f -> ( ( F ` y ) = ( F ` f ) <-> ( F ` f ) = ( F ` f ) ) )
81	80	elrab 3363	. . . . . . . . 9 |- ( f e. { y e. A | ( F ` y ) = ( F ` f ) } <-> ( f e. A /\ ( F ` f ) = ( F ` f ) ) )
82	77, 78, 81	sylanbrc 698	. . . . . . . 8 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. { y e. A | ( F ` y ) = ( F ` f ) } )
83	76, 82	elind 3798	. . . . . . 7 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) )
84		ne0i 3921	. . . . . . 7 |- ( f e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -> ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) =/= (/) )
85	83, 84	syl 17	. . . . . 6 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) =/= (/) )
86		fri 5076	. . . . . 6 |- ( ( ( ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) e. _V /\ [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } ) /\ ( ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) C_ { y e. A | ( F ` y ) = ( F ` f ) } /\ ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) =/= (/) ) ) -> E. e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) A. g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -. g [_ ( F ` f ) / z ]_ S e )
87	64, 73, 75, 85, 86	syl22anc 1327	. . . . 5 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> E. e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) A. g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -. g [_ ( F ` f ) / z ]_ S e )
88		elin 3796	. . . . . . . 8 |- ( e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( e e. a /\ e e. { y e. A | ( F ` y ) = ( F ` f ) } ) )
89		fveq2 6191	. . . . . . . . . . 11 |- ( y = e -> ( F ` y ) = ( F ` e ) )
90	89	eqeq1d 2624	. . . . . . . . . 10 |- ( y = e -> ( ( F ` y ) = ( F ` f ) <-> ( F ` e ) = ( F ` f ) ) )
91	90	elrab 3363	. . . . . . . . 9 |- ( e e. { y e. A | ( F ` y ) = ( F ` f ) } <-> ( e e. A /\ ( F ` e ) = ( F ` f ) ) )
92	91	anbi2i 730	. . . . . . . 8 |- ( ( e e. a /\ e e. { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) )
93	88, 92	bitri 264	. . . . . . 7 |- ( e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) )
94		elin 3796	. . . . . . . . . . . . 13 |- ( g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( g e. a /\ g e. { y e. A | ( F ` y ) = ( F ` f ) } ) )
95		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( y = g -> ( F ` y ) = ( F ` g ) )
96	95	eqeq1d 2624	. . . . . . . . . . . . . . 15 |- ( y = g -> ( ( F ` y ) = ( F ` f ) <-> ( F ` g ) = ( F ` f ) ) )
97	96	elrab 3363	. . . . . . . . . . . . . 14 |- ( g e. { y e. A | ( F ` y ) = ( F ` f ) } <-> ( g e. A /\ ( F ` g ) = ( F ` f ) ) )
98	97	anbi2i 730	. . . . . . . . . . . . 13 |- ( ( g e. a /\ g e. { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( g e. a /\ ( g e. A /\ ( F ` g ) = ( F ` f ) ) ) )
99	94, 98	bitri 264	. . . . . . . . . . . 12 |- ( g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( g e. a /\ ( g e. A /\ ( F ` g ) = ( F ` f ) ) ) )
100	99	imbi1i 339	. . . . . . . . . . 11 |- ( ( g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -> -. g [_ ( F ` f ) / z ]_ S e ) <-> ( ( g e. a /\ ( g e. A /\ ( F ` g ) = ( F ` f ) ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) )
101		impexp 462	. . . . . . . . . . 11 |- ( ( ( g e. a /\ ( g e. A /\ ( F ` g ) = ( F ` f ) ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) <-> ( g e. a -> ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) )
102	100, 101	bitri 264	. . . . . . . . . 10 |- ( ( g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -> -. g [_ ( F ` f ) / z ]_ S e ) <-> ( g e. a -> ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) )
103	102	ralbii2 2978	. . . . . . . . 9 |- ( A. g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -. g [_ ( F ` f ) / z ]_ S e <-> A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) )
104		simplrl 800	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) -> e e. a )
105		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> c e. a )
106		simplrr 801	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) -> A. d e. a -. ( F ` d ) R ( F ` f ) )
107	106	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> A. d e. a -. ( F ` d ) R ( F ` f ) )
108		fveq2 6191	. . . . . . . . . . . . . . . . . . 19 |- ( d = c -> ( F ` d ) = ( F ` c ) )
109	108	breq1d 4663	. . . . . . . . . . . . . . . . . 18 |- ( d = c -> ( ( F ` d ) R ( F ` f ) <-> ( F ` c ) R ( F ` f ) ) )
110	109	notbid 308	. . . . . . . . . . . . . . . . 17 |- ( d = c -> ( -. ( F ` d ) R ( F ` f ) <-> -. ( F ` c ) R ( F ` f ) ) )
111	110	rspcva 3307	. . . . . . . . . . . . . . . 16 |- ( ( c e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) -> -. ( F ` c ) R ( F ` f ) )
112	105, 107, 111	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> -. ( F ` c ) R ( F ` f ) )
113		simprrr 805	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) -> ( F ` e ) = ( F ` f ) )
114	113	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> ( F ` e ) = ( F ` f ) )
115	114	breq2d 4665	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> ( ( F ` c ) R ( F ` e ) <-> ( F ` c ) R ( F ` f ) ) )
116	112, 115	mtbird 315	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> -. ( F ` c ) R ( F ` e ) )
117	14	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) -> a C_ A )
118	117	sselda 3603	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> c e. A )
119	118	adantrr 753	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> c e. A )
120		simprr 796	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> ( F ` c ) = ( F ` e ) )
121	113	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> ( F ` e ) = ( F ` f ) )
122	120, 121	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> ( F ` c ) = ( F ` f ) )
123		simprl 794	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> c e. a )
124		simplr 792	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) )
125		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = c -> ( g e. A <-> c e. A ) )
126		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( g = c -> ( F ` g ) = ( F ` c ) )
127	126	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = c -> ( ( F ` g ) = ( F ` f ) <-> ( F ` c ) = ( F ` f ) ) )
128	125, 127	anbi12d 747	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = c -> ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) <-> ( c e. A /\ ( F ` c ) = ( F ` f ) ) ) )
129		breq1 4656	. . . . . . . . . . . . . . . . . . . . . 22 |- ( g = c -> ( g [_ ( F ` f ) / z ]_ S e <-> c [_ ( F ` f ) / z ]_ S e ) )
130	129	notbid 308	. . . . . . . . . . . . . . . . . . . . 21 |- ( g = c -> ( -. g [_ ( F ` f ) / z ]_ S e <-> -. c [_ ( F ` f ) / z ]_ S e ) )
131	128, 130	imbi12d 334	. . . . . . . . . . . . . . . . . . . 20 |- ( g = c -> ( ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) <-> ( ( c e. A /\ ( F ` c ) = ( F ` f ) ) -> -. c [_ ( F ` f ) / z ]_ S e ) ) )
132	131	rspcva 3307	. . . . . . . . . . . . . . . . . . 19 |- ( ( c e. a /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) -> ( ( c e. A /\ ( F ` c ) = ( F ` f ) ) -> -. c [_ ( F ` f ) / z ]_ S e ) )
133	123, 124, 132	syl2anc 693	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> ( ( c e. A /\ ( F ` c ) = ( F ` f ) ) -> -. c [_ ( F ` f ) / z ]_ S e ) )
134	119, 122, 133	mp2and 715	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> -. c [_ ( F ` f ) / z ]_ S e )
135	120, 121	eqtr2d 2657	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> ( F ` f ) = ( F ` c ) )
136	135	csbeq1d 3540	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> [_ ( F ` f ) / z ]_ S = [_ ( F ` c ) / z ]_ S )
137	136	breqd 4664	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> ( c [_ ( F ` f ) / z ]_ S e <-> c [_ ( F ` c ) / z ]_ S e ) )
138	134, 137	mtbid 314	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ ( c e. a /\ ( F ` c ) = ( F ` e ) ) ) -> -. c [_ ( F ` c ) / z ]_ S e )
139	138	expr 643	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> ( ( F ` c ) = ( F ` e ) -> -. c [_ ( F ` c ) / z ]_ S e ) )
140		imnan 438	. . . . . . . . . . . . . . 15 |- ( ( ( F ` c ) = ( F ` e ) -> -. c [_ ( F ` c ) / z ]_ S e ) <-> -. ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) )
141	139, 140	sylib 208	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> -. ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) )
142		ioran 511	. . . . . . . . . . . . . 14 |- ( -. ( ( F ` c ) R ( F ` e ) \/ ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) ) <-> ( -. ( F ` c ) R ( F ` e ) /\ -. ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) ) )
143	116, 141, 142	sylanbrc 698	. . . . . . . . . . . . 13 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> -. ( ( F ` c ) R ( F ` e ) \/ ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) ) )
144	66, 67	fnwe2val 37619	. . . . . . . . . . . . 13 |- ( c T e <-> ( ( F ` c ) R ( F ` e ) \/ ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) ) )
145	143, 144	sylnibr 319	. . . . . . . . . . . 12 |- ( ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) /\ c e. a ) -> -. c T e )
146	145	ralrimiva 2966	. . . . . . . . . . 11 |- ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) -> A. c e. a -. c T e )
147		breq2 4657	. . . . . . . . . . . . . 14 |- ( b = e -> ( c T b <-> c T e ) )
148	147	notbid 308	. . . . . . . . . . . . 13 |- ( b = e -> ( -. c T b <-> -. c T e ) )
149	148	ralbidv 2986	. . . . . . . . . . . 12 |- ( b = e -> ( A. c e. a -. c T b <-> A. c e. a -. c T e ) )
150	149	rspcev 3309	. . . . . . . . . . 11 |- ( ( e e. a /\ A. c e. a -. c T e ) -> E. b e. a A. c e. a -. c T b )
151	104, 146, 150	syl2anc 693	. . . . . . . . . 10 |- ( ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) /\ A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) ) -> E. b e. a A. c e. a -. c T b )
152	151	ex 450	. . . . . . . . 9 |- ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) -> ( A. g e. a ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) -> -. g [_ ( F ` f ) / z ]_ S e ) -> E. b e. a A. c e. a -. c T b ) )
153	103, 152	syl5bi 232	. . . . . . . 8 |- ( ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) /\ ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) ) -> ( A. g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -. g [_ ( F ` f ) / z ]_ S e -> E. b e. a A. c e. a -. c T b ) )
154	153	ex 450	. . . . . . 7 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) -> ( A. g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -. g [_ ( F ` f ) / z ]_ S e -> E. b e. a A. c e. a -. c T b ) ) )
155	93, 154	syl5bi 232	. . . . . 6 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -> ( A. g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -. g [_ ( F ` f ) / z ]_ S e -> E. b e. a A. c e. a -. c T b ) ) )
156	155	rexlimdv 3030	. . . . 5 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( E. e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) A. g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) -. g [_ ( F ` f ) / z ]_ S e -> E. b e. a A. c e. a -. c T b ) )
157	87, 156	mpd 15	. . . 4 |- ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> E. b e. a A. c e. a -. c T b )
158	157	rexlimdvaa 3032	. . 3 |- ( ph -> ( E. f e. a A. d e. a -. ( F ` d ) R ( F ` f ) -> E. b e. a A. c e. a -. c T b ) )
159	62, 158	sylbid 230	. 2 |- ( ph -> ( E. d e. ( ( F |` A ) " a ) A. e e. ( ( F |` A ) " a ) -. e R d -> E. b e. a A. c e. a -. c T b ) )
160	27, 159	mpd 15	1 |- ( ph -> E. b e. a A. c e. a -. c T b )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   [_csb 3533   i^i cin 3573   C_ wss 3574   (/)c0 3915   class class class wbr 4653   {copab 4712   Fr wfr 5070   We wwe 5072   dom cdm 5114   ran crn 5115   |` cres 5116   "cima 5117   Fun wfun 5882   Fn wfn 5883   -->wf 5884   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  fnwe2  37623