naddcllem - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > naddcllem		Structured version Visualization version GIF version

Theorem naddcllem 8661

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

**Assertion**
Ref	Expression
naddcllem	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))

Distinct variable groups: 𝑥,𝐴 𝑥,𝐵

Proof of Theorem naddcllem Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑓 𝑡 𝑝 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7418	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
2	1	eleq1d 2854	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3		sneq 4604	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → {𝑎} = {𝑐})
4	3	xpeq1d 5691	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
5	4	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
6	5	sseq1d 3976	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7		xpeq1 5676	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
8	7	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
9	8	sseq1d 3976	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
10	6, 9	anbi12d 643	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
11	10	rabbidv 3430	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
12	11	inteqd 4921	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
13	1, 12	eqeq12d 2785	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}))
14	2, 13	anbi12d 643	. 2 ⊢ (𝑎 = 𝑐 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})))
15		oveq2 7419	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
16	15	eleq1d 2854	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17		xpeq2 5683	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
18	17	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
19	18	sseq1d 3976	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20		sneq 4604	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → {𝑏} = {𝑑})
21	20	xpeq2d 5692	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
22	21	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
23	22	sseq1d 3976	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
24	19, 23	anbi12d 643	. . . . . 6 ⊢ (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
25	24	rabbidv 3430	. . . . 5 ⊢ (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
26	25	inteqd 4921	. . . 4 ⊢ (𝑏 = 𝑑 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
27	15, 26	eqeq12d 2785	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
28	16, 27	anbi12d 643	. 2 ⊢ (𝑏 = 𝑑 → (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
29		oveq1 7418	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
30	29	eleq1d 2854	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
31	3	xpeq1d 5691	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
32	31	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
33	32	sseq1d 3976	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34		xpeq1 5676	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
35	34	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
36	35	sseq1d 3976	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
37	33, 36	anbi12d 643	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
38	37	rabbidv 3430	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
39	38	inteqd 4921	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
40	29, 39	eqeq12d 2785	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
41	30, 40	anbi12d 643	. 2 ⊢ (𝑎 = 𝑐 → (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
42		oveq1 7418	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
43	42	eleq1d 2854	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44		sneq 4604	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
45	44	xpeq1d 5691	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
46	45	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
47	46	sseq1d 3976	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48		xpeq1 5676	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
49	48	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
50	49	sseq1d 3976	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
51	47, 50	anbi12d 643	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
52	51	rabbidv 3430	. . . . 5 ⊢ (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
53	52	inteqd 4921	. . . 4 ⊢ (𝑎 = 𝐴 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
54	42, 53	eqeq12d 2785	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}))
55	43, 54	anbi12d 643	. 2 ⊢ (𝑎 = 𝐴 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})))
56		oveq2 7419	. . . 4 ⊢ (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
57	56	eleq1d 2854	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58		xpeq2 5683	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
59	58	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
60	59	sseq1d 3976	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61		sneq 4604	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
62	61	xpeq2d 5692	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
63	62	imaeq2d 6063	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
64	63	sseq1d 3976	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
65	60, 64	anbi12d 643	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
66	65	rabbidv 3430	. . . . 5 ⊢ (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
67	66	inteqd 4921	. . . 4 ⊢ (𝑏 = 𝐵 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
68	56, 67	eqeq12d 2785	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
69	57, 68	anbi12d 643	. 2 ⊢ (𝑏 = 𝐵 → (((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})))
70		simpl 487	. . . . . 6 ⊢ (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → (𝑐 +no 𝑏) ∈ On)
71	70	ralimi 3108	. . . . 5 ⊢ (∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
72	71	3ad2ant2 1150	. . . 4 ⊢ ((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
73		simpl 487	. . . . . 6 ⊢ (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → (𝑎 +no 𝑑) ∈ On)
74	73	ralimi 3108	. . . . 5 ⊢ (∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
75	74	3ad2ant3 1151	. . . 4 ⊢ ((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
76	72, 75	jca 520	. . 3 ⊢ ((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On))
77		df-nadd 8651	. . . . . . . . 9 ⊢ +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 ‘𝑡)})) ⊆ 𝑥)}))
78	77	on2recsov 8653	. . . . . . . 8 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
79	78	adantr 485	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
80		opex 5446	. . . . . . . 8 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
81		naddfn 8660	. . . . . . . . . 10 ⊢ +no Fn (On × On)
82		fnfun 6636	. . . . . . . . . 10 ⊢ ( +no Fn (On × On) → Fun +no )
83	81, 82	ax-mp 5	. . . . . . . . 9 ⊢ Fun +no
84		vex 3467	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
85	84	sucex 7804	. . . . . . . . . . 11 ⊢ suc 𝑎 ∈ V
86		vex 3467	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
87	86	sucex 7804	. . . . . . . . . . 11 ⊢ suc 𝑏 ∈ V
88	85, 87	xpex 7751	. . . . . . . . . 10 ⊢ (suc 𝑎 × suc 𝑏) ∈ V
89	88	difexi 5301	. . . . . . . . 9 ⊢ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V
90		resfunexg 7214	. . . . . . . . 9 ⊢ ((Fun +no ∧ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V) → ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V)
91	83, 89, 90	mp2an 704	. . . . . . . 8 ⊢ ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V
92		eloni 6371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ On → Ord 𝑏)
93	92	ad2antlr 739	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94		ordirr 6379	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑏 → ¬ 𝑏 ∈ 𝑏)
95	93, 94	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏 ∈ 𝑏)
96	95	olcd 887	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
97		ianor 997	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
98		opelxp 5698	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏))
99	97, 98	xchnxbir 336	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
100	96, 99	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
101	84	sucid 6446	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ suc 𝑎
102		snssi 4756	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎} ⊆ suc 𝑎
104		sssucid 6444	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ⊆ suc 𝑏
105		xpss12 5677	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑎} ⊆ suc 𝑎 ∧ 𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106	103, 104, 105	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107		ssdifsn 4760	. . . . . . . . . . . . . . . 16 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ (({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏)))
108	106, 107	mpbiran 721	. . . . . . . . . . . . . . 15 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
109	100, 108	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
110		resima2 6016	. . . . . . . . . . . . . 14 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
111	109, 110	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
112	111	sseq1d 3976	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113		eloni 6371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ On → Ord 𝑎)
114	113	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115		ordirr 6379	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
116	114, 115	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎 ∈ 𝑎)
117	116	orcd 886	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118		ianor 997	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119		opelxp 5698	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}))
120	118, 119	xchnxbir 336	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121	117, 120	sylibr 237	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122		sssucid 6444	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ⊆ suc 𝑎
123	86	sucid 6446	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ suc 𝑏
124		snssi 4756	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} ⊆ suc 𝑏
126		xpss12 5677	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127	122, 125, 126	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128		ssdifsn 4760	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏})))
129	127, 128	mpbiran 721	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
130	121, 129	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
131		resima2 6016	. . . . . . . . . . . . . 14 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
132	130, 131	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
133	132	sseq1d 3976	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
134	112, 133	anbi12d 643	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)))
135	134	rabbidv 3430	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136	135	inteqd 4921	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
137		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
138		oveq1 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (𝑡 +no 𝑑) = (𝑎 +no 𝑑))
139	138	eleq1d 2854	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140	139	ralbidv 3194	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → (∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On))
141	84, 140	ralsn 4652	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
142	137, 141	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On)
143		snssi 4756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → {𝑎} ⊆ On)
144		onss 7783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → 𝑏 ⊆ On)
145		xpss12 5677	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑎} ⊆ On ∧ 𝑏 ⊆ On) → ({𝑎} × 𝑏) ⊆ (On × On))
146	143, 144, 145	syl2an 607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ({𝑎} × 𝑏) ⊆ (On × On))
147	146	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ (On × On))
148	81	fndmi 6640	. . . . . . . . . . . . . . . . . 18 ⊢ dom +no = (On × On)
149	147, 148	sseqtrrdi 3986	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ dom +no )
150		funimassov 7588	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ⊆ dom +no ) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On))
151	83, 149, 150	sylancr 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On))
152	142, 151	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ On)
153		simprl 782	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
154		oveq2 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑏 → (𝑐 +no 𝑡) = (𝑐 +no 𝑏))
155	154	eleq1d 2854	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
156	86, 155	ralsn 4652	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157	156	ralbii 3117	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
158	153, 157	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159		onss 7783	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
160		snssi 4756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → {𝑏} ⊆ On)
161		xpss12 5677	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ⊆ On ∧ {𝑏} ⊆ On) → (𝑎 × {𝑏}) ⊆ (On × On))
162	159, 160, 161	syl2an 607	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 × {𝑏}) ⊆ (On × On))
163	162	adantr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ (On × On))
164	163, 148	sseqtrrdi 3986	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ dom +no )
165		funimassov 7588	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ⊆ dom +no ) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
166	83, 164, 165	sylancr 598	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
167	158, 166	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ On)
168	152, 167	unssd 4153	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169		ssorduni 7777	. . . . . . . . . . . . . 14 ⊢ ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170	168, 169	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171		vsnex 5407	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎} ∈ V
172	171, 86	xpex 7751	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑎} × 𝑏) ∈ V
173		funimaexg 6623	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
174	83, 172, 173	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ ({𝑎} × 𝑏)) ∈ V
175		vsnex 5407	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑏} ∈ V
176	84, 175	xpex 7751	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 × {𝑏}) ∈ V
177		funimaexg 6623	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
178	83, 176, 177	mp2an 704	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ (𝑎 × {𝑏})) ∈ V
179	174, 178	unex 7742	. . . . . . . . . . . . . . 15 ⊢ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180	179	uniex 7739	. . . . . . . . . . . . . 14 ⊢ ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181	180	elon 6370	. . . . . . . . . . . . 13 ⊢ (∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
182	170, 181	sylibr 237	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
183		onsucb 7812	. . . . . . . . . . . 12 ⊢ (∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
184	182, 183	sylib 221	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
185		onsucuni 7823	. . . . . . . . . . . . 13 ⊢ ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
186	168, 185	syl 18	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
187	186	unssad 4154	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188	186	unssbd 4155	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189		sseq2 3971	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190		sseq2 3971	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
191	189, 190	anbi12d 643	. . . . . . . . . . . 12 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))))
192	191	rspcev 3590	. . . . . . . . . . 11 ⊢ ((suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ∧ (( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
193	184, 187, 188, 192	syl12anc 849	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
194		onintrab2 7795	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
195	193, 194	sylib 221	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
196	136, 195	eqeltrd 2869	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
197	84, 86	op1std 7995	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (1^st ‘𝑡) = 𝑎)
198	197	sneqd 4606	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(1^st ‘𝑡)} = {𝑎})
199	84, 86	op2ndd 7996	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (2^nd ‘𝑡) = 𝑏)
200	198, 199	xpeq12d 5693	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1^st ‘𝑡)} × (2^nd ‘𝑡)) = ({𝑎} × 𝑏))
201	200	imaeq2d 6063	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202	201	sseq1d 3976	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203	199	sneqd 4606	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(2^nd ‘𝑡)} = {𝑏})
204	197, 203	xpeq12d 5693	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((1^st ‘𝑡) × {(2^nd ‘𝑡)}) = (𝑎 × {𝑏}))
205	204	imaeq2d 6063	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206	205	sseq1d 3976	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207	202, 206	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208	207	rabbidv 3430	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209	208	inteqd 4921	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210		imaeq1 6058	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211	210	sseq1d 3976	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212		imaeq1 6058	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213	212	sseq1d 3976	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥))
214	211, 213	anbi12d 643	. . . . . . . . . . 11 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)))
215	214	rabbidv 3430	. . . . . . . . . 10 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216	215	inteqd 4921	. . . . . . . . 9 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
217		eqid 2769	. . . . . . . . 9 ⊢ (𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)}) = (𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})
218	209, 216, 217	ovmpog 7570	. . . . . . . 8 ⊢ ((⟨𝑎, 𝑏⟩ ∈ V ∧ ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V ∧ ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On) → (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))) = ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
219	80, 91, 196, 218	mp3an12i 1491	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))) = ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
220	79, 219, 136	3eqtrd 2808	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
221	220, 195	eqeltrd 2869	. . . . 5 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) ∈ On)
222	221, 220	jca 520	. . . 4 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}))
223	222	ex 417	. . 3 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})))
224	76, 223	syl5 35	. 2 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})))
225	14, 28, 41, 55, 69, 224	on2ind 8654	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ∀wral 3085 ∃wrex 3095 {crab 3423 Vcvv 3463 ∖ cdif 3910 ∪ cun 3911 ⊆ wss 3913 {csn 4594 ⟨cop 4600 ∪ cuni 4876 ∩ cint 4916 × cxp 5660 dom cdm 5662 ↾ cres 5664 “ cima 5665 Ord word 6360 Oncon0 6361 suc csuc 6363 Fun wfun 6531 Fn wfn 6532 ‘cfv 6537 (class class class)co 7411 ∈ cmpo 7413 1^st c1st 7983 2^nd c2nd 7984 +no cnadd 8650

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7985 df-2nd 7986 df-frecs 8277 df-nadd 8651

This theorem is referenced by: naddcl 8662 naddov 8663

W3C validator