Metamath Proof Explorer

Theorem pwsdompw

Description: Lemma for domtriom . This is the equinumerosity version of the algebraic identity sum_ k e. n ( 2 ^ k ) = ( 2 ^ n ) - 1 . (Contributed by Mario Carneiro, 7-Feb-2013)

Ref Expression
Assertion pwsdompw 
|- ( ( n e. _om /\ A. k e. suc n ( B ` k ) ~~ ~P k ) -> U_ k e. n ( B ` k ) ~< ( B ` n ) )

Proof

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