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 df-ss
 |-  ( 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 syl5eq
 |-  ( 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 syl5bb
 |-  ( 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 syl5bb
 |-  ( 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 syl5bi
 |-  ( ( ( 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 syl5bi
 |-  ( ( 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 )