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

Metamath Proof Explorer

Theorem oacl

Description: Closure law for ordinal addition. Proposition 8.2 of TakeutiZaring p. 57. Remark 2.8 of Schloeder p. 5. (Contributed by NM, 5-May-1995)

Ref Expression
Assertion oacl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o ∅ ) )
2 1 eleq1d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 +o 𝑥 ) ∈ On ↔ ( 𝐴 +o ∅ ) ∈ On ) )
3 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝑦 ) )
4 3 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 +o 𝑥 ) ∈ On ↔ ( 𝐴 +o 𝑦 ) ∈ On ) )
5 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o suc 𝑦 ) )
6 5 eleq1d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 +o 𝑥 ) ∈ On ↔ ( 𝐴 +o suc 𝑦 ) ∈ On ) )
7 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 +o 𝑥 ) = ( 𝐴 +o 𝐵 ) )
8 7 eleq1d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 +o 𝑥 ) ∈ On ↔ ( 𝐴 +o 𝐵 ) ∈ On ) )
9 oa0 ⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) = 𝐴 )
10 9 eleq1d ⊢ ( 𝐴 ∈ On → ( ( 𝐴 +o ∅ ) ∈ On ↔ 𝐴 ∈ On ) )
11 10 ibir ⊢ ( 𝐴 ∈ On → ( 𝐴 +o ∅ ) ∈ On )
12 onsuc ⊢ ( ( 𝐴 +o 𝑦 ) ∈ On → suc ( 𝐴 +o 𝑦 ) ∈ On )
13 oasuc ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 +o suc 𝑦 ) = suc ( 𝐴 +o 𝑦 ) )
14 13 eleq1d ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o suc 𝑦 ) ∈ On ↔ suc ( 𝐴 +o 𝑦 ) ∈ On ) )
15 12 14 imbitrrid ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 +o 𝑦 ) ∈ On → ( 𝐴 +o suc 𝑦 ) ∈ On ) )
16 15 expcom ⊢ ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( ( 𝐴 +o 𝑦 ) ∈ On → ( 𝐴 +o suc 𝑦 ) ∈ On ) ) )
17 vex ⊢ 𝑥 ∈ V
18 iunon ⊢ ( ( 𝑥 ∈ V ∧ ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ∈ On ) → ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ∈ On )
19 17 18 mpan ⊢ ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ∈ On → ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ∈ On )
20 oalim ⊢ ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐴 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) )
21 17 20 mpanr1 ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) → ( 𝐴 +o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) )
22 21 eleq1d ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) → ( ( 𝐴 +o 𝑥 ) ∈ On ↔ ∪ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ∈ On ) )
23 19 22 imbitrrid ⊢ ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ∈ On → ( 𝐴 +o 𝑥 ) ∈ On ) )
24 23 expcom ⊢ ( Lim 𝑥 → ( 𝐴 ∈ On → ( ∀ 𝑦 ∈ 𝑥 ( 𝐴 +o 𝑦 ) ∈ On → ( 𝐴 +o 𝑥 ) ∈ On ) ) )
25 2 4 6 8 11 16 24 tfinds3 ⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( 𝐴 +o 𝐵 ) ∈ On ) )
26 25 impcom ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )