Metamath Proof Explorer

Theorem fnwe2lem3

Description: Lemma for fnwe2 . 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)

Ref Expression
Hypotheses 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 )
fnwe2lem3.a 
|- ( ph -> a C_ A )
fnwe2lem3.n0 
|- ( ph -> a =/= (/) )
Assertion fnwe2lem3 
|- ( ph -> E. b e. a A. c e. a -. c T b )

Proof

Step Hyp Ref Expression
1 fnwe2.su 
 |-  ( z = ( F ` x ) -> S = U )
2 fnwe2.t 
 |-  T = { <. x , y >. | ( ( F ` x ) R ( F ` y ) \/ ( ( F ` x ) = ( F ` y ) /\ x U y ) ) }
3 fnwe2.s 
 |-  ( ( ph /\ x e. A ) -> U We { y e. A | ( F ` y ) = ( F ` x ) } )
4 fnwe2.f 
 |-  ( ph -> ( F |` A ) : A --> B )
5 fnwe2.r 
 |-  ( ph -> R We B )
6 fnwe2lem3.a 
 |-  ( ph -> a C_ A )
7 fnwe2lem3.n0 
 |-  ( ph -> a =/= (/) )
8 ffun 
 |-  ( ( F |` A ) : A --> B -> Fun ( F |` A ) )
9 vex 
 |-  a e. _V
