Metamath Proof Explorer

Theorem oaun3

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

Ref Expression
Assertion oaun3 
|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = U. { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } , { z | E. a e. A E. b e. B z = ( a +o b ) } } )

Proof

Step Hyp Ref Expression
1 oacl 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
2 1 difexd 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) \ A ) e. _V )
3 uniprg 
 |-  ( ( A e. On /\ ( ( A +o B ) \ A ) e. _V ) -> U. { A , ( ( A +o B ) \ A ) } = ( A u. ( ( A +o B ) \ A ) ) )
4 2 3 syldan 
 |-  ( ( A e. On /\ B e. On ) -> U. { A , ( ( A +o B ) \ A ) } = ( A u. ( ( A +o B ) \ A ) ) )
5 undif2 
 |-  ( A u. ( ( A +o B ) \ A ) ) = ( A u. ( A +o B ) )
6 oaword1 
 |-  ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
7 ssequn1 
 |-  ( A C_ ( A +o B ) <-> ( A u. ( A +o B ) ) = ( A +o B ) )
8 6 7 sylib 
 |-  ( ( A e. On /\ B e. On ) -> ( A u. ( A +o B ) ) = ( A +o B ) )
9 5 8 eqtrid 
 |-  ( ( A e. On /\ B e. On ) -> ( A u. ( ( A +o B ) \ A ) ) = ( A +o B ) )
10 4 9 eqtrd 
 |-  ( ( A e. On /\ B e. On ) -> U. { A , ( ( A +o B ) \ A ) } = ( A +o B ) )
11 oaun3lem4 
 |-  ( ( A e. On /\ B e. On ) -> { z | E. a e. A E. b e. B z = ( a +o b ) } e. suc ( A +o B ) )
12 unisng 
 |-  ( { z | E. a e. A E. b e. B z = ( a +o b ) } e. suc ( A +o B ) -> U. { { z | E. a e. A E. b e. B z = ( a +o b ) } } = { z | E. a e. A E. b e. B z = ( a +o b ) } )
13 11 12 syl 
 |-  ( ( A e. On /\ B e. On ) -> U. { { z | E. a e. A E. b e. B z = ( a +o b ) } } = { z | E. a e. A E. b e. B z = ( a +o b ) } )
14 10 13 uneq12d 
 |-  ( ( A e. On /\ B e. On ) -> ( U. { A , ( ( A +o B ) \ A ) } u. U. { { z | E. a e. A E. b e. B z = ( a +o b ) } } ) = ( ( A +o B ) u. { z | E. a e. A E. b e. B z = ( a +o b ) } ) )
15 uniun 
 |-  U. ( { A , ( ( A +o B ) \ A ) } u. { { z | E. a e. A E. b e. B z = ( a +o b ) } } ) = ( U. { A , ( ( A +o B ) \ A ) } u. U. { { z | E. a e. A E. b e. B z = ( a +o b ) } } )
16 df-tp 
 |-  { A , ( ( A +o B ) \ A ) , { z | E. a e. A E. b e. B z = ( a +o b ) } } = ( { A , ( ( A +o B ) \ A ) } u. { { z | E. a e. A E. b e. B z = ( a +o b ) } } )
17 rp-abid 
 |-  A = { x | E. a e. A x = a }
18 17 a1i 
 |-  ( ( A e. On /\ B e. On ) -> A = { x | E. a e. A x = a } )
19 oadif1 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) \ A ) = { y | E. b e. B y = ( A +o b ) } )
20 eqidd 
 |-  ( ( A e. On /\ B e. On ) -> { z | E. a e. A E. b e. B z = ( a +o b ) } = { z | E. a e. A E. b e. B z = ( a +o b ) } )
21 18 19 20 tpeq123d 
 |-  ( ( A e. On /\ B e. On ) -> { A , ( ( A +o B ) \ A ) , { z | E. a e. A E. b e. B z = ( a +o b ) } } = { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } , { z | E. a e. A E. b e. B z = ( a +o b ) } } )
22 16 21 eqtr3id 
 |-  ( ( A e. On /\ B e. On ) -> ( { A , ( ( A +o B ) \ A ) } u. { { z | E. a e. A E. b e. B z = ( a +o b ) } } ) = { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } , { z | E. a e. A E. b e. B z = ( a +o b ) } } )
23 22 unieqd 
 |-  ( ( A e. On /\ B e. On ) -> U. ( { A , ( ( A +o B ) \ A ) } u. { { z | E. a e. A E. b e. B z = ( a +o b ) } } ) = U. { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } , { z | E. a e. A E. b e. B z = ( a +o b ) } } )
24 15 23 eqtr3id 
 |-  ( ( A e. On /\ B e. On ) -> ( U. { A , ( ( A +o B ) \ A ) } u. U. { { z | E. a e. A E. b e. B z = ( a +o b ) } } ) = U. { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } , { z | E. a e. A E. b e. B z = ( a +o b ) } } )
25 oaun3lem2 
 |-  ( ( A e. On /\ B e. On ) -> { z | E. a e. A E. b e. B z = ( a +o b ) } C_ ( A +o B ) )
26 ssequn2 
 |-  ( { z | E. a e. A E. b e. B z = ( a +o b ) } C_ ( A +o B ) <-> ( ( A +o B ) u. { z | E. a e. A E. b e. B z = ( a +o b ) } ) = ( A +o B ) )
27 25 26 sylib 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A +o B ) u. { z | E. a e. A E. b e. B z = ( a +o b ) } ) = ( A +o B ) )
28 14 24 27 3eqtr3rd 
 |-  ( ( A e. On /\ B e. On ) -> ( A +o B ) = U. { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } , { z | E. a e. A E. b e. B z = ( a +o b ) } } )