Step |
Hyp |
Ref |
Expression |
1 |
|
pwfseqlem4.g |
|- ( ph -> G : ~P A -1-1-> U_ n e. _om ( A ^m n ) ) |
2 |
|
pwfseqlem4.x |
|- ( ph -> X C_ A ) |
3 |
|
pwfseqlem4.h |
|- ( ph -> H : _om -1-1-onto-> X ) |
4 |
|
pwfseqlem4.ps |
|- ( ps <-> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) ) |
5 |
|
pwfseqlem4.k |
|- ( ( ph /\ ps ) -> K : U_ n e. _om ( x ^m n ) -1-1-> x ) |
6 |
|
pwfseqlem4.d |
|- D = ( G ` { w e. x | ( ( `' K ` w ) e. ran G /\ -. w e. ( `' G ` ( `' K ` w ) ) ) } ) |
7 |
|
pwfseqlem4.f |
|- F = ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) ) |
8 |
|
isfinite |
|- ( a e. Fin <-> a ~< _om ) |
9 |
|
simpr |
|- ( ( ph /\ a e. Fin ) -> a e. Fin ) |
10 |
|
vex |
|- s e. _V |
11 |
1 2 3 4 5 6 7
|
pwfseqlem2 |
|- ( ( a e. Fin /\ s e. _V ) -> ( a F s ) = ( H ` ( card ` a ) ) ) |
12 |
9 10 11
|
sylancl |
|- ( ( ph /\ a e. Fin ) -> ( a F s ) = ( H ` ( card ` a ) ) ) |
13 |
|
f1of |
|- ( H : _om -1-1-onto-> X -> H : _om --> X ) |
14 |
3 13
|
syl |
|- ( ph -> H : _om --> X ) |
15 |
14 2
|
fssd |
|- ( ph -> H : _om --> A ) |
16 |
|
ficardom |
|- ( a e. Fin -> ( card ` a ) e. _om ) |
17 |
|
ffvelrn |
|- ( ( H : _om --> A /\ ( card ` a ) e. _om ) -> ( H ` ( card ` a ) ) e. A ) |
18 |
15 16 17
|
syl2an |
|- ( ( ph /\ a e. Fin ) -> ( H ` ( card ` a ) ) e. A ) |
19 |
12 18
|
eqeltrd |
|- ( ( ph /\ a e. Fin ) -> ( a F s ) e. A ) |
20 |
19
|
ex |
|- ( ph -> ( a e. Fin -> ( a F s ) e. A ) ) |
21 |
20
|
adantr |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a e. Fin -> ( a F s ) e. A ) ) |
22 |
8 21
|
syl5bir |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a ~< _om -> ( a F s ) e. A ) ) |
23 |
|
omelon |
|- _om e. On |
24 |
|
onenon |
|- ( _om e. On -> _om e. dom card ) |
25 |
23 24
|
ax-mp |
|- _om e. dom card |
26 |
|
simpr3 |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> s We a ) |
27 |
26
|
19.8ad |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> E. s s We a ) |
28 |
|
ween |
|- ( a e. dom card <-> E. s s We a ) |
29 |
27 28
|
sylibr |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> a e. dom card ) |
30 |
|
domtri2 |
|- ( ( _om e. dom card /\ a e. dom card ) -> ( _om ~<_ a <-> -. a ~< _om ) ) |
31 |
25 29 30
|
sylancr |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a <-> -. a ~< _om ) ) |
32 |
|
nfv |
|- F/ r ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) |
33 |
|
nfcv |
|- F/_ r a |
34 |
|
nfmpo2 |
|- F/_ r ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) ) |
35 |
7 34
|
nfcxfr |
|- F/_ r F |
36 |
|
nfcv |
|- F/_ r s |
37 |
33 35 36
|
nfov |
|- F/_ r ( a F s ) |
38 |
37
|
nfel1 |
|- F/ r ( a F s ) e. ( A \ a ) |
39 |
32 38
|
nfim |
|- F/ r ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) ) |
40 |
|
sseq1 |
|- ( r = s -> ( r C_ ( a X. a ) <-> s C_ ( a X. a ) ) ) |
41 |
|
weeq1 |
|- ( r = s -> ( r We a <-> s We a ) ) |
42 |
40 41
|
3anbi23d |
|- ( r = s -> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) <-> ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) ) |
43 |
42
|
anbi1d |
|- ( r = s -> ( ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) <-> ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) ) |
44 |
43
|
anbi2d |
|- ( r = s -> ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) <-> ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) ) ) |
45 |
|
oveq2 |
|- ( r = s -> ( a F r ) = ( a F s ) ) |
46 |
45
|
eleq1d |
|- ( r = s -> ( ( a F r ) e. ( A \ a ) <-> ( a F s ) e. ( A \ a ) ) ) |
47 |
44 46
|
imbi12d |
|- ( r = s -> ( ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) ) <-> ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) ) ) ) |
48 |
|
nfv |
|- F/ x ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) |
49 |
|
nfcv |
|- F/_ x a |
50 |
|
nfmpo1 |
|- F/_ x ( x e. _V , r e. _V |-> if ( x e. Fin , ( H ` ( card ` x ) ) , ( D ` |^| { z e. _om | -. ( D ` z ) e. x } ) ) ) |
51 |
7 50
|
nfcxfr |
|- F/_ x F |
52 |
|
nfcv |
|- F/_ x r |
53 |
49 51 52
|
nfov |
|- F/_ x ( a F r ) |
54 |
53
|
nfel1 |
|- F/ x ( a F r ) e. ( A \ a ) |
55 |
48 54
|
nfim |
|- F/ x ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) ) |
56 |
|
sseq1 |
|- ( x = a -> ( x C_ A <-> a C_ A ) ) |
57 |
|
xpeq12 |
|- ( ( x = a /\ x = a ) -> ( x X. x ) = ( a X. a ) ) |
58 |
57
|
anidms |
|- ( x = a -> ( x X. x ) = ( a X. a ) ) |
59 |
58
|
sseq2d |
|- ( x = a -> ( r C_ ( x X. x ) <-> r C_ ( a X. a ) ) ) |
60 |
|
weeq2 |
|- ( x = a -> ( r We x <-> r We a ) ) |
61 |
56 59 60
|
3anbi123d |
|- ( x = a -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) ) ) |
62 |
|
breq2 |
|- ( x = a -> ( _om ~<_ x <-> _om ~<_ a ) ) |
63 |
61 62
|
anbi12d |
|- ( x = a -> ( ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) /\ _om ~<_ x ) <-> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) ) |
64 |
4 63
|
syl5bb |
|- ( x = a -> ( ps <-> ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) ) |
65 |
64
|
anbi2d |
|- ( x = a -> ( ( ph /\ ps ) <-> ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) ) ) |
66 |
|
oveq1 |
|- ( x = a -> ( x F r ) = ( a F r ) ) |
67 |
|
difeq2 |
|- ( x = a -> ( A \ x ) = ( A \ a ) ) |
68 |
66 67
|
eleq12d |
|- ( x = a -> ( ( x F r ) e. ( A \ x ) <-> ( a F r ) e. ( A \ a ) ) ) |
69 |
65 68
|
imbi12d |
|- ( x = a -> ( ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) ) <-> ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) ) ) ) |
70 |
1 2 3 4 5 6 7
|
pwfseqlem3 |
|- ( ( ph /\ ps ) -> ( x F r ) e. ( A \ x ) ) |
71 |
55 69 70
|
chvarfv |
|- ( ( ph /\ ( ( a C_ A /\ r C_ ( a X. a ) /\ r We a ) /\ _om ~<_ a ) ) -> ( a F r ) e. ( A \ a ) ) |
72 |
39 47 71
|
chvarfv |
|- ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. ( A \ a ) ) |
73 |
72
|
eldifad |
|- ( ( ph /\ ( ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) /\ _om ~<_ a ) ) -> ( a F s ) e. A ) |
74 |
73
|
expr |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( _om ~<_ a -> ( a F s ) e. A ) ) |
75 |
31 74
|
sylbird |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( -. a ~< _om -> ( a F s ) e. A ) ) |
76 |
22 75
|
pm2.61d |
|- ( ( ph /\ ( a C_ A /\ s C_ ( a X. a ) /\ s We a ) ) -> ( a F s ) e. A ) |