Step |
Hyp |
Ref |
Expression |
1 |
|
suceq |
|- ( n = (/) -> suc n = suc (/) ) |
2 |
1
|
raleqdv |
|- ( n = (/) -> ( A. k e. suc n ( B ` k ) ~~ ~P k <-> A. k e. suc (/) ( B ` k ) ~~ ~P k ) ) |
3 |
|
iuneq1 |
|- ( n = (/) -> U_ k e. n ( B ` k ) = U_ k e. (/) ( B ` k ) ) |
4 |
|
fveq2 |
|- ( n = (/) -> ( B ` n ) = ( B ` (/) ) ) |
5 |
3 4
|
breq12d |
|- ( n = (/) -> ( U_ k e. n ( B ` k ) ~< ( B ` n ) <-> U_ k e. (/) ( B ` k ) ~< ( B ` (/) ) ) ) |
6 |
2 5
|
imbi12d |
|- ( n = (/) -> ( ( A. k e. suc n ( B ` k ) ~~ ~P k -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) <-> ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> U_ k e. (/) ( B ` k ) ~< ( B ` (/) ) ) ) ) |
7 |
|
suceq |
|- ( n = m -> suc n = suc m ) |
8 |
7
|
raleqdv |
|- ( n = m -> ( A. k e. suc n ( B ` k ) ~~ ~P k <-> A. k e. suc m ( B ` k ) ~~ ~P k ) ) |
9 |
|
iuneq1 |
|- ( n = m -> U_ k e. n ( B ` k ) = U_ k e. m ( B ` k ) ) |
10 |
|
fveq2 |
|- ( n = m -> ( B ` n ) = ( B ` m ) ) |
11 |
9 10
|
breq12d |
|- ( n = m -> ( U_ k e. n ( B ` k ) ~< ( B ` n ) <-> U_ k e. m ( B ` k ) ~< ( B ` m ) ) ) |
12 |
8 11
|
imbi12d |
|- ( n = m -> ( ( A. k e. suc n ( B ` k ) ~~ ~P k -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) <-> ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) ) ) |
13 |
|
suceq |
|- ( n = suc m -> suc n = suc suc m ) |
14 |
13
|
raleqdv |
|- ( n = suc m -> ( A. k e. suc n ( B ` k ) ~~ ~P k <-> A. k e. suc suc m ( B ` k ) ~~ ~P k ) ) |
15 |
|
iuneq1 |
|- ( n = suc m -> U_ k e. n ( B ` k ) = U_ k e. suc m ( B ` k ) ) |
16 |
|
fveq2 |
|- ( n = suc m -> ( B ` n ) = ( B ` suc m ) ) |
17 |
15 16
|
breq12d |
|- ( n = suc m -> ( U_ k e. n ( B ` k ) ~< ( B ` n ) <-> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) |
18 |
14 17
|
imbi12d |
|- ( n = suc m -> ( ( A. k e. suc n ( B ` k ) ~~ ~P k -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) <-> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) ) |
19 |
|
0iun |
|- U_ k e. (/) ( B ` k ) = (/) |
20 |
|
0ex |
|- (/) e. _V |
21 |
20
|
sucid |
|- (/) e. suc (/) |
22 |
|
fveq2 |
|- ( k = (/) -> ( B ` k ) = ( B ` (/) ) ) |
23 |
|
pweq |
|- ( k = (/) -> ~P k = ~P (/) ) |
24 |
22 23
|
breq12d |
|- ( k = (/) -> ( ( B ` k ) ~~ ~P k <-> ( B ` (/) ) ~~ ~P (/) ) ) |
25 |
24
|
rspcv |
|- ( (/) e. suc (/) -> ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> ( B ` (/) ) ~~ ~P (/) ) ) |
26 |
21 25
|
ax-mp |
|- ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> ( B ` (/) ) ~~ ~P (/) ) |
27 |
20
|
canth2 |
|- (/) ~< ~P (/) |
28 |
|
ensym |
|- ( ( B ` (/) ) ~~ ~P (/) -> ~P (/) ~~ ( B ` (/) ) ) |
29 |
|
sdomentr |
|- ( ( (/) ~< ~P (/) /\ ~P (/) ~~ ( B ` (/) ) ) -> (/) ~< ( B ` (/) ) ) |
30 |
27 28 29
|
sylancr |
|- ( ( B ` (/) ) ~~ ~P (/) -> (/) ~< ( B ` (/) ) ) |
31 |
26 30
|
syl |
|- ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> (/) ~< ( B ` (/) ) ) |
32 |
19 31
|
eqbrtrid |
|- ( A. k e. suc (/) ( B ` k ) ~~ ~P k -> U_ k e. (/) ( B ` k ) ~< ( B ` (/) ) ) |
33 |
|
sssucid |
|- suc m C_ suc suc m |
34 |
|
ssralv |
|- ( suc m C_ suc suc m -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> A. k e. suc m ( B ` k ) ~~ ~P k ) ) |
35 |
33 34
|
ax-mp |
|- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> A. k e. suc m ( B ` k ) ~~ ~P k ) |
36 |
|
pm2.27 |
|- ( A. k e. suc m ( B ` k ) ~~ ~P k -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) ) |
37 |
35 36
|
syl |
|- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) ) |
38 |
37
|
adantl |
|- ( ( m e. _om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) ) |
39 |
|
vex |
|- m e. _V |
40 |
39
|
sucid |
|- m e. suc m |
41 |
|
elelsuc |
|- ( m e. suc m -> m e. suc suc m ) |
42 |
|
fveq2 |
|- ( k = m -> ( B ` k ) = ( B ` m ) ) |
43 |
|
pweq |
|- ( k = m -> ~P k = ~P m ) |
44 |
42 43
|
breq12d |
|- ( k = m -> ( ( B ` k ) ~~ ~P k <-> ( B ` m ) ~~ ~P m ) ) |
45 |
44
|
rspcv |
|- ( m e. suc suc m -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( B ` m ) ~~ ~P m ) ) |
46 |
40 41 45
|
mp2b |
|- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( B ` m ) ~~ ~P m ) |
47 |
|
djuen |
|- ( ( ( B ` m ) ~~ ~P m /\ ( B ` m ) ~~ ~P m ) -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ( ~P m |_| ~P m ) ) |
48 |
46 46 47
|
syl2anc |
|- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ( ~P m |_| ~P m ) ) |
49 |
|
pwdju1 |
|- ( m e. _om -> ( ~P m |_| ~P m ) ~~ ~P ( m |_| 1o ) ) |
50 |
|
nnord |
|- ( m e. _om -> Ord m ) |
51 |
|
ordirr |
|- ( Ord m -> -. m e. m ) |
52 |
50 51
|
syl |
|- ( m e. _om -> -. m e. m ) |
53 |
|
dju1en |
|- ( ( m e. _om /\ -. m e. m ) -> ( m |_| 1o ) ~~ suc m ) |
54 |
52 53
|
mpdan |
|- ( m e. _om -> ( m |_| 1o ) ~~ suc m ) |
55 |
|
pwen |
|- ( ( m |_| 1o ) ~~ suc m -> ~P ( m |_| 1o ) ~~ ~P suc m ) |
56 |
54 55
|
syl |
|- ( m e. _om -> ~P ( m |_| 1o ) ~~ ~P suc m ) |
57 |
|
entr |
|- ( ( ( ~P m |_| ~P m ) ~~ ~P ( m |_| 1o ) /\ ~P ( m |_| 1o ) ~~ ~P suc m ) -> ( ~P m |_| ~P m ) ~~ ~P suc m ) |
58 |
49 56 57
|
syl2anc |
|- ( m e. _om -> ( ~P m |_| ~P m ) ~~ ~P suc m ) |
59 |
|
entr |
|- ( ( ( ( B ` m ) |_| ( B ` m ) ) ~~ ( ~P m |_| ~P m ) /\ ( ~P m |_| ~P m ) ~~ ~P suc m ) -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ~P suc m ) |
60 |
48 58 59
|
syl2an |
|- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. _om ) -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ~P suc m ) |
61 |
39
|
sucex |
|- suc m e. _V |
62 |
61
|
sucid |
|- suc m e. suc suc m |
63 |
|
fveq2 |
|- ( k = suc m -> ( B ` k ) = ( B ` suc m ) ) |
64 |
|
pweq |
|- ( k = suc m -> ~P k = ~P suc m ) |
65 |
63 64
|
breq12d |
|- ( k = suc m -> ( ( B ` k ) ~~ ~P k <-> ( B ` suc m ) ~~ ~P suc m ) ) |
66 |
65
|
rspcv |
|- ( suc m e. suc suc m -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( B ` suc m ) ~~ ~P suc m ) ) |
67 |
62 66
|
ax-mp |
|- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( B ` suc m ) ~~ ~P suc m ) |
68 |
67
|
ensymd |
|- ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ~P suc m ~~ ( B ` suc m ) ) |
69 |
68
|
adantr |
|- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. _om ) -> ~P suc m ~~ ( B ` suc m ) ) |
70 |
|
entr |
|- ( ( ( ( B ` m ) |_| ( B ` m ) ) ~~ ~P suc m /\ ~P suc m ~~ ( B ` suc m ) ) -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ( B ` suc m ) ) |
71 |
60 69 70
|
syl2anc |
|- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. _om ) -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ( B ` suc m ) ) |
72 |
71
|
ancoms |
|- ( ( m e. _om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ( B ` suc m ) ) |
73 |
|
nnfi |
|- ( m e. _om -> m e. Fin ) |
74 |
|
pwfi |
|- ( m e. Fin <-> ~P m e. Fin ) |
75 |
|
isfinite |
|- ( ~P m e. Fin <-> ~P m ~< _om ) |
76 |
74 75
|
bitri |
|- ( m e. Fin <-> ~P m ~< _om ) |
77 |
73 76
|
sylib |
|- ( m e. _om -> ~P m ~< _om ) |
78 |
|
ensdomtr |
|- ( ( ( B ` m ) ~~ ~P m /\ ~P m ~< _om ) -> ( B ` m ) ~< _om ) |
79 |
46 77 78
|
syl2an |
|- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. _om ) -> ( B ` m ) ~< _om ) |
80 |
|
isfinite |
|- ( ( B ` m ) e. Fin <-> ( B ` m ) ~< _om ) |
81 |
79 80
|
sylibr |
|- ( ( A. k e. suc suc m ( B ` k ) ~~ ~P k /\ m e. _om ) -> ( B ` m ) e. Fin ) |
82 |
81
|
ancoms |
|- ( ( m e. _om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( B ` m ) e. Fin ) |
83 |
39 42
|
iunsuc |
|- U_ k e. suc m ( B ` k ) = ( U_ k e. m ( B ` k ) u. ( B ` m ) ) |
84 |
|
fvex |
|- ( B ` k ) e. _V |
85 |
39 84
|
iunex |
|- U_ k e. m ( B ` k ) e. _V |
86 |
|
fvex |
|- ( B ` m ) e. _V |
87 |
|
undjudom |
|- ( ( U_ k e. m ( B ` k ) e. _V /\ ( B ` m ) e. _V ) -> ( U_ k e. m ( B ` k ) u. ( B ` m ) ) ~<_ ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ) |
88 |
85 86 87
|
mp2an |
|- ( U_ k e. m ( B ` k ) u. ( B ` m ) ) ~<_ ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) |
89 |
83 88
|
eqbrtri |
|- U_ k e. suc m ( B ` k ) ~<_ ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) |
90 |
|
sdomtr |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) ~< _om ) -> U_ k e. m ( B ` k ) ~< _om ) |
91 |
80 90
|
sylan2b |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. m ( B ` k ) ~< _om ) |
92 |
|
isfinite |
|- ( U_ k e. m ( B ` k ) e. Fin <-> U_ k e. m ( B ` k ) ~< _om ) |
93 |
91 92
|
sylibr |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. m ( B ` k ) e. Fin ) |
94 |
|
finnum |
|- ( U_ k e. m ( B ` k ) e. Fin -> U_ k e. m ( B ` k ) e. dom card ) |
95 |
93 94
|
syl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. m ( B ` k ) e. dom card ) |
96 |
|
finnum |
|- ( ( B ` m ) e. Fin -> ( B ` m ) e. dom card ) |
97 |
96
|
adantl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( B ` m ) e. dom card ) |
98 |
|
cardadju |
|- ( ( U_ k e. m ( B ` k ) e. dom card /\ ( B ` m ) e. dom card ) -> ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~~ ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) ) |
99 |
95 97 98
|
syl2anc |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~~ ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) ) |
100 |
|
ficardom |
|- ( U_ k e. m ( B ` k ) e. Fin -> ( card ` U_ k e. m ( B ` k ) ) e. _om ) |
101 |
93 100
|
syl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` U_ k e. m ( B ` k ) ) e. _om ) |
102 |
|
ficardom |
|- ( ( B ` m ) e. Fin -> ( card ` ( B ` m ) ) e. _om ) |
103 |
102
|
adantl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` ( B ` m ) ) e. _om ) |
104 |
|
cardid2 |
|- ( U_ k e. m ( B ` k ) e. dom card -> ( card ` U_ k e. m ( B ` k ) ) ~~ U_ k e. m ( B ` k ) ) |
105 |
93 94 104
|
3syl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` U_ k e. m ( B ` k ) ) ~~ U_ k e. m ( B ` k ) ) |
106 |
|
simpl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) |
107 |
|
cardid2 |
|- ( ( B ` m ) e. dom card -> ( card ` ( B ` m ) ) ~~ ( B ` m ) ) |
108 |
|
ensym |
|- ( ( card ` ( B ` m ) ) ~~ ( B ` m ) -> ( B ` m ) ~~ ( card ` ( B ` m ) ) ) |
109 |
96 107 108
|
3syl |
|- ( ( B ` m ) e. Fin -> ( B ` m ) ~~ ( card ` ( B ` m ) ) ) |
110 |
109
|
adantl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( B ` m ) ~~ ( card ` ( B ` m ) ) ) |
111 |
|
ensdomtr |
|- ( ( ( card ` U_ k e. m ( B ` k ) ) ~~ U_ k e. m ( B ` k ) /\ U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> ( card ` U_ k e. m ( B ` k ) ) ~< ( B ` m ) ) |
112 |
|
sdomentr |
|- ( ( ( card ` U_ k e. m ( B ` k ) ) ~< ( B ` m ) /\ ( B ` m ) ~~ ( card ` ( B ` m ) ) ) -> ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) ) |
113 |
111 112
|
sylan |
|- ( ( ( ( card ` U_ k e. m ( B ` k ) ) ~~ U_ k e. m ( B ` k ) /\ U_ k e. m ( B ` k ) ~< ( B ` m ) ) /\ ( B ` m ) ~~ ( card ` ( B ` m ) ) ) -> ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) ) |
114 |
105 106 110 113
|
syl21anc |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) ) |
115 |
|
cardon |
|- ( card ` U_ k e. m ( B ` k ) ) e. On |
116 |
|
cardon |
|- ( card ` ( B ` m ) ) e. On |
117 |
|
onenon |
|- ( ( card ` ( B ` m ) ) e. On -> ( card ` ( B ` m ) ) e. dom card ) |
118 |
116 117
|
ax-mp |
|- ( card ` ( B ` m ) ) e. dom card |
119 |
|
cardsdomel |
|- ( ( ( card ` U_ k e. m ( B ` k ) ) e. On /\ ( card ` ( B ` m ) ) e. dom card ) -> ( ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) <-> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( card ` ( B ` m ) ) ) ) ) |
120 |
115 118 119
|
mp2an |
|- ( ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) <-> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( card ` ( B ` m ) ) ) ) |
121 |
|
cardidm |
|- ( card ` ( card ` ( B ` m ) ) ) = ( card ` ( B ` m ) ) |
122 |
121
|
eleq2i |
|- ( ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( card ` ( B ` m ) ) ) <-> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) ) |
123 |
120 122
|
bitri |
|- ( ( card ` U_ k e. m ( B ` k ) ) ~< ( card ` ( B ` m ) ) <-> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) ) |
124 |
114 123
|
sylib |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) ) |
125 |
|
nnaordr |
|- ( ( ( card ` U_ k e. m ( B ` k ) ) e. _om /\ ( card ` ( B ` m ) ) e. _om /\ ( card ` ( B ` m ) ) e. _om ) -> ( ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) <-> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) ) |
126 |
125
|
biimpa |
|- ( ( ( ( card ` U_ k e. m ( B ` k ) ) e. _om /\ ( card ` ( B ` m ) ) e. _om /\ ( card ` ( B ` m ) ) e. _om ) /\ ( card ` U_ k e. m ( B ` k ) ) e. ( card ` ( B ` m ) ) ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
127 |
101 103 103 124 126
|
syl31anc |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
128 |
|
nnacl |
|- ( ( ( card ` ( B ` m ) ) e. _om /\ ( card ` ( B ` m ) ) e. _om ) -> ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) e. _om ) |
129 |
102 102 128
|
syl2anc |
|- ( ( B ` m ) e. Fin -> ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) e. _om ) |
130 |
|
cardnn |
|- ( ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) e. _om -> ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) = ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
131 |
129 130
|
syl |
|- ( ( B ` m ) e. Fin -> ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) = ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
132 |
131
|
adantl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) = ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
133 |
127 132
|
eleqtrrd |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) ) |
134 |
|
cardsdomelir |
|- ( ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) e. ( card ` ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
135 |
133 134
|
syl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
136 |
|
ensdomtr |
|- ( ( ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~~ ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) /\ ( ( card ` U_ k e. m ( B ` k ) ) +o ( card ` ( B ` m ) ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) -> ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
137 |
99 135 136
|
syl2anc |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
138 |
|
cardadju |
|- ( ( ( B ` m ) e. dom card /\ ( B ` m ) e. dom card ) -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
139 |
96 96 138
|
syl2anc |
|- ( ( B ` m ) e. Fin -> ( ( B ` m ) |_| ( B ` m ) ) ~~ ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ) |
140 |
139
|
ensymd |
|- ( ( B ` m ) e. Fin -> ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ~~ ( ( B ` m ) |_| ( B ` m ) ) ) |
141 |
140
|
adantl |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ~~ ( ( B ` m ) |_| ( B ` m ) ) ) |
142 |
|
sdomentr |
|- ( ( ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~< ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) /\ ( ( card ` ( B ` m ) ) +o ( card ` ( B ` m ) ) ) ~~ ( ( B ` m ) |_| ( B ` m ) ) ) -> ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~< ( ( B ` m ) |_| ( B ` m ) ) ) |
143 |
137 141 142
|
syl2anc |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~< ( ( B ` m ) |_| ( B ` m ) ) ) |
144 |
|
domsdomtr |
|- ( ( U_ k e. suc m ( B ` k ) ~<_ ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) /\ ( U_ k e. m ( B ` k ) |_| ( B ` m ) ) ~< ( ( B ` m ) |_| ( B ` m ) ) ) -> U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) |_| ( B ` m ) ) ) |
145 |
89 143 144
|
sylancr |
|- ( ( U_ k e. m ( B ` k ) ~< ( B ` m ) /\ ( B ` m ) e. Fin ) -> U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) |_| ( B ` m ) ) ) |
146 |
145
|
expcom |
|- ( ( B ` m ) e. Fin -> ( U_ k e. m ( B ` k ) ~< ( B ` m ) -> U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) |_| ( B ` m ) ) ) ) |
147 |
82 146
|
syl |
|- ( ( m e. _om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( U_ k e. m ( B ` k ) ~< ( B ` m ) -> U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) |_| ( B ` m ) ) ) ) |
148 |
|
sdomentr |
|- ( ( U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) |_| ( B ` m ) ) /\ ( ( B ` m ) |_| ( B ` m ) ) ~~ ( B ` suc m ) ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) |
149 |
148
|
expcom |
|- ( ( ( B ` m ) |_| ( B ` m ) ) ~~ ( B ` suc m ) -> ( U_ k e. suc m ( B ` k ) ~< ( ( B ` m ) |_| ( B ` m ) ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) |
150 |
72 147 149
|
sylsyld |
|- ( ( m e. _om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( U_ k e. m ( B ` k ) ~< ( B ` m ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) |
151 |
38 150
|
syld |
|- ( ( m e. _om /\ A. k e. suc suc m ( B ` k ) ~~ ~P k ) -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) |
152 |
151
|
ex |
|- ( m e. _om -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) ) |
153 |
152
|
com23 |
|- ( m e. _om -> ( ( A. k e. suc m ( B ` k ) ~~ ~P k -> U_ k e. m ( B ` k ) ~< ( B ` m ) ) -> ( A. k e. suc suc m ( B ` k ) ~~ ~P k -> U_ k e. suc m ( B ` k ) ~< ( B ` suc m ) ) ) ) |
154 |
6 12 18 32 153
|
finds1 |
|- ( n e. _om -> ( A. k e. suc n ( B ` k ) ~~ ~P k -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) ) |
155 |
154
|
imp |
|- ( ( n e. _om /\ A. k e. suc n ( B ` k ) ~~ ~P k ) -> U_ k e. n ( B ` k ) ~< ( B ` n ) ) |