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