Step |
Hyp |
Ref |
Expression |
1 |
|
cnfcom.s |
|- S = dom ( _om CNF A ) |
2 |
|
cnfcom.a |
|- ( ph -> A e. On ) |
3 |
|
cnfcom.b |
|- ( ph -> B e. ( _om ^o A ) ) |
4 |
|
cnfcom.f |
|- F = ( `' ( _om CNF A ) ` B ) |
5 |
|
cnfcom.g |
|- G = OrdIso ( _E , ( F supp (/) ) ) |
6 |
|
cnfcom.h |
|- H = seqom ( ( k e. _V , z e. _V |-> ( M +o z ) ) , (/) ) |
7 |
|
cnfcom.t |
|- T = seqom ( ( k e. _V , f e. _V |-> K ) , (/) ) |
8 |
|
cnfcom.m |
|- M = ( ( _om ^o ( G ` k ) ) .o ( F ` ( G ` k ) ) ) |
9 |
|
cnfcom.k |
|- K = ( ( x e. M |-> ( dom f +o x ) ) u. `' ( x e. dom f |-> ( M +o x ) ) ) |
10 |
|
cnfcom.w |
|- W = ( G ` U. dom G ) |
11 |
|
cnfcom3.1 |
|- ( ph -> _om C_ B ) |
12 |
|
cnfcom.x |
|- X = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( F ` W ) .o v ) +o u ) ) |
13 |
|
cnfcom.y |
|- Y = ( u e. ( F ` W ) , v e. ( _om ^o W ) |-> ( ( ( _om ^o W ) .o u ) +o v ) ) |
14 |
|
cnfcom.n |
|- N = ( ( X o. `' Y ) o. ( T ` dom G ) ) |
15 |
|
omelon |
|- _om e. On |
16 |
|
suppssdm |
|- ( F supp (/) ) C_ dom F |
17 |
15
|
a1i |
|- ( ph -> _om e. On ) |
18 |
1 17 2
|
cantnff1o |
|- ( ph -> ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) ) |
19 |
|
f1ocnv |
|- ( ( _om CNF A ) : S -1-1-onto-> ( _om ^o A ) -> `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S ) |
20 |
|
f1of |
|- ( `' ( _om CNF A ) : ( _om ^o A ) -1-1-onto-> S -> `' ( _om CNF A ) : ( _om ^o A ) --> S ) |
21 |
18 19 20
|
3syl |
|- ( ph -> `' ( _om CNF A ) : ( _om ^o A ) --> S ) |
22 |
21 3
|
ffvelrnd |
|- ( ph -> ( `' ( _om CNF A ) ` B ) e. S ) |
23 |
4 22
|
eqeltrid |
|- ( ph -> F e. S ) |
24 |
1 17 2
|
cantnfs |
|- ( ph -> ( F e. S <-> ( F : A --> _om /\ F finSupp (/) ) ) ) |
25 |
23 24
|
mpbid |
|- ( ph -> ( F : A --> _om /\ F finSupp (/) ) ) |
26 |
25
|
simpld |
|- ( ph -> F : A --> _om ) |
27 |
16 26
|
fssdm |
|- ( ph -> ( F supp (/) ) C_ A ) |
28 |
|
ovex |
|- ( F supp (/) ) e. _V |
29 |
5
|
oion |
|- ( ( F supp (/) ) e. _V -> dom G e. On ) |
30 |
28 29
|
ax-mp |
|- dom G e. On |
31 |
30
|
elexi |
|- dom G e. _V |
32 |
31
|
uniex |
|- U. dom G e. _V |
33 |
32
|
sucid |
|- U. dom G e. suc U. dom G |
34 |
|
peano1 |
|- (/) e. _om |
35 |
34
|
a1i |
|- ( ph -> (/) e. _om ) |
36 |
11 35
|
sseldd |
|- ( ph -> (/) e. B ) |
37 |
1 2 3 4 5 6 7 8 9 10 36
|
cnfcom2lem |
|- ( ph -> dom G = suc U. dom G ) |
38 |
33 37
|
eleqtrrid |
|- ( ph -> U. dom G e. dom G ) |
39 |
5
|
oif |
|- G : dom G --> ( F supp (/) ) |
40 |
39
|
ffvelrni |
|- ( U. dom G e. dom G -> ( G ` U. dom G ) e. ( F supp (/) ) ) |
41 |
38 40
|
syl |
|- ( ph -> ( G ` U. dom G ) e. ( F supp (/) ) ) |
42 |
10 41
|
eqeltrid |
|- ( ph -> W e. ( F supp (/) ) ) |
43 |
27 42
|
sseldd |
|- ( ph -> W e. A ) |
44 |
|
onelon |
|- ( ( A e. On /\ W e. A ) -> W e. On ) |
45 |
2 43 44
|
syl2anc |
|- ( ph -> W e. On ) |
46 |
|
oecl |
|- ( ( _om e. On /\ W e. On ) -> ( _om ^o W ) e. On ) |
47 |
15 45 46
|
sylancr |
|- ( ph -> ( _om ^o W ) e. On ) |
48 |
26 43
|
ffvelrnd |
|- ( ph -> ( F ` W ) e. _om ) |
49 |
|
nnon |
|- ( ( F ` W ) e. _om -> ( F ` W ) e. On ) |
50 |
48 49
|
syl |
|- ( ph -> ( F ` W ) e. On ) |
51 |
13 12
|
omf1o |
|- ( ( ( _om ^o W ) e. On /\ ( F ` W ) e. On ) -> ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( ( F ` W ) .o ( _om ^o W ) ) ) |
52 |
47 50 51
|
syl2anc |
|- ( ph -> ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( ( F ` W ) .o ( _om ^o W ) ) ) |
53 |
26
|
ffnd |
|- ( ph -> F Fn A ) |
54 |
|
0ex |
|- (/) e. _V |
55 |
54
|
a1i |
|- ( ph -> (/) e. _V ) |
56 |
|
elsuppfn |
|- ( ( F Fn A /\ A e. On /\ (/) e. _V ) -> ( W e. ( F supp (/) ) <-> ( W e. A /\ ( F ` W ) =/= (/) ) ) ) |
57 |
53 2 55 56
|
syl3anc |
|- ( ph -> ( W e. ( F supp (/) ) <-> ( W e. A /\ ( F ` W ) =/= (/) ) ) ) |
58 |
|
simpr |
|- ( ( W e. A /\ ( F ` W ) =/= (/) ) -> ( F ` W ) =/= (/) ) |
59 |
57 58
|
syl6bi |
|- ( ph -> ( W e. ( F supp (/) ) -> ( F ` W ) =/= (/) ) ) |
60 |
42 59
|
mpd |
|- ( ph -> ( F ` W ) =/= (/) ) |
61 |
|
on0eln0 |
|- ( ( F ` W ) e. On -> ( (/) e. ( F ` W ) <-> ( F ` W ) =/= (/) ) ) |
62 |
48 49 61
|
3syl |
|- ( ph -> ( (/) e. ( F ` W ) <-> ( F ` W ) =/= (/) ) ) |
63 |
60 62
|
mpbird |
|- ( ph -> (/) e. ( F ` W ) ) |
64 |
1 2 3 4 5 6 7 8 9 10 11
|
cnfcom3lem |
|- ( ph -> W e. ( On \ 1o ) ) |
65 |
|
ondif1 |
|- ( W e. ( On \ 1o ) <-> ( W e. On /\ (/) e. W ) ) |
66 |
65
|
simprbi |
|- ( W e. ( On \ 1o ) -> (/) e. W ) |
67 |
64 66
|
syl |
|- ( ph -> (/) e. W ) |
68 |
|
omabs |
|- ( ( ( ( F ` W ) e. _om /\ (/) e. ( F ` W ) ) /\ ( W e. On /\ (/) e. W ) ) -> ( ( F ` W ) .o ( _om ^o W ) ) = ( _om ^o W ) ) |
69 |
48 63 45 67 68
|
syl22anc |
|- ( ph -> ( ( F ` W ) .o ( _om ^o W ) ) = ( _om ^o W ) ) |
70 |
69
|
f1oeq3d |
|- ( ph -> ( ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( ( F ` W ) .o ( _om ^o W ) ) <-> ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( _om ^o W ) ) ) |
71 |
52 70
|
mpbid |
|- ( ph -> ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( _om ^o W ) ) |
72 |
1 2 3 4 5 6 7 8 9 10 36
|
cnfcom2 |
|- ( ph -> ( T ` dom G ) : B -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) ) |
73 |
|
f1oco |
|- ( ( ( X o. `' Y ) : ( ( _om ^o W ) .o ( F ` W ) ) -1-1-onto-> ( _om ^o W ) /\ ( T ` dom G ) : B -1-1-onto-> ( ( _om ^o W ) .o ( F ` W ) ) ) -> ( ( X o. `' Y ) o. ( T ` dom G ) ) : B -1-1-onto-> ( _om ^o W ) ) |
74 |
71 72 73
|
syl2anc |
|- ( ph -> ( ( X o. `' Y ) o. ( T ` dom G ) ) : B -1-1-onto-> ( _om ^o W ) ) |
75 |
|
f1oeq1 |
|- ( N = ( ( X o. `' Y ) o. ( T ` dom G ) ) -> ( N : B -1-1-onto-> ( _om ^o W ) <-> ( ( X o. `' Y ) o. ( T ` dom G ) ) : B -1-1-onto-> ( _om ^o W ) ) ) |
76 |
14 75
|
ax-mp |
|- ( N : B -1-1-onto-> ( _om ^o W ) <-> ( ( X o. `' Y ) o. ( T ` dom G ) ) : B -1-1-onto-> ( _om ^o W ) ) |
77 |
74 76
|
sylibr |
|- ( ph -> N : B -1-1-onto-> ( _om ^o W ) ) |