This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑛 ∈ ω ∧ ∀ 𝑘 ∈ suc 𝑛 ( 𝐵 ‘ 𝑘 ) ≈ 𝒫 𝑘 ) → ∪ 𝑘 ∈ 𝑛 ( 𝐵 ‘ 𝑘 ) ≺ ( 𝐵 ‘ 𝑛 ) )

Proof

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