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 )