Metamath Proof Explorer

Theorem fnwe2lem2

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 )
fnwe2lem2.a 
|- ( ph -> a C_ A )
fnwe2lem2.n0 
|- ( ph -> a =/= (/) )
Assertion fnwe2lem2 
|- ( 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 fnwe2lem2.a 
 |-  ( ph -> a C_ A )
7 fnwe2lem2.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 imassrn 
 |-  ( ( F |` A ) " a ) C_ ran ( F |` A )
15 4 frnd 
 |-  ( ph -> ran ( F |` A ) C_ B )
16 14 15 sstrid 
 |-  ( ph -> ( ( F |` A ) " a ) C_ B )
17 incom 
 |-  ( dom ( F |` A ) i^i a ) = ( a i^i dom ( F |` A ) )
18 4 fdmd 
 |-  ( ph -> dom ( F |` A ) = A )
19 6 18 sseqtrrd 
 |-  ( ph -> a C_ dom ( F |` A ) )
20 dfss2 
 |-  ( a C_ dom ( F |` A ) <-> ( a i^i dom ( F |` A ) ) = a )
21 19 20 sylib 
 |-  ( ph -> ( a i^i dom ( F |` A ) ) = a )
22 17 21 eqtrid 
 |-  ( ph -> ( dom ( F |` A ) i^i a ) = a )
23 22 7 eqnetrd 
 |-  ( ph -> ( dom ( F |` A ) i^i a ) =/= (/) )
24 imadisj 
 |-  ( ( ( F |` A ) " a ) = (/) <-> ( dom ( F |` A ) i^i a ) = (/) )
25 24 necon3bii 
 |-  ( ( ( F |` A ) " a ) =/= (/) <-> ( dom ( F |` A ) i^i a ) =/= (/) )
26 23 25 sylibr 
 |-  ( ph -> ( ( F |` A ) " a ) =/= (/) )
27 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 )
28 11 13 16 26 27 syl22anc 
 |-  ( ph -> E. d e. ( ( F |` A ) " a ) A. e e. ( ( F |` A ) " a ) -. e R d )
29 df-ima 
 |-  ( ( F |` A ) " a ) = ran ( ( F |` A ) |` a )
30 29 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 )
31 4 ffnd 
 |-  ( ph -> ( F |` A ) Fn A )
32 fnssres 
 |-  ( ( ( F |` A ) Fn A /\ a C_ A ) -> ( ( F |` A ) |` a ) Fn a )
33 31 6 32 syl2anc 
 |-  ( ph -> ( ( F |` A ) |` a ) Fn a )
34 breq2 
 |-  ( d = ( ( ( F |` A ) |` a ) ` f ) -> ( e R d <-> e R ( ( ( F |` A ) |` a ) ` f ) ) )
35 34 notbid 
 |-  ( d = ( ( ( F |` A ) |` a ) ` f ) -> ( -. e R d <-> -. e R ( ( ( F |` A ) |` a ) ` f ) ) )
36 35 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 ) ) )
37 36 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 ) ) )
38 33 37 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 ) ) )
39 30 38 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 ) ) )
40 29 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 ) )
41 breq1 
 |-  ( e = ( ( ( F |` A ) |` a ) ` d ) -> ( e R ( ( ( F |` A ) |` a ) ` f ) <-> ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
42 41 notbid 
 |-  ( e = ( ( ( F |` A ) |` a ) ` d ) -> ( -. e R ( ( ( F |` A ) |` a ) ` f ) <-> -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) ) )
43 42 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 ) ) )
44 33 43 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 ) ) )
45 40 44 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 ) ) )
46 45 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 ) ) )
47 6 resabs1d 
 |-  ( ph -> ( ( F |` A ) |` a ) = ( F |` a ) )
48 47 ad2antrr 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` A ) |` a ) = ( F |` a ) )
49 48 fveq1d 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` d ) = ( ( F |` a ) ` d ) )
50 fvres 
 |-  ( d e. a -> ( ( F |` a ) ` d ) = ( F ` d ) )
51 50 adantl 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` a ) ` d ) = ( F ` d ) )
52 49 51 eqtrd 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` d ) = ( F ` d ) )
53 48 fveq1d 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` f ) = ( ( F |` a ) ` f ) )
54 fvres 
 |-  ( f e. a -> ( ( F |` a ) ` f ) = ( F ` f ) )
55 54 ad2antlr 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( F |` a ) ` f ) = ( F ` f ) )
56 53 55 eqtrd 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( F |` A ) |` a ) ` f ) = ( F ` f ) )
57 52 56 breq12d 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) <-> ( F ` d ) R ( F ` f ) ) )
58 57 notbid 
 |-  ( ( ( ph /\ f e. a ) /\ d e. a ) -> ( -. ( ( ( F |` A ) |` a ) ` d ) R ( ( ( F |` A ) |` a ) ` f ) <-> -. ( F ` d ) R ( F ` f ) ) )
59 58 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 ) ) )
60 46 59 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 ) ) )
61 60 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 ) ) )
62 39 61 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 ) ) )
63 9 inex1 
 |-  ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) e. _V
64 63 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 )
65 6 sselda 
 |-  ( ( ph /\ f e. a ) -> f e. A )
66 1 2 3 fnwe2lem1 
 |-  ( ( ph /\ f e. A ) -> [_ ( F ` f ) / z ]_ S We { y e. A | ( F ` y ) = ( F ` f ) } )
