Metamath Proof Explorer

Theorem oalimcl

Description: The ordinal sum with a limit ordinal is a limit ordinal. Proposition 8.11 of TakeutiZaring p. 60. (Contributed by NM, 8-Dec-2004)

Ref Expression
Assertion oalimcl ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → Lim ( 𝐴 +o 𝐵 ) )

Proof

Step Hyp Ref Expression
1 limelon ⊢ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → 𝐵 ∈ On )
2 oacl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )
3 eloni ⊢ ( ( 𝐴 +o 𝐵 ) ∈ On → Ord ( 𝐴 +o 𝐵 ) )
4 2 3 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord ( 𝐴 +o 𝐵 ) )
5 1 4 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → Ord ( 𝐴 +o 𝐵 ) )
6 0ellim ⊢ ( Lim 𝐵 → ∅ ∈ 𝐵 )
7 n0i ⊢ ( ∅ ∈ 𝐵 → ¬ 𝐵 = ∅ )
8 6 7 syl ⊢ ( Lim 𝐵 → ¬ 𝐵 = ∅ )
9 8 ad2antll ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ¬ 𝐵 = ∅ )
10 oa00 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = ∅ ↔ ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) ) )
11 simpr ⊢ ( ( 𝐴 = ∅ ∧ 𝐵 = ∅ ) → 𝐵 = ∅ )
12 10 11 syl6bi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) = ∅ → 𝐵 = ∅ ) )
13 12 con3d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ 𝐵 = ∅ → ¬ ( 𝐴 +o 𝐵 ) = ∅ ) )
14 1 13 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( ¬ 𝐵 = ∅ → ¬ ( 𝐴 +o 𝐵 ) = ∅ ) )
15 9 14 mpd ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ¬ ( 𝐴 +o 𝐵 ) = ∅ )
16 vex ⊢ 𝑦 ∈ V
17 16 sucid ⊢ 𝑦 ∈ suc 𝑦
18 oalim ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝐴 +o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 +o 𝑥 ) )
19 eqeq1 ⊢ ( ( 𝐴 +o 𝐵 ) = suc 𝑦 → ( ( 𝐴 +o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 +o 𝑥 ) ↔ suc 𝑦 = ∪ 𝑥 ∈ 𝐵 ( 𝐴 +o 𝑥 ) ) )
20 18 19 syl5ib ⊢ ( ( 𝐴 +o 𝐵 ) = suc 𝑦 → ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → suc 𝑦 = ∪ 𝑥 ∈ 𝐵 ( 𝐴 +o 𝑥 ) ) )
21 20 imp ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ) → suc 𝑦 = ∪ 𝑥 ∈ 𝐵 ( 𝐴 +o 𝑥 ) )
22 17 21 eleqtrid ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ) → 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 ( 𝐴 +o 𝑥 ) )
23 eliun ⊢ ( 𝑦 ∈ ∪ 𝑥 ∈ 𝐵 ( 𝐴 +o 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 +o 𝑥 ) )
24 22 23 sylib ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ) → ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 +o 𝑥 ) )
25 onelon ⊢ ( ( 𝐵 ∈ On ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
26 1 25 sylan ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ On )
27 onnbtwn ⊢ ( 𝑥 ∈ On → ¬ ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝑥 ) )
28 imnan ⊢ ( ( 𝑥 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝑥 ) ↔ ¬ ( 𝑥 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝑥 ) )
29 27 28 sylibr ⊢ ( 𝑥 ∈ On → ( 𝑥 ∈ 𝐵 → ¬ 𝐵 ∈ suc 𝑥 ) )
30 29 com12 ⊢ ( 𝑥 ∈ 𝐵 → ( 𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥 ) )
31 30 adantl ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ On → ¬ 𝐵 ∈ suc 𝑥 ) )
32 26 31 mpd ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝐵 ∈ suc 𝑥 )
33 32 ad2antrl ⊢ ( ( 𝐴 ∈ On ∧ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 +o 𝑥 ) ) ) → ¬ 𝐵 ∈ suc 𝑥 )
34 oacl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 +o 𝑥 ) ∈ On )
35 eloni ⊢ ( ( 𝐴 +o 𝑥 ) ∈ On → Ord ( 𝐴 +o 𝑥 ) )
36 ordsucelsuc ⊢ ( Ord ( 𝐴 +o 𝑥 ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) ↔ suc 𝑦 ∈ suc ( 𝐴 +o 𝑥 ) ) )
37 34 35 36 3syl ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) ↔ suc 𝑦 ∈ suc ( 𝐴 +o 𝑥 ) ) )
38 oasuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝐴 +o suc 𝑥 ) = suc ( 𝐴 +o 𝑥 ) )
39 38 eleq2d ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( suc 𝑦 ∈ ( 𝐴 +o suc 𝑥 ) ↔ suc 𝑦 ∈ suc ( 𝐴 +o 𝑥 ) ) )
40 37 39 bitr4d ⊢ ( ( 𝐴 ∈ On ∧ 𝑥 ∈ On ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) ↔ suc 𝑦 ∈ ( 𝐴 +o suc 𝑥 ) ) )
41 26 40 sylan2 ⊢ ( ( 𝐴 ∈ On ∧ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) ↔ suc 𝑦 ∈ ( 𝐴 +o suc 𝑥 ) ) )
42 eleq1 ⊢ ( ( 𝐴 +o 𝐵 ) = suc 𝑦 → ( ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o suc 𝑥 ) ↔ suc 𝑦 ∈ ( 𝐴 +o suc 𝑥 ) ) )
43 42 bicomd ⊢ ( ( 𝐴 +o 𝐵 ) = suc 𝑦 → ( suc 𝑦 ∈ ( 𝐴 +o suc 𝑥 ) ↔ ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o suc 𝑥 ) ) )
44 41 43 sylan9bbr ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ) ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) ↔ ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o suc 𝑥 ) ) )
45 1 adantr ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ On )
46 sucelon ⊢ ( 𝑥 ∈ On ↔ suc 𝑥 ∈ On )
47 26 46 sylib ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → suc 𝑥 ∈ On )
48 45 47 jca ⊢ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐵 ∈ On ∧ suc 𝑥 ∈ On ) )
49 oaord ⊢ ( ( 𝐵 ∈ On ∧ suc 𝑥 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ suc 𝑥 ↔ ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o suc 𝑥 ) ) )
50 49 3expa ⊢ ( ( ( 𝐵 ∈ On ∧ suc 𝑥 ∈ On ) ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ suc 𝑥 ↔ ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o suc 𝑥 ) ) )
51 48 50 sylan ⊢ ( ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝐴 ∈ On ) → ( 𝐵 ∈ suc 𝑥 ↔ ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o suc 𝑥 ) ) )
52 51 ancoms ⊢ ( ( 𝐴 ∈ On ∧ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝐵 ∈ suc 𝑥 ↔ ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o suc 𝑥 ) ) )
53 52 adantl ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ) ) → ( 𝐵 ∈ suc 𝑥 ↔ ( 𝐴 +o 𝐵 ) ∈ ( 𝐴 +o suc 𝑥 ) ) )
54 44 53 bitr4d ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ) ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) ↔ 𝐵 ∈ suc 𝑥 ) )
55 54 biimpd ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ) ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) → 𝐵 ∈ suc 𝑥 ) )
56 55 exp32 ⊢ ( ( 𝐴 +o 𝐵 ) = suc 𝑦 → ( 𝐴 ∈ On → ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) → 𝐵 ∈ suc 𝑥 ) ) ) )
57 56 com4l ⊢ ( 𝐴 ∈ On → ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) → ( ( 𝐴 +o 𝐵 ) = suc 𝑦 → 𝐵 ∈ suc 𝑥 ) ) ) )
58 57 imp32 ⊢ ( ( 𝐴 ∈ On ∧ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 +o 𝑥 ) ) ) → ( ( 𝐴 +o 𝐵 ) = suc 𝑦 → 𝐵 ∈ suc 𝑥 ) )
59 33 58 mtod ⊢ ( ( 𝐴 ∈ On ∧ ( ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 +o 𝑥 ) ) ) → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 )
60 59 exp44 ⊢ ( 𝐴 ∈ On → ( ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) → ( 𝑥 ∈ 𝐵 → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 ) ) ) )
61 60 imp ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( 𝑥 ∈ 𝐵 → ( 𝑦 ∈ ( 𝐴 +o 𝑥 ) → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 ) ) )
62 61 rexlimdv ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 +o 𝑥 ) → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 ) )
63 62 adantl ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ) → ( ∃ 𝑥 ∈ 𝐵 𝑦 ∈ ( 𝐴 +o 𝑥 ) → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 ) )
64 24 63 mpd ⊢ ( ( ( 𝐴 +o 𝐵 ) = suc 𝑦 ∧ ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ) → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 )
65 64 expcom ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ( ( 𝐴 +o 𝐵 ) = suc 𝑦 → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 ) )
66 65 pm2.01d ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 )
67 66 adantr ⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) ∧ 𝑦 ∈ On ) → ¬ ( 𝐴 +o 𝐵 ) = suc 𝑦 )
68 67 nrexdv ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ¬ ∃ 𝑦 ∈ On ( 𝐴 +o 𝐵 ) = suc 𝑦 )
69 ioran ⊢ ( ¬ ( ( 𝐴 +o 𝐵 ) = ∅ ∨ ∃ 𝑦 ∈ On ( 𝐴 +o 𝐵 ) = suc 𝑦 ) ↔ ( ¬ ( 𝐴 +o 𝐵 ) = ∅ ∧ ¬ ∃ 𝑦 ∈ On ( 𝐴 +o 𝐵 ) = suc 𝑦 ) )
70 15 68 69 sylanbrc ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → ¬ ( ( 𝐴 +o 𝐵 ) = ∅ ∨ ∃ 𝑦 ∈ On ( 𝐴 +o 𝐵 ) = suc 𝑦 ) )
71 dflim3 ⊢ ( Lim ( 𝐴 +o 𝐵 ) ↔ ( Ord ( 𝐴 +o 𝐵 ) ∧ ¬ ( ( 𝐴 +o 𝐵 ) = ∅ ∨ ∃ 𝑦 ∈ On ( 𝐴 +o 𝐵 ) = suc 𝑦 ) ) )
72 5 70 71 sylanbrc ⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐶 ∧ Lim 𝐵 ) ) → Lim ( 𝐴 +o 𝐵 ) )