Metamath Proof Explorer

Theorem oaun3

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

Ref Expression
Assertion oaun3 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ∪ { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +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 undif2 ⊢ ( 𝐴 ∪ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) = ( 𝐴 ∪ ( 𝐴 +o 𝐵 ) )
6 oaword1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 ⊆ ( 𝐴 +o 𝐵 ) )
7 ssequn1 ⊢ ( 𝐴 ⊆ ( 𝐴 +o 𝐵 ) ↔ ( 𝐴 ∪ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )
8 6 7 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ ( 𝐴 +o 𝐵 ) ) = ( 𝐴 +o 𝐵 ) )
9 5 8 eqtrid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) ) = ( 𝐴 +o 𝐵 ) )
10 4 9 eqtrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∪ { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } = ( 𝐴 +o 𝐵 ) )
11 oaun3lem4 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } ∈ suc ( 𝐴 +o 𝐵 ) )
12 unisng ⊢ ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } ∈ suc ( 𝐴 +o 𝐵 ) → ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } )
13 11 12 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } )
14 10 13 uneq12d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∪ { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } ∪ ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } ) = ( ( 𝐴 +o 𝐵 ) ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } ) )
15 uniun ⊢ ∪ ( { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } ) = ( ∪ { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } ∪ ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } )
16 df-tp ⊢ { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) , { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } = ( { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } )
17 rp-abid ⊢ 𝐴 = { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 }
18 17 a1i ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → 𝐴 = { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } )
19 oadif1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) = { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } )
20 eqidd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } = { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } )
21 18 19 20 tpeq123d ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) , { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } = { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } , { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } )
22 16 21 eqtr3id ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } ) = { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } , { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } )
23 22 unieqd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∪ ( { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } ) = ∪ { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } , { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } )
24 15 23 eqtr3id ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∪ { 𝐴 , ( ( 𝐴 +o 𝐵 ) ∖ 𝐴 ) } ∪ ∪ { { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } ) = ∪ { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } , { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } )
25 oaun3lem2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } ⊆ ( 𝐴 +o 𝐵 ) )
26 ssequn2 ⊢ ( { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } ⊆ ( 𝐴 +o 𝐵 ) ↔ ( ( 𝐴 +o 𝐵 ) ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } ) = ( 𝐴 +o 𝐵 ) )
27 25 26 sylib ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 +o 𝐵 ) ∪ { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } ) = ( 𝐴 +o 𝐵 ) )
28 14 24 27 3eqtr3rd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ∪ { { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 𝑥 = 𝑎 } , { 𝑦 ∣ ∃ 𝑏 ∈ 𝐵 𝑦 = ( 𝐴 +o 𝑏 ) } , { 𝑧 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑧 = ( 𝑎 +o 𝑏 ) } } )