Step |
Hyp |
Ref |
Expression |
1 |
|
cantnfs.s |
|- S = dom ( A CNF B ) |
2 |
|
cantnfs.a |
|- ( ph -> A e. On ) |
3 |
|
cantnfs.b |
|- ( ph -> B e. On ) |
4 |
|
oemapval.t |
|- T = { <. x , y >. | E. z e. B ( ( x ` z ) e. ( y ` z ) /\ A. w e. B ( z e. w -> ( x ` w ) = ( y ` w ) ) ) } |
5 |
|
oemapval.f |
|- ( ph -> F e. S ) |
6 |
|
oemapval.g |
|- ( ph -> G e. S ) |
7 |
|
oemapvali.r |
|- ( ph -> F T G ) |
8 |
|
oemapvali.x |
|- X = U. { c e. B | ( F ` c ) e. ( G ` c ) } |
9 |
|
cantnflem1.o |
|- O = OrdIso ( _E , ( G supp (/) ) ) |
10 |
|
cantnflem1.h |
|- H = seqom ( ( k e. _V , z e. _V |-> ( ( ( A ^o ( O ` k ) ) .o ( G ` ( O ` k ) ) ) +o z ) ) , (/) ) |
11 |
1 2 3 4 5 6 7 8
|
oemapvali |
|- ( ph -> ( X e. B /\ ( F ` X ) e. ( G ` X ) /\ A. w e. B ( X e. w -> ( F ` w ) = ( G ` w ) ) ) ) |
12 |
11
|
simp1d |
|- ( ph -> X e. B ) |
13 |
|
onelon |
|- ( ( B e. On /\ X e. B ) -> X e. On ) |
14 |
3 12 13
|
syl2anc |
|- ( ph -> X e. On ) |
15 |
|
oecl |
|- ( ( A e. On /\ X e. On ) -> ( A ^o X ) e. On ) |
16 |
2 14 15
|
syl2anc |
|- ( ph -> ( A ^o X ) e. On ) |
17 |
1 2 3
|
cantnfs |
|- ( ph -> ( G e. S <-> ( G : B --> A /\ G finSupp (/) ) ) ) |
18 |
6 17
|
mpbid |
|- ( ph -> ( G : B --> A /\ G finSupp (/) ) ) |
19 |
18
|
simpld |
|- ( ph -> G : B --> A ) |
20 |
19 12
|
ffvelrnd |
|- ( ph -> ( G ` X ) e. A ) |
21 |
|
onelon |
|- ( ( A e. On /\ ( G ` X ) e. A ) -> ( G ` X ) e. On ) |
22 |
2 20 21
|
syl2anc |
|- ( ph -> ( G ` X ) e. On ) |
23 |
|
omcl |
|- ( ( ( A ^o X ) e. On /\ ( G ` X ) e. On ) -> ( ( A ^o X ) .o ( G ` X ) ) e. On ) |
24 |
16 22 23
|
syl2anc |
|- ( ph -> ( ( A ^o X ) .o ( G ` X ) ) e. On ) |
25 |
|
ovexd |
|- ( ph -> ( G supp (/) ) e. _V ) |
26 |
1 2 3 9 6
|
cantnfcl |
|- ( ph -> ( _E We ( G supp (/) ) /\ dom O e. _om ) ) |
27 |
26
|
simpld |
|- ( ph -> _E We ( G supp (/) ) ) |
28 |
9
|
oiiso |
|- ( ( ( G supp (/) ) e. _V /\ _E We ( G supp (/) ) ) -> O Isom _E , _E ( dom O , ( G supp (/) ) ) ) |
29 |
25 27 28
|
syl2anc |
|- ( ph -> O Isom _E , _E ( dom O , ( G supp (/) ) ) ) |
30 |
|
isof1o |
|- ( O Isom _E , _E ( dom O , ( G supp (/) ) ) -> O : dom O -1-1-onto-> ( G supp (/) ) ) |
31 |
29 30
|
syl |
|- ( ph -> O : dom O -1-1-onto-> ( G supp (/) ) ) |
32 |
|
f1ocnv |
|- ( O : dom O -1-1-onto-> ( G supp (/) ) -> `' O : ( G supp (/) ) -1-1-onto-> dom O ) |
33 |
|
f1of |
|- ( `' O : ( G supp (/) ) -1-1-onto-> dom O -> `' O : ( G supp (/) ) --> dom O ) |
34 |
31 32 33
|
3syl |
|- ( ph -> `' O : ( G supp (/) ) --> dom O ) |
35 |
1 2 3 4 5 6 7 8
|
cantnflem1a |
|- ( ph -> X e. ( G supp (/) ) ) |
36 |
34 35
|
ffvelrnd |
|- ( ph -> ( `' O ` X ) e. dom O ) |
37 |
26
|
simprd |
|- ( ph -> dom O e. _om ) |
38 |
|
elnn |
|- ( ( ( `' O ` X ) e. dom O /\ dom O e. _om ) -> ( `' O ` X ) e. _om ) |
39 |
36 37 38
|
syl2anc |
|- ( ph -> ( `' O ` X ) e. _om ) |
40 |
10
|
cantnfvalf |
|- H : _om --> On |
41 |
40
|
ffvelrni |
|- ( ( `' O ` X ) e. _om -> ( H ` ( `' O ` X ) ) e. On ) |
42 |
39 41
|
syl |
|- ( ph -> ( H ` ( `' O ` X ) ) e. On ) |
43 |
|
oaword1 |
|- ( ( ( ( A ^o X ) .o ( G ` X ) ) e. On /\ ( H ` ( `' O ` X ) ) e. On ) -> ( ( A ^o X ) .o ( G ` X ) ) C_ ( ( ( A ^o X ) .o ( G ` X ) ) +o ( H ` ( `' O ` X ) ) ) ) |
44 |
24 42 43
|
syl2anc |
|- ( ph -> ( ( A ^o X ) .o ( G ` X ) ) C_ ( ( ( A ^o X ) .o ( G ` X ) ) +o ( H ` ( `' O ` X ) ) ) ) |
45 |
1 2 3 9 6 10
|
cantnfsuc |
|- ( ( ph /\ ( `' O ` X ) e. _om ) -> ( H ` suc ( `' O ` X ) ) = ( ( ( A ^o ( O ` ( `' O ` X ) ) ) .o ( G ` ( O ` ( `' O ` X ) ) ) ) +o ( H ` ( `' O ` X ) ) ) ) |
46 |
39 45
|
mpdan |
|- ( ph -> ( H ` suc ( `' O ` X ) ) = ( ( ( A ^o ( O ` ( `' O ` X ) ) ) .o ( G ` ( O ` ( `' O ` X ) ) ) ) +o ( H ` ( `' O ` X ) ) ) ) |
47 |
|
f1ocnvfv2 |
|- ( ( O : dom O -1-1-onto-> ( G supp (/) ) /\ X e. ( G supp (/) ) ) -> ( O ` ( `' O ` X ) ) = X ) |
48 |
31 35 47
|
syl2anc |
|- ( ph -> ( O ` ( `' O ` X ) ) = X ) |
49 |
48
|
oveq2d |
|- ( ph -> ( A ^o ( O ` ( `' O ` X ) ) ) = ( A ^o X ) ) |
50 |
48
|
fveq2d |
|- ( ph -> ( G ` ( O ` ( `' O ` X ) ) ) = ( G ` X ) ) |
51 |
49 50
|
oveq12d |
|- ( ph -> ( ( A ^o ( O ` ( `' O ` X ) ) ) .o ( G ` ( O ` ( `' O ` X ) ) ) ) = ( ( A ^o X ) .o ( G ` X ) ) ) |
52 |
51
|
oveq1d |
|- ( ph -> ( ( ( A ^o ( O ` ( `' O ` X ) ) ) .o ( G ` ( O ` ( `' O ` X ) ) ) ) +o ( H ` ( `' O ` X ) ) ) = ( ( ( A ^o X ) .o ( G ` X ) ) +o ( H ` ( `' O ` X ) ) ) ) |
53 |
46 52
|
eqtrd |
|- ( ph -> ( H ` suc ( `' O ` X ) ) = ( ( ( A ^o X ) .o ( G ` X ) ) +o ( H ` ( `' O ` X ) ) ) ) |
54 |
44 53
|
sseqtrrd |
|- ( ph -> ( ( A ^o X ) .o ( G ` X ) ) C_ ( H ` suc ( `' O ` X ) ) ) |
55 |
|
onss |
|- ( B e. On -> B C_ On ) |
56 |
3 55
|
syl |
|- ( ph -> B C_ On ) |
57 |
56
|
sselda |
|- ( ( ph /\ x e. B ) -> x e. On ) |
58 |
14
|
adantr |
|- ( ( ph /\ x e. B ) -> X e. On ) |
59 |
|
onsseleq |
|- ( ( x e. On /\ X e. On ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) ) |
60 |
57 58 59
|
syl2anc |
|- ( ( ph /\ x e. B ) -> ( x C_ X <-> ( x e. X \/ x = X ) ) ) |
61 |
|
orcom |
|- ( ( x e. X \/ x = X ) <-> ( x = X \/ x e. X ) ) |
62 |
60 61
|
bitrdi |
|- ( ( ph /\ x e. B ) -> ( x C_ X <-> ( x = X \/ x e. X ) ) ) |
63 |
62
|
ifbid |
|- ( ( ph /\ x e. B ) -> if ( x C_ X , ( F ` x ) , (/) ) = if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) |
64 |
63
|
mpteq2dva |
|- ( ph -> ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) ) |
65 |
64
|
fveq2d |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) = ( ( A CNF B ) ` ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) ) ) |
66 |
1 2 3
|
cantnfs |
|- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) ) |
67 |
5 66
|
mpbid |
|- ( ph -> ( F : B --> A /\ F finSupp (/) ) ) |
68 |
67
|
simpld |
|- ( ph -> F : B --> A ) |
69 |
68
|
ffvelrnda |
|- ( ( ph /\ y e. B ) -> ( F ` y ) e. A ) |
70 |
20
|
ne0d |
|- ( ph -> A =/= (/) ) |
71 |
|
on0eln0 |
|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) ) |
72 |
2 71
|
syl |
|- ( ph -> ( (/) e. A <-> A =/= (/) ) ) |
73 |
70 72
|
mpbird |
|- ( ph -> (/) e. A ) |
74 |
73
|
adantr |
|- ( ( ph /\ y e. B ) -> (/) e. A ) |
75 |
69 74
|
ifcld |
|- ( ( ph /\ y e. B ) -> if ( y e. X , ( F ` y ) , (/) ) e. A ) |
76 |
75
|
fmpttd |
|- ( ph -> ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) : B --> A ) |
77 |
|
0ex |
|- (/) e. _V |
78 |
77
|
a1i |
|- ( ph -> (/) e. _V ) |
79 |
67
|
simprd |
|- ( ph -> F finSupp (/) ) |
80 |
68 3 78 79
|
fsuppmptif |
|- ( ph -> ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) finSupp (/) ) |
81 |
1 2 3
|
cantnfs |
|- ( ph -> ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) e. S <-> ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) : B --> A /\ ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) finSupp (/) ) ) ) |
82 |
76 80 81
|
mpbir2and |
|- ( ph -> ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) e. S ) |
83 |
68 12
|
ffvelrnd |
|- ( ph -> ( F ` X ) e. A ) |
84 |
|
eldifn |
|- ( y e. ( B \ X ) -> -. y e. X ) |
85 |
84
|
adantl |
|- ( ( ph /\ y e. ( B \ X ) ) -> -. y e. X ) |
86 |
85
|
iffalsed |
|- ( ( ph /\ y e. ( B \ X ) ) -> if ( y e. X , ( F ` y ) , (/) ) = (/) ) |
87 |
86 3
|
suppss2 |
|- ( ph -> ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) supp (/) ) C_ X ) |
88 |
|
ifor |
|- if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) = if ( x = X , ( F ` x ) , if ( x e. X , ( F ` x ) , (/) ) ) |
89 |
|
fveq2 |
|- ( x = X -> ( F ` x ) = ( F ` X ) ) |
90 |
89
|
adantl |
|- ( ( x e. B /\ x = X ) -> ( F ` x ) = ( F ` X ) ) |
91 |
90
|
ifeq1da |
|- ( x e. B -> if ( x = X , ( F ` x ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) = if ( x = X , ( F ` X ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) ) |
92 |
|
eleq1w |
|- ( y = x -> ( y e. X <-> x e. X ) ) |
93 |
|
fveq2 |
|- ( y = x -> ( F ` y ) = ( F ` x ) ) |
94 |
92 93
|
ifbieq1d |
|- ( y = x -> if ( y e. X , ( F ` y ) , (/) ) = if ( x e. X , ( F ` x ) , (/) ) ) |
95 |
|
eqid |
|- ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) = ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) |
96 |
|
fvex |
|- ( F ` x ) e. _V |
97 |
96 77
|
ifex |
|- if ( x e. X , ( F ` x ) , (/) ) e. _V |
98 |
94 95 97
|
fvmpt |
|- ( x e. B -> ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) = if ( x e. X , ( F ` x ) , (/) ) ) |
99 |
98
|
ifeq2d |
|- ( x e. B -> if ( x = X , ( F ` x ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) = if ( x = X , ( F ` x ) , if ( x e. X , ( F ` x ) , (/) ) ) ) |
100 |
91 99
|
eqtr3d |
|- ( x e. B -> if ( x = X , ( F ` X ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) = if ( x = X , ( F ` x ) , if ( x e. X , ( F ` x ) , (/) ) ) ) |
101 |
88 100
|
eqtr4id |
|- ( x e. B -> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) = if ( x = X , ( F ` X ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) ) |
102 |
101
|
mpteq2ia |
|- ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) = ( x e. B |-> if ( x = X , ( F ` X ) , ( ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ` x ) ) ) |
103 |
1 2 3 82 12 83 87 102
|
cantnfp1 |
|- ( ph -> ( ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) e. S /\ ( ( A CNF B ) ` ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) ) ) |
104 |
103
|
simprd |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( ( x = X \/ x e. X ) , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) ) |
105 |
65 104
|
eqtrd |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) ) |
106 |
|
onelon |
|- ( ( A e. On /\ ( F ` X ) e. A ) -> ( F ` X ) e. On ) |
107 |
2 83 106
|
syl2anc |
|- ( ph -> ( F ` X ) e. On ) |
108 |
|
omsuc |
|- ( ( ( A ^o X ) e. On /\ ( F ` X ) e. On ) -> ( ( A ^o X ) .o suc ( F ` X ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) ) |
109 |
16 107 108
|
syl2anc |
|- ( ph -> ( ( A ^o X ) .o suc ( F ` X ) ) = ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) ) |
110 |
|
eloni |
|- ( ( G ` X ) e. On -> Ord ( G ` X ) ) |
111 |
22 110
|
syl |
|- ( ph -> Ord ( G ` X ) ) |
112 |
11
|
simp2d |
|- ( ph -> ( F ` X ) e. ( G ` X ) ) |
113 |
|
ordsucss |
|- ( Ord ( G ` X ) -> ( ( F ` X ) e. ( G ` X ) -> suc ( F ` X ) C_ ( G ` X ) ) ) |
114 |
111 112 113
|
sylc |
|- ( ph -> suc ( F ` X ) C_ ( G ` X ) ) |
115 |
|
suceloni |
|- ( ( F ` X ) e. On -> suc ( F ` X ) e. On ) |
116 |
107 115
|
syl |
|- ( ph -> suc ( F ` X ) e. On ) |
117 |
|
omwordi |
|- ( ( suc ( F ` X ) e. On /\ ( G ` X ) e. On /\ ( A ^o X ) e. On ) -> ( suc ( F ` X ) C_ ( G ` X ) -> ( ( A ^o X ) .o suc ( F ` X ) ) C_ ( ( A ^o X ) .o ( G ` X ) ) ) ) |
118 |
116 22 16 117
|
syl3anc |
|- ( ph -> ( suc ( F ` X ) C_ ( G ` X ) -> ( ( A ^o X ) .o suc ( F ` X ) ) C_ ( ( A ^o X ) .o ( G ` X ) ) ) ) |
119 |
114 118
|
mpd |
|- ( ph -> ( ( A ^o X ) .o suc ( F ` X ) ) C_ ( ( A ^o X ) .o ( G ` X ) ) ) |
120 |
109 119
|
eqsstrrd |
|- ( ph -> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) C_ ( ( A ^o X ) .o ( G ` X ) ) ) |
121 |
1 2 3 82 73 14 87
|
cantnflt2 |
|- ( ph -> ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. ( A ^o X ) ) |
122 |
|
onelon |
|- ( ( ( A ^o X ) e. On /\ ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. ( A ^o X ) ) -> ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. On ) |
123 |
16 121 122
|
syl2anc |
|- ( ph -> ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. On ) |
124 |
|
omcl |
|- ( ( ( A ^o X ) e. On /\ ( F ` X ) e. On ) -> ( ( A ^o X ) .o ( F ` X ) ) e. On ) |
125 |
16 107 124
|
syl2anc |
|- ( ph -> ( ( A ^o X ) .o ( F ` X ) ) e. On ) |
126 |
|
oaord |
|- ( ( ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. On /\ ( A ^o X ) e. On /\ ( ( A ^o X ) .o ( F ` X ) ) e. On ) -> ( ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. ( A ^o X ) <-> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) e. ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) ) ) |
127 |
123 16 125 126
|
syl3anc |
|- ( ph -> ( ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) e. ( A ^o X ) <-> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) e. ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) ) ) |
128 |
121 127
|
mpbid |
|- ( ph -> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) e. ( ( ( A ^o X ) .o ( F ` X ) ) +o ( A ^o X ) ) ) |
129 |
120 128
|
sseldd |
|- ( ph -> ( ( ( A ^o X ) .o ( F ` X ) ) +o ( ( A CNF B ) ` ( y e. B |-> if ( y e. X , ( F ` y ) , (/) ) ) ) ) e. ( ( A ^o X ) .o ( G ` X ) ) ) |
130 |
105 129
|
eqeltrd |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( ( A ^o X ) .o ( G ` X ) ) ) |
131 |
54 130
|
sseldd |
|- ( ph -> ( ( A CNF B ) ` ( x e. B |-> if ( x C_ X , ( F ` x ) , (/) ) ) ) e. ( H ` suc ( `' O ` X ) ) ) |