67 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 ) } )
68 66 67 syl 
 |-  ( ( ph /\ f e. A ) -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
69 65 68 syldan 
 |-  ( ( ph /\ f e. a ) -> [_ ( F ` f ) / z ]_ S Fr { y e. A | ( F ` y ) = ( F ` f ) } )
70 69 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 ) } )
71 inss2 
 |-  ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) C_ { y e. A | ( F ` y ) = ( F ` f ) }
72 71 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 ) } )
73 simprl 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. a )
74 fveqeq2 
 |-  ( y = f -> ( ( F ` y ) = ( F ` f ) <-> ( F ` f ) = ( F ` f ) ) )
75 65 adantrr 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. A )
76 eqidd 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( F ` f ) = ( F ` f ) )
77 74 75 76 elrabd 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> f e. { y e. A | ( F ` y ) = ( F ` f ) } )
78 73 77 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 ) } ) )
79 78 ne0d 
 |-  ( ( ph /\ ( f e. a /\ A. d e. a -. ( F ` d ) R ( F ` f ) ) ) -> ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) =/= (/) )
80 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 )
81 64 70 72 79 80 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 )
82 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 ) } ) )
83 fveqeq2 
 |-  ( y = e -> ( ( F ` y ) = ( F ` f ) <-> ( F ` e ) = ( F ` f ) ) )
84 83 elrab 
 |-  ( e e. { y e. A | ( F ` y ) = ( F ` f ) } <-> ( e e. A /\ ( F ` e ) = ( F ` f ) ) )
85 84 anbi2i 
 |-  ( ( e e. a /\ e e. { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) )
86 82 85 bitri 
 |-  ( e e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( e e. a /\ ( e e. A /\ ( F ` e ) = ( F ` f ) ) ) )
87 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 ) } ) )
88 fveqeq2 
 |-  ( y = g -> ( ( F ` y ) = ( F ` f ) <-> ( F ` g ) = ( F ` f ) ) )
89 88 elrab 
 |-  ( g e. { y e. A | ( F ` y ) = ( F ` f ) } <-> ( g e. A /\ ( F ` g ) = ( F ` f ) ) )
90 89 anbi2i 
 |-  ( ( g e. a /\ g e. { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( g e. a /\ ( g e. A /\ ( F ` g ) = ( F ` f ) ) ) )
91 87 90 bitri 
 |-  ( g e. ( a i^i { y e. A | ( F ` y ) = ( F ` f ) } ) <-> ( g e. a /\ ( g e. A /\ ( F ` g ) = ( F ` f ) ) ) )
92 91 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 ) )
93 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 ) ) )
94 92 93 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 ) ) )
95 94 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 ) )
96 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 )
97 fveq2 
 |-  ( d = c -> ( F ` d ) = ( F ` c ) )
98 97 breq1d 
 |-  ( d = c -> ( ( F ` d ) R ( F ` f ) <-> ( F ` c ) R ( F ` f ) ) )
99 98 notbid 
 |-  ( d = c -> ( -. ( F ` d ) R ( F ` f ) <-> -. ( F ` c ) R ( F ` f ) ) )
100 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 ) )
101 100 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 ) )
102 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 )
103 99 101 102 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 ) )
104 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 ) )
105 104 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 ) )
106 105 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 ) ) )
107 103 106 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 ) )
108 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 )
109 108 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 )
110 109 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 )
111 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 ) )
112 104 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 ) )
113 111 112 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 ) )
114 eleq1w 
 |-  ( g = c -> ( g e. A <-> c e. A ) )
115 fveqeq2 
 |-  ( g = c -> ( ( F ` g ) = ( F ` f ) <-> ( F ` c ) = ( F ` f ) ) )
116 114 115 anbi12d 
 |-  ( g = c -> ( ( g e. A /\ ( F ` g ) = ( F ` f ) ) <-> ( c e. A /\ ( F ` c ) = ( F ` f ) ) ) )
117 breq1 
 |-  ( g = c -> ( g [_ ( F ` f ) / z ]_ S e <-> c [_ ( F ` f ) / z ]_ S e ) )
118 117 notbid 
 |-  ( g = c -> ( -. g [_ ( F ` f ) / z ]_ S e <-> -. c [_ ( F ` f ) / z ]_ S e ) )
119 116 118 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 ) ) )
120 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 ) )
121 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 )
122 119 120 121 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 ) )
123 110 113 122 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 )
124 111 112 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 ) )
125 124 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 )
126 125 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 ) )
127 123 126 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 )
128 127 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 ) )
129 imnan 
 |-  ( ( ( F ` c ) = ( F ` e ) -> -. c [_ ( F ` c ) / z ]_ S e ) <-> -. ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) )
130 128 129 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 ) )
131 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 ) ) )
132 107 130 131 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 ) ) )
133 1 2 fnwe2val 
 |-  ( c T e <-> ( ( F ` c ) R ( F ` e ) \/ ( ( F ` c ) = ( F ` e ) /\ c [_ ( F ` c ) / z ]_ S e ) ) )
134 132 133 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 )
135 134 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 )
136 breq2 
 |-  ( b = e -> ( c T b <-> c T e ) )
137 136 notbid 
 |-  ( b = e -> ( -. c T b <-> -. c T e ) )
138 137 ralbidv 
 |-  ( b = e -> ( A. c e. a -. c T b <-> A. c e. a -. c T e ) )
139 138 rspcev 
 |-  ( ( e e. a /\ A. c e. a -. c T e ) -> E. b e. a A. c e. a -. c T b )
140 96 135 139 syl2anc 
 |-  ( ( ( ( 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 )
141 140 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 ) )
142 95 141 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 ) )
143 142 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 ) ) )
144 86 143 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 ) ) )
145 144 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 ) )
146 81 145 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 )
147 146 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 ) )
148 62 147 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 ) )
149 28 148 mpd 
 |-  ( ph -> E. b e. a A. c e. a -. c T b )