Metamath Proof Explorer


Definition df-nadd

Description: Define natural ordinal addition. This is a commutative form of addition over the ordinals. (Contributed by Scott Fenton, 26-Aug-2024)

Ref Expression
Assertion df-nadd +no = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) E ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 ) ) } , ( On × On ) , ( 𝑧 ∈ V , 𝑎 ∈ V ↦ { 𝑤 ∈ On ∣ ( ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) ) ⊆ 𝑤 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnadd +no
1 vx 𝑥
2 vy 𝑦
3 1 cv 𝑥
4 con0 On
5 4 4 cxp ( On × On )
6 3 5 wcel 𝑥 ∈ ( On × On )
7 2 cv 𝑦
8 7 5 wcel 𝑦 ∈ ( On × On )
9 c1st 1st
10 3 9 cfv ( 1st𝑥 )
11 cep E
12 7 9 cfv ( 1st𝑦 )
13 10 12 11 wbr ( 1st𝑥 ) E ( 1st𝑦 )
14 10 12 wceq ( 1st𝑥 ) = ( 1st𝑦 )
15 13 14 wo ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) )
16 c2nd 2nd
17 3 16 cfv ( 2nd𝑥 )
18 7 16 cfv ( 2nd𝑦 )
19 17 18 11 wbr ( 2nd𝑥 ) E ( 2nd𝑦 )
20 17 18 wceq ( 2nd𝑥 ) = ( 2nd𝑦 )
21 19 20 wo ( ( 2nd𝑥 ) E ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) )
22 3 7 wne 𝑥𝑦
23 15 21 22 w3a ( ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) E ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 )
24 6 8 23 w3a ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) E ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 ) )
25 24 1 2 copab { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) E ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 ) ) }
26 vz 𝑧
27 cvv V
28 va 𝑎
29 vw 𝑤
30 28 cv 𝑎
31 26 cv 𝑧
32 31 9 cfv ( 1st𝑧 )
33 32 csn { ( 1st𝑧 ) }
34 31 16 cfv ( 2nd𝑧 )
35 33 34 cxp ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) )
36 30 35 cima ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) )
37 29 cv 𝑤
38 36 37 wss ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) ) ⊆ 𝑤
39 34 csn { ( 2nd𝑧 ) }
40 32 39 cxp ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } )
41 30 40 cima ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) )
42 41 37 wss ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) ) ⊆ 𝑤
43 38 42 wa ( ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) ) ⊆ 𝑤 )
44 43 29 4 crab { 𝑤 ∈ On ∣ ( ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) ) ⊆ 𝑤 ) }
45 44 cint { 𝑤 ∈ On ∣ ( ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) ) ⊆ 𝑤 ) }
46 26 28 27 27 45 cmpo ( 𝑧 ∈ V , 𝑎 ∈ V ↦ { 𝑤 ∈ On ∣ ( ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) ) ⊆ 𝑤 ) } )
47 5 25 46 cfrecs frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) E ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 ) ) } , ( On × On ) , ( 𝑧 ∈ V , 𝑎 ∈ V ↦ { 𝑤 ∈ On ∣ ( ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) ) ⊆ 𝑤 ) } ) )
48 0 47 wceq +no = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st𝑥 ) E ( 1st𝑦 ) ∨ ( 1st𝑥 ) = ( 1st𝑦 ) ) ∧ ( ( 2nd𝑥 ) E ( 2nd𝑦 ) ∨ ( 2nd𝑥 ) = ( 2nd𝑦 ) ) ∧ 𝑥𝑦 ) ) } , ( On × On ) , ( 𝑧 ∈ V , 𝑎 ∈ V ↦ { 𝑤 ∈ On ∣ ( ( 𝑎 “ ( { ( 1st𝑧 ) } × ( 2nd𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1st𝑧 ) × { ( 2nd𝑧 ) } ) ) ⊆ 𝑤 ) } ) )