Metamath Proof Explorer

Theorem oelim2

Description: Ordinal exponentiation with a limit exponent. Part of Exercise 4.36 of Mendelson p. 250. (Contributed by NM, 6-Jan-2005)

Ref Expression
Assertion oelim2 ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) )

Proof

Step Hyp Ref Expression
1 limelon ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On )
2 0ellim ⊢ ( Lim 𝐵 → ∅ ∈ 𝐵 )
3 2 adantl ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ∅ ∈ 𝐵 )
4 oe0m1 ⊢ ( 𝐵 ∈ On → ( ∅ ∈ 𝐵 ↔ ( ∅ ↑o 𝐵 ) = ∅ ) )
5 4 biimpa ⊢ ( ( 𝐵 ∈ On ∧ ∅ ∈ 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ )
6 1 3 5 syl2anc ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∅ )
7 eldif ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 1o ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1o ) )
8 limord ⊢ ( Lim 𝐵 → Ord 𝐵 )
9 ordelon ⊢ ( ( Ord 𝐵 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
10 8 9 sylan ⊢ ( ( Lim 𝐵 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
11 on0eln0 ⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ 𝑥 ≠ ∅ ) )
12 el1o ⊢ ( 𝑥 ∈ 1o ↔ 𝑥 = ∅ )
13 12 necon3bbii ⊢ ( ¬ 𝑥 ∈ 1o ↔ 𝑥 ≠ ∅ )
14 11 13 bitr4di ⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ ¬ 𝑥 ∈ 1o ) )
15 oe0m1 ⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 ↔ ( ∅ ↑o 𝑥 ) = ∅ ) )
16 15 biimpd ⊢ ( 𝑥 ∈ On → ( ∅ ∈ 𝑥 → ( ∅ ↑o 𝑥 ) = ∅ ) )
17 14 16 sylbird ⊢ ( 𝑥 ∈ On → ( ¬ 𝑥 ∈ 1o → ( ∅ ↑o 𝑥 ) = ∅ ) )
18 10 17 syl ⊢ ( ( Lim 𝐵 ∧ 𝑥 ∈ 𝐵 ) → ( ¬ 𝑥 ∈ 1o → ( ∅ ↑o 𝑥 ) = ∅ ) )
19 18 impr ⊢ ( ( Lim 𝐵 ∧ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 1o ) ) → ( ∅ ↑o 𝑥 ) = ∅ )
20 7 19 sylan2b ⊢ ( ( Lim 𝐵 ∧ 𝑥 ∈ ( 𝐵 ∖ 1o ) ) → ( ∅ ↑o 𝑥 ) = ∅ )
21 20 iuneq2dv ⊢ ( Lim 𝐵 → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ )
22 df-1o ⊢ 1o = suc ∅
23 limsuc ⊢ ( Lim 𝐵 → ( ∅ ∈ 𝐵 ↔ suc ∅ ∈ 𝐵 ) )
24 2 23 mpbid ⊢ ( Lim 𝐵 → suc ∅ ∈ 𝐵 )
25 22 24 eqeltrid ⊢ ( Lim 𝐵 → 1o ∈ 𝐵 )
26 1on ⊢ 1o ∈ On
27 26 onirri ⊢ ¬ 1o ∈ 1o
28 eldif ⊢ ( 1o ∈ ( 𝐵 ∖ 1o ) ↔ ( 1o ∈ 𝐵 ∧ ¬ 1o ∈ 1o ) )
29 25 27 28 sylanblrc ⊢ ( Lim 𝐵 → 1o ∈ ( 𝐵 ∖ 1o ) )
30 ne0i ⊢ ( 1o ∈ ( 𝐵 ∖ 1o ) → ( 𝐵 ∖ 1o ) ≠ ∅ )
31 iunconst ⊢ ( ( 𝐵 ∖ 1o ) ≠ ∅ → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ = ∅ )
32 29 30 31 3syl ⊢ ( Lim 𝐵 → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ∅ = ∅ )
33 21 32 eqtrd ⊢ ( Lim 𝐵 → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = ∅ )
34 33 adantl ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) = ∅ )
35 6 34 eqtr4d ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( ∅ ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) )
36 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝐵 ) = ( ∅ ↑o 𝐵 ) )
37 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ↑o 𝑥 ) = ( ∅ ↑o 𝑥 ) )
38 37 iuneq2d ⊢ ( 𝐴 = ∅ → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) )
39 36 38 eqeq12d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ↔ ( ∅ ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( ∅ ↑o 𝑥 ) ) )
40 35 39 syl5ibr ⊢ ( 𝐴 = ∅ → ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ) )
41 40 impcom ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝐴 = ∅ ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) )
42 oelim ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) )
43 limsuc ⊢ ( Lim 𝐵 → ( 𝑦 ∈ 𝐵 ↔ suc 𝑦 ∈ 𝐵 ) )
44 43 biimpa ⊢ ( ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) → suc 𝑦 ∈ 𝐵 )
45 nsuceq0 ⊢ suc 𝑦 ≠ ∅
46 dif1o ⊢ ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ↔ ( suc 𝑦 ∈ 𝐵 ∧ suc 𝑦 ≠ ∅ ) )
47 44 45 46 sylanblrc ⊢ ( ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) )
48 47 ex ⊢ ( Lim 𝐵 → ( 𝑦 ∈ 𝐵 → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ) )
49 48 ad2antlr ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ) )
50 sssucid ⊢ 𝑦 ⊆ suc 𝑦
51 ordelon ⊢ ( ( Ord 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ On )
52 8 51 sylan ⊢ ( ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ On )
53 suceloni ⊢ ( 𝑦 ∈ On → suc 𝑦 ∈ On )
54 52 53 jccir ⊢ ( ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) )
55 id ⊢ ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
56 55 3expa ⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) ∧ 𝐴 ∈ On ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
57 56 ancoms ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ) ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
58 54 57 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ ( Lim 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
59 58 anassrs ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) )
60 oewordi ⊢ ( ( ( 𝑦 ∈ On ∧ suc 𝑦 ∈ On ∧ 𝐴 ∈ On ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
61 59 60 sylan ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ 𝑦 ∈ 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
62 61 an32s ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ⊆ suc 𝑦 → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
63 50 62 mpi ⊢ ( ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) )
64 63 ex ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
65 49 64 jcad ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) ) )
66 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o suc 𝑦 ) )
67 66 sseq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) ↔ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) )
68 67 rspcev ⊢ ( ( suc 𝑦 ∈ ( 𝐵 ∖ 1o ) ∧ ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o suc 𝑦 ) ) → ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) )
69 65 68 syl6 ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) ) )
70 69 ralrimiv ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) )
71 iunss2 ⊢ ( ∀ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑦 ) ⊆ ( 𝐴 ↑o 𝑥 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) ⊆ ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) )
72 70 71 syl ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) ⊆ ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) )
73 difss ⊢ ( 𝐵 ∖ 1o ) ⊆ 𝐵
74 iunss1 ⊢ ( ( 𝐵 ∖ 1o ) ⊆ 𝐵 → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) )
75 73 74 ax-mp ⊢ ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 )
76 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ↑o 𝑥 ) = ( 𝐴 ↑o 𝑦 ) )
77 76 cbviunv ⊢ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ↑o 𝑥 ) = ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 )
78 75 77 sseqtri ⊢ ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 )
79 78 a1i ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) ⊆ ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) )
80 72 79 eqssd ⊢ ( ( ( 𝐴 ∈ On ∧ Lim 𝐵 ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) )
81 80 adantlrl ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 ↑o 𝑦 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) )
82 42 81 eqtrd ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) )
83 41 82 oe0lem ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 ↑o 𝐵 ) = ∪ 𝑥 ∈ ( 𝐵 ∖ 1o ) ( 𝐴 ↑o 𝑥 ) )