Theorem oaun2

Description: Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025)

	Ref	Expression
Assertion	oaun2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ∪ { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } } )

Proof

Step	Hyp	Ref	Expression
1		oacl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )
2	1	difexd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ∈ V )
3		uniprg	⊢ ( ( 𝐴 ∈ On ∧ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ∈ V ) → ∪ { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } = ( 𝐴 ∪ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) )
4	2 3	syldan	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∪ { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } = ( 𝐴 ∪ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) )
5		rp-abid	⊢ 𝐴 = { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 }
6	5	a1i	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 = { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } )
7		oadif1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } )
8	6 7	preq12d	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } = { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } } )
9	8	unieqd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∪ { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } = ∪ { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } } )
10		undif2	⊢ ( 𝐴 ∪ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) = ( 𝐴 ∪ ( 𝐴 +o 𝐵 ) )
11		oaword1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐴 +o 𝐵 ) )
12		ssequn1	⊢ ( 𝐴 ⊆ ( 𝐴 +o 𝐵 ) ↔ ( 𝐴 ∪ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )
13	11 12	sylib	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )
14	10 13	eqtrid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) = ( 𝐴 +o 𝐵 ) )
15	4 9 14	3eqtr3rd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ∪ { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } } )