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	$⊢ + = frecs (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, On \times On, (z \in V, a \in V ⟼ ⋂ \{w \in On \| (a [\{1^{st} (z)\} \times 2^{nd} (z)] \subseteq w \land a [1^{st} (z) \times \{2^{nd} (z)\}] \subseteq w)\}))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnadd	$class +$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4		con0	$class On$
5	4 4	cxp	$class (On \times On)$
6	3 5	wcel	$wff x \in (On \times On)$
7	2	cv	$setvar y$
8	7 5	wcel	$wff y \in (On \times On)$
9		c1st	$class 1^{st}$
10	3 9	cfv	$class 1^{st} (x)$
11		cep	$class E$
12	7 9	cfv	$class 1^{st} (y)$
13	10 12 11	wbr	$wff 1^{st} (x) E 1^{st} (y)$
14	10 12	wceq	$wff 1^{st} (x) = 1^{st} (y)$
15	13 14	wo	$wff (1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y))$
16		c2nd	$class 2^{nd}$
17	3 16	cfv	$class 2^{nd} (x)$
18	7 16	cfv	$class 2^{nd} (y)$
19	17 18 11	wbr	$wff 2^{nd} (x) E 2^{nd} (y)$
20	17 18	wceq	$wff 2^{nd} (x) = 2^{nd} (y)$
21	19 20	wo	$wff (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y))$
22	3 7	wne	$wff x \neq y$
23	15 21 22	w3a	$wff ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y)$
24	6 8 23	w3a	$wff (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))$
25	24 1 2	copab	$class \{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
26		vz	$setvar z$
27		cvv	$class V$
28		va	$setvar a$
29		vw	$setvar w$
30	28	cv	$setvar a$
31	26	cv	$setvar z$
32	31 9	cfv	$class 1^{st} (z)$
33	32	csn	$class \{1^{st} (z)\}$
34	31 16	cfv	$class 2^{nd} (z)$
35	33 34	cxp	$class (\{1^{st} (z)\} \times 2^{nd} (z))$
36	30 35	cima	$class a [\{1^{st} (z)\} \times 2^{nd} (z)]$
37	29	cv	$setvar w$
38	36 37	wss	$wff a [\{1^{st} (z)\} \times 2^{nd} (z)] \subseteq w$
39	34	csn	$class \{2^{nd} (z)\}$
40	32 39	cxp	$class (1^{st} (z) \times \{2^{nd} (z)\})$
41	30 40	cima	$class a [1^{st} (z) \times \{2^{nd} (z)\}]$
42	41 37	wss	$wff a [1^{st} (z) \times \{2^{nd} (z)\}] \subseteq w$
43	38 42	wa	$wff (a [\{1^{st} (z)\} \times 2^{nd} (z)] \subseteq w \land a [1^{st} (z) \times \{2^{nd} (z)\}] \subseteq w)$
44	43 29 4	crab	$class \{w \in On \| (a [\{1^{st} (z)\} \times 2^{nd} (z)] \subseteq w \land a [1^{st} (z) \times \{2^{nd} (z)\}] \subseteq w)\}$
45	44	cint	$class ⋂ \{w \in On \| (a [\{1^{st} (z)\} \times 2^{nd} (z)] \subseteq w \land a [1^{st} (z) \times \{2^{nd} (z)\}] \subseteq w)\}$
46	26 28 27 27 45	cmpo	$class (z \in V, a \in V ⟼ ⋂ \{w \in On \| (a [\{1^{st} (z)\} \times 2^{nd} (z)] \subseteq w \land a [1^{st} (z) \times \{2^{nd} (z)\}] \subseteq w)\})$
47	5 25 46	cfrecs	$class frecs (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, On \times On, (z \in V, a \in V ⟼ ⋂ \{w \in On \| (a [\{1^{st} (z)\} \times 2^{nd} (z)] \subseteq w \land a [1^{st} (z) \times \{2^{nd} (z)\}] \subseteq w)\}))$
48	0 47	wceq	$wff + = frecs (\{⟨x, y⟩ \| (x \in (On \times On) \land y \in (On \times On) \land ((1^{st} (x) E 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) E 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}, On \times On, (z \in V, a \in V ⟼ ⋂ \{w \in On \| (a [\{1^{st} (z)\} \times 2^{nd} (z)] \subseteq w \land a [1^{st} (z) \times \{2^{nd} (z)\}] \subseteq w)\}))$

Metamath Proof Explorer

Definition df-nadd

Detailed syntax breakdown