naddcllem

Description: Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024)

		Ref	Expression
	Assertion	naddcllem	$⊢ (A \in On \land B \in On) \to (A + B \in On \land A + B = ⋂ \{x \in On \| (+ [\{A\} \times B] \subseteq x \land + [A \times \{B\}] \subseteq x)\})$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ a = c \to a + b = c + b$
2	1	eleq1d	$⊢ a = c \to (a + b \in On \leftrightarrow c + b \in On)$
3		sneq	$⊢ a = c \to \{a\} = \{c\}$
4	3	xpeq1d	$⊢ a = c \to \{a\} \times b = \{c\} \times b$
5	4	imaeq2d	$⊢ a = c \to + [\{a\} \times b] = + [\{c\} \times b]$
6	5	sseq1d	$⊢ a = c \to (+ [\{a\} \times b] \subseteq x \leftrightarrow + [\{c\} \times b] \subseteq x)$
7		xpeq1	$⊢ a = c \to a \times \{b\} = c \times \{b\}$
8	7	imaeq2d	$⊢ a = c \to + [a \times \{b\}] = + [c \times \{b\}]$
9	8	sseq1d	$⊢ a = c \to (+ [a \times \{b\}] \subseteq x \leftrightarrow + [c \times \{b\}] \subseteq x)$
10	6 9	anbi12d	$⊢ a = c \to ((+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x) \leftrightarrow (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x))$
11	10	rabbidv	$⊢ a = c \to \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\} = \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}$
12	11	inteqd	$⊢ a = c \to ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\} = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}$
13	1 12	eqeq12d	$⊢ a = c \to (a + b = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\} \leftrightarrow c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\})$
14	2 13	anbi12d	$⊢ a = c \to ((a + b \in On \land a + b = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\}) \leftrightarrow (c + b \in On \land c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}))$
15		oveq2	$⊢ b = d \to c + b = c + d$
16	15	eleq1d	$⊢ b = d \to (c + b \in On \leftrightarrow c + d \in On)$
17		xpeq2	$⊢ b = d \to \{c\} \times b = \{c\} \times d$
18	17	imaeq2d	$⊢ b = d \to + [\{c\} \times b] = + [\{c\} \times d]$
19	18	sseq1d	$⊢ b = d \to (+ [\{c\} \times b] \subseteq x \leftrightarrow + [\{c\} \times d] \subseteq x)$
20		sneq	$⊢ b = d \to \{b\} = \{d\}$
21	20	xpeq2d	$⊢ b = d \to c \times \{b\} = c \times \{d\}$
22	21	imaeq2d	$⊢ b = d \to + [c \times \{b\}] = + [c \times \{d\}]$
23	22	sseq1d	$⊢ b = d \to (+ [c \times \{b\}] \subseteq x \leftrightarrow + [c \times \{d\}] \subseteq x)$
24	19 23	anbi12d	$⊢ b = d \to ((+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x) \leftrightarrow (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x))$
25	24	rabbidv	$⊢ b = d \to \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\} = \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}$
26	25	inteqd	$⊢ b = d \to ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\} = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}$
27	15 26	eqeq12d	$⊢ b = d \to (c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\} \leftrightarrow c + d = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\})$
28	16 27	anbi12d	$⊢ b = d \to ((c + b \in On \land c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}) \leftrightarrow (c + d \in On \land c + d = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}))$
29		oveq1	$⊢ a = c \to a + d = c + d$
30	29	eleq1d	$⊢ a = c \to (a + d \in On \leftrightarrow c + d \in On)$
31	3	xpeq1d	$⊢ a = c \to \{a\} \times d = \{c\} \times d$
32	31	imaeq2d	$⊢ a = c \to + [\{a\} \times d] = + [\{c\} \times d]$
33	32	sseq1d	$⊢ a = c \to (+ [\{a\} \times d] \subseteq x \leftrightarrow + [\{c\} \times d] \subseteq x)$
34		xpeq1	$⊢ a = c \to a \times \{d\} = c \times \{d\}$
35	34	imaeq2d	$⊢ a = c \to + [a \times \{d\}] = + [c \times \{d\}]$
36	35	sseq1d	$⊢ a = c \to (+ [a \times \{d\}] \subseteq x \leftrightarrow + [c \times \{d\}] \subseteq x)$
37	33 36	anbi12d	$⊢ a = c \to ((+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x) \leftrightarrow (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x))$
38	37	rabbidv	$⊢ a = c \to \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\} = \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}$
39	38	inteqd	$⊢ a = c \to ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\} = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}$
40	29 39	eqeq12d	$⊢ a = c \to (a + d = ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\} \leftrightarrow c + d = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\})$
41	30 40	anbi12d	$⊢ a = c \to ((a + d \in On \land a + d = ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\}) \leftrightarrow (c + d \in On \land c + d = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}))$
42		oveq1	$⊢ a = A \to a + b = A + b$
43	42	eleq1d	$⊢ a = A \to (a + b \in On \leftrightarrow A + b \in On)$
44		sneq	$⊢ a = A \to \{a\} = \{A\}$
45	44	xpeq1d	$⊢ a = A \to \{a\} \times b = \{A\} \times b$
46	45	imaeq2d	$⊢ a = A \to + [\{a\} \times b] = + [\{A\} \times b]$
47	46	sseq1d	$⊢ a = A \to (+ [\{a\} \times b] \subseteq x \leftrightarrow + [\{A\} \times b] \subseteq x)$
48		xpeq1	$⊢ a = A \to a \times \{b\} = A \times \{b\}$
49	48	imaeq2d	$⊢ a = A \to + [a \times \{b\}] = + [A \times \{b\}]$
50	49	sseq1d	$⊢ a = A \to (+ [a \times \{b\}] \subseteq x \leftrightarrow + [A \times \{b\}] \subseteq x)$
51	47 50	anbi12d	$⊢ a = A \to ((+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x) \leftrightarrow (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x))$
52	51	rabbidv	$⊢ a = A \to \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\} = \{x \in On \| (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x)\}$
53	52	inteqd	$⊢ a = A \to ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\} = ⋂ \{x \in On \| (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x)\}$
54	42 53	eqeq12d	$⊢ a = A \to (a + b = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\} \leftrightarrow A + b = ⋂ \{x \in On \| (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x)\})$
55	43 54	anbi12d	$⊢ a = A \to ((a + b \in On \land a + b = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\}) \leftrightarrow (A + b \in On \land A + b = ⋂ \{x \in On \| (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x)\}))$
56		oveq2	$⊢ b = B \to A + b = A + B$
57	56	eleq1d	$⊢ b = B \to (A + b \in On \leftrightarrow A + B \in On)$
58		xpeq2	$⊢ b = B \to \{A\} \times b = \{A\} \times B$
59	58	imaeq2d	$⊢ b = B \to + [\{A\} \times b] = + [\{A\} \times B]$
60	59	sseq1d	$⊢ b = B \to (+ [\{A\} \times b] \subseteq x \leftrightarrow + [\{A\} \times B] \subseteq x)$
61		sneq	$⊢ b = B \to \{b\} = \{B\}$
62	61	xpeq2d	$⊢ b = B \to A \times \{b\} = A \times \{B\}$
63	62	imaeq2d	$⊢ b = B \to + [A \times \{b\}] = + [A \times \{B\}]$
64	63	sseq1d	$⊢ b = B \to (+ [A \times \{b\}] \subseteq x \leftrightarrow + [A \times \{B\}] \subseteq x)$
65	60 64	anbi12d	$⊢ b = B \to ((+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x) \leftrightarrow (+ [\{A\} \times B] \subseteq x \land + [A \times \{B\}] \subseteq x))$
66	65	rabbidv	$⊢ b = B \to \{x \in On \| (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x)\} = \{x \in On \| (+ [\{A\} \times B] \subseteq x \land + [A \times \{B\}] \subseteq x)\}$
67	66	inteqd	$⊢ b = B \to ⋂ \{x \in On \| (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x)\} = ⋂ \{x \in On \| (+ [\{A\} \times B] \subseteq x \land + [A \times \{B\}] \subseteq x)\}$
68	56 67	eqeq12d	$⊢ b = B \to (A + b = ⋂ \{x \in On \| (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x)\} \leftrightarrow A + B = ⋂ \{x \in On \| (+ [\{A\} \times B] \subseteq x \land + [A \times \{B\}] \subseteq x)\})$
69	57 68	anbi12d	$⊢ b = B \to ((A + b \in On \land A + b = ⋂ \{x \in On \| (+ [\{A\} \times b] \subseteq x \land + [A \times \{b\}] \subseteq x)\}) \leftrightarrow (A + B \in On \land A + B = ⋂ \{x \in On \| (+ [\{A\} \times B] \subseteq x \land + [A \times \{B\}] \subseteq x)\}))$
70		simpl	$⊢ (c + b \in On \land c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}) \to c + b \in On$
71	70	ralimi	$⊢ \forall c \in a (c + b \in On \land c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}) \to \forall c \in a c + b \in On$
72	71	3ad2ant2	$⊢ (\forall c \in a \forall d \in b (c + d \in On \land c + d = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}) \land \forall c \in a (c + b \in On \land c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}) \land \forall d \in b (a + d \in On \land a + d = ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\})) \to \forall c \in a c + b \in On$
73		simpl	$⊢ (a + d \in On \land a + d = ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\}) \to a + d \in On$
74	73	ralimi	$⊢ \forall d \in b (a + d \in On \land a + d = ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\}) \to \forall d \in b a + d \in On$
75	74	3ad2ant3	$⊢ (\forall c \in a \forall d \in b (c + d \in On \land c + d = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}) \land \forall c \in a (c + b \in On \land c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}) \land \forall d \in b (a + d \in On \land a + d = ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\})) \to \forall d \in b a + d \in On$
76	72 75	jca	$⊢ (\forall c \in a \forall d \in b (c + d \in On \land c + d = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}) \land \forall c \in a (c + b \in On \land c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}) \land \forall d \in b (a + d \in On \land a + d = ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\})) \to (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)$
77		df-nadd	$⊢ + = frecs (\{⟨p, q⟩ \| (p \in (On \times On) \land q \in (On \times On) \land ((1^{st} (p) E 1^{st} (q) \lor 1^{st} (p) = 1^{st} (q)) \land (2^{nd} (p) E 2^{nd} (q) \lor 2^{nd} (p) = 2^{nd} (q)) \land p \neq q))\}, On \times On, (t \in V, f \in V ⟼ ⋂ \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\}))$
78	77	on2recsov	$⊢ (a \in On \land b \in On) \to a + b = ⟨a, b⟩ (t \in V, f \in V ⟼ ⋂ \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\}) ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})})$
79	78	adantr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to a + b = ⟨a, b⟩ (t \in V, f \in V ⟼ ⋂ \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\}) ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})})$
80		opex	$⊢ ⟨a, b⟩ \in V$
81		naddfn	$⊢ + Fn (On \times On)$
82		fnfun	$⊢ + Fn (On \times On) \to Fun +$
83	81 82	ax-mp	$⊢ Fun +$
84		vex	$⊢ a \in V$
85	84	sucex	$⊢ suc a \in V$
86		vex	$⊢ b \in V$
87	86	sucex	$⊢ suc b \in V$
88	85 87	xpex	$⊢ suc a \times suc b \in V$
89	88	difexi	$⊢ (suc a \times suc b) ∖ \{⟨a, b⟩\} \in V$
90		resfunexg	$⊢ (Fun + \land (suc a \times suc b) ∖ \{⟨a, b⟩\} \in V) \to {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \in V$
91	83 89 90	mp2an	$⊢ {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \in V$
92		eloni	$⊢ b \in On \to Ord b$
93	92	ad2antlr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to Ord b$
94		ordirr	$⊢ Ord b \to \neg b \in b$
95	93 94	syl	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \neg b \in b$
96	95	olcd	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to (\neg a \in \{a\} \lor \neg b \in b)$
97		ianor	$⊢ \neg (a \in \{a\} \land b \in b) \leftrightarrow (\neg a \in \{a\} \lor \neg b \in b)$
98		opelxp	$⊢ ⟨a, b⟩ \in (\{a\} \times b) \leftrightarrow (a \in \{a\} \land b \in b)$
99	97 98	xchnxbir	$⊢ \neg ⟨a, b⟩ \in (\{a\} \times b) \leftrightarrow (\neg a \in \{a\} \lor \neg b \in b)$
100	96 99	sylibr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \neg ⟨a, b⟩ \in (\{a\} \times b)$
101	84	sucid	$⊢ a \in suc a$
102		snssi	$⊢ a \in suc a \to \{a\} \subseteq suc a$
103	101 102	ax-mp	$⊢ \{a\} \subseteq suc a$
104		sssucid	$⊢ b \subseteq suc b$
105		xpss12	$⊢ (\{a\} \subseteq suc a \land b \subseteq suc b) \to \{a\} \times b \subseteq suc a \times suc b$
106	103 104 105	mp2an	$⊢ \{a\} \times b \subseteq suc a \times suc b$
107		ssdifsn	$⊢ \{a\} \times b \subseteq (suc a \times suc b) ∖ \{⟨a, b⟩\} \leftrightarrow (\{a\} \times b \subseteq suc a \times suc b \land \neg ⟨a, b⟩ \in (\{a\} \times b))$
108	106 107	mpbiran	$⊢ \{a\} \times b \subseteq (suc a \times suc b) ∖ \{⟨a, b⟩\} \leftrightarrow \neg ⟨a, b⟩ \in (\{a\} \times b)$
109	100 108	sylibr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \{a\} \times b \subseteq (suc a \times suc b) ∖ \{⟨a, b⟩\}$
110		resima2	$⊢ \{a\} \times b \subseteq (suc a \times suc b) ∖ \{⟨a, b⟩\} \to ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] = + [\{a\} \times b]$
111	109 110	syl	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] = + [\{a\} \times b]$
112	111	sseq1d	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \leftrightarrow + [\{a\} \times b] \subseteq x)$
113		eloni	$⊢ a \in On \to Ord a$
114	113	ad2antrr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to Ord a$
115		ordirr	$⊢ Ord a \to \neg a \in a$
116	114 115	syl	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \neg a \in a$
117	116	orcd	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to (\neg a \in a \lor \neg b \in \{b\})$
118		ianor	$⊢ \neg (a \in a \land b \in \{b\}) \leftrightarrow (\neg a \in a \lor \neg b \in \{b\})$
119		opelxp	$⊢ ⟨a, b⟩ \in (a \times \{b\}) \leftrightarrow (a \in a \land b \in \{b\})$
120	118 119	xchnxbir	$⊢ \neg ⟨a, b⟩ \in (a \times \{b\}) \leftrightarrow (\neg a \in a \lor \neg b \in \{b\})$
121	117 120	sylibr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \neg ⟨a, b⟩ \in (a \times \{b\})$
122		sssucid	$⊢ a \subseteq suc a$
123	86	sucid	$⊢ b \in suc b$
124		snssi	$⊢ b \in suc b \to \{b\} \subseteq suc b$
125	123 124	ax-mp	$⊢ \{b\} \subseteq suc b$
126		xpss12	$⊢ (a \subseteq suc a \land \{b\} \subseteq suc b) \to a \times \{b\} \subseteq suc a \times suc b$
127	122 125 126	mp2an	$⊢ a \times \{b\} \subseteq suc a \times suc b$
128		ssdifsn	$⊢ a \times \{b\} \subseteq (suc a \times suc b) ∖ \{⟨a, b⟩\} \leftrightarrow (a \times \{b\} \subseteq suc a \times suc b \land \neg ⟨a, b⟩ \in (a \times \{b\}))$
129	127 128	mpbiran	$⊢ a \times \{b\} \subseteq (suc a \times suc b) ∖ \{⟨a, b⟩\} \leftrightarrow \neg ⟨a, b⟩ \in (a \times \{b\})$
130	121 129	sylibr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to a \times \{b\} \subseteq (suc a \times suc b) ∖ \{⟨a, b⟩\}$
131		resima2	$⊢ a \times \{b\} \subseteq (suc a \times suc b) ∖ \{⟨a, b⟩\} \to ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] = + [a \times \{b\}]$
132	130 131	syl	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] = + [a \times \{b\}]$
133	132	sseq1d	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x \leftrightarrow + [a \times \{b\}] \subseteq x)$
134	112 133	anbi12d	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to ((({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x) \leftrightarrow (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x))$
135	134	rabbidv	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \{x \in On \| (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)\} = \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\}$
136	135	inteqd	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to ⋂ \{x \in On \| (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)\} = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\}$
137		simprr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \forall d \in b a + d \in On$
138		oveq1	$⊢ t = a \to t + d = a + d$
139	138	eleq1d	$⊢ t = a \to (t + d \in On \leftrightarrow a + d \in On)$
140	139	ralbidv	$⊢ t = a \to (\forall d \in b t + d \in On \leftrightarrow \forall d \in b a + d \in On)$
141	84 140	ralsn	$⊢ \forall t \in \{a\} \forall d \in b t + d \in On \leftrightarrow \forall d \in b a + d \in On$
142	137 141	sylibr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \forall t \in \{a\} \forall d \in b t + d \in On$
143		snssi	$⊢ a \in On \to \{a\} \subseteq On$
144		onss	$⊢ b \in On \to b \subseteq On$
145		xpss12	$⊢ (\{a\} \subseteq On \land b \subseteq On) \to \{a\} \times b \subseteq On \times On$
146	143 144 145	syl2an	$⊢ (a \in On \land b \in On) \to \{a\} \times b \subseteq On \times On$
147	146	adantr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \{a\} \times b \subseteq On \times On$
148	81	fndmi	$⊢ dom + = On \times On$
149	147 148	sseqtrrdi	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \{a\} \times b \subseteq dom +$
150		funimassov	$⊢ (Fun + \land \{a\} \times b \subseteq dom +) \to (+ [\{a\} \times b] \subseteq On \leftrightarrow \forall t \in \{a\} \forall d \in b t + d \in On)$
151	83 149 150	sylancr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to (+ [\{a\} \times b] \subseteq On \leftrightarrow \forall t \in \{a\} \forall d \in b t + d \in On)$
152	142 151	mpbird	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to + [\{a\} \times b] \subseteq On$
153		simprl	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \forall c \in a c + b \in On$
154		oveq2	$⊢ t = b \to c + t = c + b$
155	154	eleq1d	$⊢ t = b \to (c + t \in On \leftrightarrow c + b \in On)$
156	86 155	ralsn	$⊢ \forall t \in \{b\} c + t \in On \leftrightarrow c + b \in On$
157	156	ralbii	$⊢ \forall c \in a \forall t \in \{b\} c + t \in On \leftrightarrow \forall c \in a c + b \in On$
158	153 157	sylibr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \forall c \in a \forall t \in \{b\} c + t \in On$
159		onss	$⊢ a \in On \to a \subseteq On$
160		snssi	$⊢ b \in On \to \{b\} \subseteq On$
161		xpss12	$⊢ (a \subseteq On \land \{b\} \subseteq On) \to a \times \{b\} \subseteq On \times On$
162	159 160 161	syl2an	$⊢ (a \in On \land b \in On) \to a \times \{b\} \subseteq On \times On$
163	162	adantr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to a \times \{b\} \subseteq On \times On$
164	163 148	sseqtrrdi	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to a \times \{b\} \subseteq dom +$
165		funimassov	$⊢ (Fun + \land a \times \{b\} \subseteq dom +) \to (+ [a \times \{b\}] \subseteq On \leftrightarrow \forall c \in a \forall t \in \{b\} c + t \in On)$
166	83 164 165	sylancr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to (+ [a \times \{b\}] \subseteq On \leftrightarrow \forall c \in a \forall t \in \{b\} c + t \in On)$
167	158 166	mpbird	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to + [a \times \{b\}] \subseteq On$
168	152 167	unssd	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to + [\{a\} \times b] \cup + [a \times \{b\}] \subseteq On$
169		ssorduni	$⊢ + [\{a\} \times b] \cup + [a \times \{b\}] \subseteq On \to Ord ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}])$
170	168 169	syl	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to Ord ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}])$
171		vsnex	$⊢ \{a\} \in V$
172	171 86	xpex	$⊢ \{a\} \times b \in V$
173		funimaexg	$⊢ (Fun + \land \{a\} \times b \in V) \to + [\{a\} \times b] \in V$
174	83 172 173	mp2an	$⊢ + [\{a\} \times b] \in V$
175		vsnex	$⊢ \{b\} \in V$
176	84 175	xpex	$⊢ a \times \{b\} \in V$
177		funimaexg	$⊢ (Fun + \land a \times \{b\} \in V) \to + [a \times \{b\}] \in V$
178	83 176 177	mp2an	$⊢ + [a \times \{b\}] \in V$
179	174 178	unex	$⊢ + [\{a\} \times b] \cup + [a \times \{b\}] \in V$
180	179	uniex	$⊢ ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \in V$
181	180	elon	$⊢ ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \in On \leftrightarrow Ord ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}])$
182	170 181	sylibr	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \in On$
183		onsucb	$⊢ ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \in On \leftrightarrow suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \in On$
184	182 183	sylib	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \in On$
185		onsucuni	$⊢ + [\{a\} \times b] \cup + [a \times \{b\}] \subseteq On \to + [\{a\} \times b] \cup + [a \times \{b\}] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}])$
186	168 185	syl	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to + [\{a\} \times b] \cup + [a \times \{b\}] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}])$
187	186	unssad	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to + [\{a\} \times b] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}])$
188	186	unssbd	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to + [a \times \{b\}] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}])$
189		sseq2	$⊢ x = suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \to (+ [\{a\} \times b] \subseteq x \leftrightarrow + [\{a\} \times b] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]))$
190		sseq2	$⊢ x = suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \to (+ [a \times \{b\}] \subseteq x \leftrightarrow + [a \times \{b\}] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]))$
191	189 190	anbi12d	$⊢ x = suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \to ((+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x) \leftrightarrow (+ [\{a\} \times b] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \land + [a \times \{b\}] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}])))$
192	191	rspcev	$⊢ (suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \in On \land (+ [\{a\} \times b] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]) \land + [a \times \{b\}] \subseteq suc ⋃ (+ [\{a\} \times b] \cup + [a \times \{b\}]))) \to \exists x \in On (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)$
193	184 187 188 192	syl12anc	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to \exists x \in On (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)$
194		onintrab2	$⊢ \exists x \in On (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x) \leftrightarrow ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\} \in On$
195	193 194	sylib	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\} \in On$
196	136 195	eqeltrd	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to ⋂ \{x \in On \| (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)\} \in On$
197	84 86	op1std	$⊢ t = ⟨a, b⟩ \to 1^{st} (t) = a$
198	197	sneqd	$⊢ t = ⟨a, b⟩ \to \{1^{st} (t)\} = \{a\}$
199	84 86	op2ndd	$⊢ t = ⟨a, b⟩ \to 2^{nd} (t) = b$
200	198 199	xpeq12d	$⊢ t = ⟨a, b⟩ \to \{1^{st} (t)\} \times 2^{nd} (t) = \{a\} \times b$
201	200	imaeq2d	$⊢ t = ⟨a, b⟩ \to f [\{1^{st} (t)\} \times 2^{nd} (t)] = f [\{a\} \times b]$
202	201	sseq1d	$⊢ t = ⟨a, b⟩ \to (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \leftrightarrow f [\{a\} \times b] \subseteq x)$
203	199	sneqd	$⊢ t = ⟨a, b⟩ \to \{2^{nd} (t)\} = \{b\}$
204	197 203	xpeq12d	$⊢ t = ⟨a, b⟩ \to 1^{st} (t) \times \{2^{nd} (t)\} = a \times \{b\}$
205	204	imaeq2d	$⊢ t = ⟨a, b⟩ \to f [1^{st} (t) \times \{2^{nd} (t)\}] = f [a \times \{b\}]$
206	205	sseq1d	$⊢ t = ⟨a, b⟩ \to (f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x \leftrightarrow f [a \times \{b\}] \subseteq x)$
207	202 206	anbi12d	$⊢ t = ⟨a, b⟩ \to ((f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x) \leftrightarrow (f [\{a\} \times b] \subseteq x \land f [a \times \{b\}] \subseteq x))$
208	207	rabbidv	$⊢ t = ⟨a, b⟩ \to \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\} = \{x \in On \| (f [\{a\} \times b] \subseteq x \land f [a \times \{b\}] \subseteq x)\}$
209	208	inteqd	$⊢ t = ⟨a, b⟩ \to ⋂ \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\} = ⋂ \{x \in On \| (f [\{a\} \times b] \subseteq x \land f [a \times \{b\}] \subseteq x)\}$
210		imaeq1	$⊢ f = {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \to f [\{a\} \times b] = ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b]$
211	210	sseq1d	$⊢ f = {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \to (f [\{a\} \times b] \subseteq x \leftrightarrow ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x)$
212		imaeq1	$⊢ f = {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \to f [a \times \{b\}] = ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}]$
213	212	sseq1d	$⊢ f = {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \to (f [a \times \{b\}] \subseteq x \leftrightarrow ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)$
214	211 213	anbi12d	$⊢ f = {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \to ((f [\{a\} \times b] \subseteq x \land f [a \times \{b\}] \subseteq x) \leftrightarrow (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x))$
215	214	rabbidv	$⊢ f = {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \to \{x \in On \| (f [\{a\} \times b] \subseteq x \land f [a \times \{b\}] \subseteq x)\} = \{x \in On \| (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)\}$
216	215	inteqd	$⊢ f = {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \to ⋂ \{x \in On \| (f [\{a\} \times b] \subseteq x \land f [a \times \{b\}] \subseteq x)\} = ⋂ \{x \in On \| (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)\}$
217		eqid	$⊢ (t \in V, f \in V ⟼ ⋂ \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\}) = (t \in V, f \in V ⟼ ⋂ \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\})$
218	209 216 217	ovmpog	$⊢ (⟨a, b⟩ \in V \land {+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})} \in V \land ⋂ \{x \in On \| (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)\} \in On) \to ⟨a, b⟩ (t \in V, f \in V ⟼ ⋂ \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\}) ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) = ⋂ \{x \in On \| (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)\}$
219	80 91 196 218	mp3an12i	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to ⟨a, b⟩ (t \in V, f \in V ⟼ ⋂ \{x \in On \| (f [\{1^{st} (t)\} \times 2^{nd} (t)] \subseteq x \land f [1^{st} (t) \times \{2^{nd} (t)\}] \subseteq x)\}) ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) = ⋂ \{x \in On \| (({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [\{a\} \times b] \subseteq x \land ({+ ↾}_{((suc a \times suc b) ∖ \{⟨a, b⟩\})}) [a \times \{b\}] \subseteq x)\}$
220	79 219 136	3eqtrd	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to a + b = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\}$
221	220 195	eqeltrd	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to a + b \in On$
222	221 220	jca	$⊢ ((a \in On \land b \in On) \land (\forall c \in a c + b \in On \land \forall d \in b a + d \in On)) \to (a + b \in On \land a + b = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\})$
223	222	ex	$⊢ (a \in On \land b \in On) \to ((\forall c \in a c + b \in On \land \forall d \in b a + d \in On) \to (a + b \in On \land a + b = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\}))$
224	76 223	syl5	$⊢ (a \in On \land b \in On) \to ((\forall c \in a \forall d \in b (c + d \in On \land c + d = ⋂ \{x \in On \| (+ [\{c\} \times d] \subseteq x \land + [c \times \{d\}] \subseteq x)\}) \land \forall c \in a (c + b \in On \land c + b = ⋂ \{x \in On \| (+ [\{c\} \times b] \subseteq x \land + [c \times \{b\}] \subseteq x)\}) \land \forall d \in b (a + d \in On \land a + d = ⋂ \{x \in On \| (+ [\{a\} \times d] \subseteq x \land + [a \times \{d\}] \subseteq x)\})) \to (a + b \in On \land a + b = ⋂ \{x \in On \| (+ [\{a\} \times b] \subseteq x \land + [a \times \{b\}] \subseteq x)\}))$
225	14 28 41 55 69 224	on2ind	$⊢ (A \in On \land B \in On) \to (A + B \in On \land A + B = ⋂ \{x \in On \| (+ [\{A\} \times B] \subseteq x \land + [A \times \{B\}] \subseteq x)\})$

Metamath Proof Explorer

Theorem naddcllem

Proof