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 ) ∧ ( ( ( 1^st ‘ 𝑥 ) E ( 1^st ‘ 𝑦 ) ∨ ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ) ∧ ( ( 2^nd ‘ 𝑥 ) E ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ( 𝑧 ∈ V , 𝑎 ∈ V ↦ ∩ { 𝑤 ∈ On ∣ ( ( 𝑎 “ ( { ( 1^st ‘ 𝑧 ) } × ( 2^nd ‘ 𝑧 ) ) ) ⊆ 𝑤 ∧ ( 𝑎 “ ( ( 1^st ‘ 𝑧 ) × { ( 2^nd ‘ 𝑧 ) } ) ) ⊆ 𝑤 ) } ) )

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

Metamath Proof Explorer

Definition df-nadd

Detailed syntax breakdown