10 9 funimaex 
 |-  ( Fun ( F |` A ) -> ( ( F |` A ) " a ) e. _V )
11 4 8 10 3syl 
 |-  ( ph -> ( ( F |` A ) " a ) e. _V )
12 wefr 
 |-  ( R We B -> R Fr B )
13 5 12 syl 
 |-  ( ph -> R Fr B )
14 4 fimassd 
 |-  ( ph -> ( ( F |` A ) " a ) C_ B )
15 4 ffnd 
 |-  ( ph -> ( F |` A ) Fn A )
16 fnimaeq0 
 |-  ( ( ( F |` A ) Fn A /\ a C_ A ) -> ( ( ( F |` A ) " a ) = (/) <-> a = (/) ) )
17 15 6 16 syl2anc 
 |-  ( ph -> ( ( ( F |` A ) " a ) = (/) <-> a = (/) ) )
18 17 necon3bid 
 |-  ( ph -> ( ( ( F |` A ) " a ) =/= (/) <-> a =/= (/) ) )
19 7 18 mpbird 
 |-  ( ph -> ( ( F |` A ) " a ) =/= (/) )
20 fri 
 |-  ( ( ( ( ( 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 )
21 11 13 14 19 20 syl22anc 
 |-  ( ph -> E. d e. ( ( F |` A ) " a ) A. e e. ( ( F |` A ) " a ) -. e R d )
22 df-ima 
 |-  ( ( F |` A ) " a ) = ran ( ( F |` A ) |` a )
23 22 rexeqi 
 |-  ( 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 )
24 15 6 fnssresd 
 |-  ( ph -> ( ( F |` A ) |` a ) Fn a )
25 breq2 
 |-  ( d = ( ( ( F |` A ) |` a ) ` f ) -> ( e R d <-> e R ( ( ( F |` A ) |` a ) ` f ) ) )
26 25 notbid 
 |-  ( d = ( ( ( F |` A ) |` a ) ` f ) -> ( -. e R d <-> -. e R ( ( ( F |` A ) |` a ) ` f ) ) )
27 26 ralbidv 
 |-  ( 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 ) ) )
28 27 rexrn 
 |-  ( ( ( 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 ) ) )
29 24 28 syl 
 |-  ( 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 ) ) )
30 23 29 bitrid 
 |-  ( 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 ) ) )
31 22 raleqi 
 |-  ( 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 ) )
32 breq1 
 |-  ( e = ( ( ( F |` A ) |` a ) ` d ) -> ( e R ( ( ( F |` A ) |` a ) ` f ) <-> ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
33 32 notbid 
 |-  ( e = ( ( ( F |` A ) |` a ) ` d ) -> ( -. e R ( ( ( F |` A ) |` a ) ` f ) <-> -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
34 33 ralrn 
 |-  ( ( ( 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 ) ) )
35 24 34 syl 
 |-  ( 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 ) ) )
36 31 35 bitrid 
 |-  ( 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 ) ) )
37 36 adantr 
 |-  ( ( 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 ) ) )
38 6 resabs1d 
 |-  ( ph -> ( ( F |` A ) |` a ) = ( F |` a ) )
39 38 ad2antrr 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` A ) |` a ) = ( F |` a ) )
40 39 fveq1d 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` d ) = ( ( F |` a ) ` d ) )
41 fvres 
 |-  ( d e. a -> ( ( F |` a ) ` d ) = ( F ` d ) )
42 41 adantl 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` a ) ` d ) = ( F ` d ) )
43 40 42 eqtrd 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` d ) = ( F ` d ) )
44 39 fveq1d 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` f ) = ( ( F |` a ) ` f ) )
45 fvres 
 |-  ( f e. a -> ( ( F |` a ) ` f ) = ( F ` f ) )
46 45 ad2antlr 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` a ) ` f ) = ( F ` f ) )
47 44 46 eqtrd 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` f ) = ( F ` f ) )
48 43 47 breq12d 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) <-> ( F ` d ) R ( F ` f ) ) )
49 48 notbid 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) <-> -. ( F ` d ) R ( F ` f ) ) )
50 49 ralbidva 
 |-  ( ( 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 ) ) )
51 37 50 bitrd 
 |-  ( ( 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 ) ) )
52 51 rexbidva 
 |-  ( 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 ) ) )
53 30 52 bitrd 
 |-  ( 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 ) ) )
54 9 inex1 
 |-  ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) e. _V
55 54 a1i 
 |-  ( ( 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 )
56 6 sselda 
 |-  ( ( ph /\ f e. a ) -> f e. A )
57 1 2 3 fnwe2lem2 
 |-  ( ( ph /\ f e. A ) -> [_ ( F ` f ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` f ) } )
58 wefr 
 |-  ( [_ ( F ` f ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` f ) } -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
59 57 58 syl 
 |-  ( ( ph /\ f e. A ) -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
60 56 59 syldan 
 |-  ( ( ph /\ f e. a ) -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
61 60 adantrr 
 |-  ( ( 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 ) } )
62 inss2 
 |-  ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) C_ { y e. A | ( F ` y ) = ( F ` f ) }
63 62 a1i 
 |-  ( ( 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 ) } )
64 simprl 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. a )
65 fveqeq2 
 |-  ( y = f -> ( ( F ` y ) = ( F ` f ) <-> ( F ` f ) = ( F ` f ) ) )
66 56 adantrr 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. A )
67 eqidd 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( F ` f ) = ( F ` f ) )
68 65 66 67 elrabd 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. { y e. A | ( F ` y ) = ( F ` f ) } )
69 64 68 elind 
 |-  ( ( 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 ) } ) )
70 69 ne0d 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) =/= (/) )
71 fri 
 |-  ( ( ( ( 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 )
72 55 61 63 70 71 syl22anc 
 |-  ( ( 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 )
73 elin 
 |-  ( e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( e e. a /\ e e. { y e. A | ( F ` y ) = ( F ` f ) } ) )
74 fveqeq2 
 |-  ( y = e -> ( ( F ` y ) = ( F ` f ) <-> ( F ` e ) = ( F ` f ) ) )
75 74 elrab 
 |-  ( e e. { y e. A | ( F ` y ) = ( F ` f ) } <-> ( e e. A /\ ( F ` e ) = ( F ` f ) ) )
76 75 anbi2i 
 |-  ( ( e e. a /\ e e. { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) )
77 73 76 bitri 
 |-  ( e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) )
78 elin 
 |-  ( g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( g e. a /\ g e. { y e. A | ( F ` y ) = ( F ` f ) } ) )
79 fveqeq2 
 |-  ( y = g -> ( ( F ` y ) = ( F ` f ) <-> ( F ` g ) = ( F ` f ) ) )
80 79 elrab 
 |-  ( g e. { y e. A | ( F ` y ) = ( F ` f ) } <-> ( g e. A /\ ( F ` g ) = ( F ` f ) ) )
81 80 anbi2i 
 |-  ( ( g e. a /\ g e. { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( g e. a /\ ( g e. A /\ ( F ` g ) = ( F ` f ) ) ) )
82 78 81 bitri 
 |-  ( g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( g e. a /\ ( g e. A /\ ( F ` g ) = ( F ` f ) ) ) )
83 82 imbi1i 
 |-  ( ( 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 ) )
84 impexp 
 |-  ( ( ( 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 ) ) )
85 83 84 bitri 
 |-  ( ( 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 ) ) )
86 85 ralbii2 
 |-  ( 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 ) )
87 breq2 
 |-  ( b = e -> ( c T b <-> c T e ) )
88 87 notbid 
 |-  ( b = e -> ( -. c T b <-> -. c T e ) )
89 88 ralbidv 
 |-  ( b = e -> ( A. c e. a -. c T b <-> A. c e. a -. c T e ) )
90 simplrl 
 |-  ( ( ( ( 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 )
91 fveq2 
 |-  ( d = c -> ( F ` d ) = ( F ` c ) )
92 91 breq1d 
 |-  ( d = c -> ( ( F ` d ) R ( F ` f ) <-> ( F ` c ) R ( F ` f ) ) )
93 92 notbid 
 |-  ( d = c -> ( -. ( F ` d ) R ( F ` f ) <-> -. ( F ` c ) R ( F ` f ) ) )
94 simplrr 
 |-  ( ( ( 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 ) )
95 94 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
96 simpr 
 |-  ( ( ( ( ( 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 )
97 93 95 96 rspcdva 
 |-  ( ( ( ( ( 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 ) )
98 simprrr 
 |-  ( ( ( 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 ) )
99 98 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
100 99 breq2d 
 |-  ( ( ( ( ( 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 ) ) )
101 97 100 mtbird 
 |-  ( ( ( ( ( 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 ) )
102 6 ad3antrrr 
 |-  ( ( ( ( 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 )
103 102 sselda 
 |-  ( ( ( ( ( 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 )
104 103 adantrr 
 |-  ( ( ( ( ( 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 )
105 simprr 
 |-  ( ( ( ( ( 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 ) )
106 98 ad2antrr 
 |-  ( ( ( ( ( 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 ) )
107 105 106 eqtrd 
 |-  ( ( ( ( ( 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 ) )
108 eleq1w 
 |-  ( g = c -> ( g e. A <-> c e. A ) )
109 fveqeq2 
 |-  ( g = c -> ( ( F ` g ) = ( F ` f ) <-> ( F ` c ) = ( F ` f ) ) )
110 108 109 anbi12d 
 |-  ( g = c -> ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) <-> ( c e. A /\ ( F ` c ) = ( F ` f ) ) ) )
111 breq1 
 |-  ( g = c -> ( g [_ ( F ` f ) / z ]_ S e <-> c [_ ( F ` f ) / z ]_ S e ) )
112 111 notbid 
 |-  ( g = c -> ( -. g [_ ( F ` f ) / z ]_ S e <-> -. c [_ ( F ` f ) / z ]_ S e ) )
113 110 112 imbi12d 
 |-  ( 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 ) ) )
114 simplr 
 |-  ( ( ( ( ( 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 ) )
115 simprl 
 |-  ( ( ( ( ( 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 )
116 113 114 115 rspcdva 
 |-  ( ( ( ( ( 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 ) )
117 104 107 116 mp2and 
 |-  ( ( ( ( ( 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 )
118 105 106 eqtr2d 
 |-  ( ( ( ( ( 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 ) )
119 118 csbeq1d 
 |-  ( ( ( ( ( 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 )
120 119 breqd 
 |-  ( ( ( ( ( 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 ) )
121 117 120 mtbid 
 |-  ( ( ( ( ( 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 )
122 121 expr 
 |-  ( ( ( ( ( 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 ) )
123 imnan 
 |-  ( ( ( F ` c ) = ( F ` e ) -> -. c [_ ( F ` c ) / z ]_ S e ) <-> -. ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) )
124 122 123 sylib 
 |-  ( ( ( ( ( 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 ) )
125 ioran 
 |-  ( -. ( ( 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 ) ) )
126 101 124 125 sylanbrc 
 |-  ( ( ( ( ( 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 ) ) )
127 1 2 fnwe2lem1 
 |-  ( c T e <-> ( ( F ` c ) R ( F ` e ) \/ ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) ) )
128 126 127 sylnibr 
 |-  ( ( ( ( ( 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 )
129 128 ralrimiva 
 |-  ( ( ( ( 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 )
130 89 90 129 rspcedvdw 
 |-  ( ( ( ( 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 )
131 130 ex 
 |-  ( ( ( 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 ) )
132 86 131 biimtrid 
 |-  ( ( ( 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 ) )
133 132 ex 
 |-  ( ( 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 ) ) )
134 77 133 biimtrid 
 |-  ( ( 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 ) ) )
135 134 rexlimdv 
 |-  ( ( 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 ) )
136 72 135 mpd 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> E. b e. a A. c e. a -. c T b )
137 136 rexlimdvaa 
 |-  ( 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 ) )
138 53 137 sylbid 
 |-  ( 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 ) )
139 21 138 mpd 
 |-  ( ph -> E. b e. a A. c e. a -. c T b )