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 ) |