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 8627

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 7369	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
2	1	eleq1d 2817	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3		sneq 4601	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → {𝑎} = {𝑐})
4	3	xpeq1d 5667	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
5	4	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
6	5	sseq1d 3978	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7		xpeq1 5652	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
8	7	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
9	8	sseq1d 3978	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
10	6, 9	anbi12d 631	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
11	10	rabbidv 3413	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
12	11	inteqd 4917	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
13	1, 12	eqeq12d 2747	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}))
14	2, 13	anbi12d 631	. 2 ⊢ (𝑎 = 𝑐 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})))
15		oveq2 7370	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
16	15	eleq1d 2817	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17		xpeq2 5659	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
18	17	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
19	18	sseq1d 3978	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20		sneq 4601	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → {𝑏} = {𝑑})
21	20	xpeq2d 5668	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
22	21	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
23	22	sseq1d 3978	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
24	19, 23	anbi12d 631	. . . . . 6 ⊢ (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
25	24	rabbidv 3413	. . . . 5 ⊢ (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
26	25	inteqd 4917	. . . 4 ⊢ (𝑏 = 𝑑 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
27	15, 26	eqeq12d 2747	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
28	16, 27	anbi12d 631	. 2 ⊢ (𝑏 = 𝑑 → (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
29		oveq1 7369	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
30	29	eleq1d 2817	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
31	3	xpeq1d 5667	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
32	31	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
33	32	sseq1d 3978	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34		xpeq1 5652	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
35	34	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
36	35	sseq1d 3978	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
37	33, 36	anbi12d 631	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
38	37	rabbidv 3413	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
39	38	inteqd 4917	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
40	29, 39	eqeq12d 2747	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
41	30, 40	anbi12d 631	. 2 ⊢ (𝑎 = 𝑐 → (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
42		oveq1 7369	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
43	42	eleq1d 2817	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44		sneq 4601	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
45	44	xpeq1d 5667	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
46	45	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
47	46	sseq1d 3978	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48		xpeq1 5652	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
49	48	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
50	49	sseq1d 3978	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
51	47, 50	anbi12d 631	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
52	51	rabbidv 3413	. . . . 5 ⊢ (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
53	52	inteqd 4917	. . . 4 ⊢ (𝑎 = 𝐴 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
54	42, 53	eqeq12d 2747	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}))
55	43, 54	anbi12d 631	. 2 ⊢ (𝑎 = 𝐴 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})))
56		oveq2 7370	. . . 4 ⊢ (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
57	56	eleq1d 2817	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58		xpeq2 5659	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
59	58	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
60	59	sseq1d 3978	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61		sneq 4601	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
62	61	xpeq2d 5668	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
63	62	imaeq2d 6018	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
64	63	sseq1d 3978	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
65	60, 64	anbi12d 631	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
66	65	rabbidv 3413	. . . . 5 ⊢ (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
67	66	inteqd 4917	. . . 4 ⊢ (𝑏 = 𝐵 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
68	56, 67	eqeq12d 2747	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
69	57, 68	anbi12d 631	. 2 ⊢ (𝑏 = 𝐵 → (((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})))
70		simpl 483	. . . . . 6 ⊢ (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → (𝑐 +no 𝑏) ∈ On)
71	70	ralimi 3082	. . . . 5 ⊢ (∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
72	71	3ad2ant2 1134	. . . 4 ⊢ ((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}) ∧ ∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ∧ ∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)})) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
73		simpl 483	. . . . . 6 ⊢ (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → (𝑎 +no 𝑑) ∈ On)
74	73	ralimi 3082	. . . . 5 ⊢ (∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
75	74	3ad2ant3 1135	. . . 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 512	. . 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 8617	. . . . . . . . 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 8619	. . . . . . . 8 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
79	78	adantr 481	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
80		opex 5426	. . . . . . . 8 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
81		naddfn 8626	. . . . . . . . . 10 ⊢ +no Fn (On × On)
82		fnfun 6607	. . . . . . . . . 10 ⊢ ( +no Fn (On × On) → Fun +no )
83	81, 82	ax-mp 5	. . . . . . . . 9 ⊢ Fun +no
84		vex 3450	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
85	84	sucex 7746	. . . . . . . . . . 11 ⊢ suc 𝑎 ∈ V
86		vex 3450	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
87	86	sucex 7746	. . . . . . . . . . 11 ⊢ suc 𝑏 ∈ V
88	85, 87	xpex 7692	. . . . . . . . . 10 ⊢ (suc 𝑎 × suc 𝑏) ∈ V
89	88	difexi 5290	. . . . . . . . 9 ⊢ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V
90		resfunexg 7170	. . . . . . . . 9 ⊢ ((Fun +no ∧ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V) → ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V)
91	83, 89, 90	mp2an 690	. . . . . . . 8 ⊢ ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V
92		eloni 6332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ On → Ord 𝑏)
93	92	ad2antlr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94		ordirr 6340	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑏 → ¬ 𝑏 ∈ 𝑏)
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏 ∈ 𝑏)
96	95	olcd 872	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
97		ianor 980	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
98		opelxp 5674	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏))
99	97, 98	xchnxbir 332	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
100	96, 99	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
101	84	sucid 6404	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ suc 𝑎
102		snssi 4773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎} ⊆ suc 𝑎
104		sssucid 6402	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ⊆ suc 𝑏
105		xpss12 5653	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑎} ⊆ suc 𝑎 ∧ 𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106	103, 104, 105	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107		ssdifsn 4753	. . . . . . . . . . . . . . . 16 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ (({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏)))
108	106, 107	mpbiran 707	. . . . . . . . . . . . . . 15 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
109	100, 108	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
110		resima2 5977	. . . . . . . . . . . . . 14 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
111	109, 110	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) = ( +no “ ({𝑎} × 𝑏)))
112	111	sseq1d 3978	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113		eloni 6332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ On → Ord 𝑎)
114	113	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115		ordirr 6340	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
116	114, 115	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎 ∈ 𝑎)
117	116	orcd 871	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118		ianor 980	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119		opelxp 5674	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}))
120	118, 119	xchnxbir 332	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121	117, 120	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122		sssucid 6402	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ⊆ suc 𝑎
123	86	sucid 6404	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ suc 𝑏
124		snssi 4773	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} ⊆ suc 𝑏
126		xpss12 5653	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127	122, 125, 126	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128		ssdifsn 4753	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏})))
129	127, 128	mpbiran 707	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
130	121, 129	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
131		resima2 5977	. . . . . . . . . . . . . 14 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
132	130, 131	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) = ( +no “ (𝑎 × {𝑏})))
133	132	sseq1d 3978	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
134	112, 133	anbi12d 631	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)))
135	134	rabbidv 3413	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136	135	inteqd 4917	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
137		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
138		oveq1 7369	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (𝑡 +no 𝑑) = (𝑎 +no 𝑑))
139	138	eleq1d 2817	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140	139	ralbidv 3170	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → (∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On))
141	84, 140	ralsn 4647	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
142	137, 141	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On)
143		snssi 4773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → {𝑎} ⊆ On)
144		onss 7724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → 𝑏 ⊆ On)
145		xpss12 5653	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑎} ⊆ On ∧ 𝑏 ⊆ On) → ({𝑎} × 𝑏) ⊆ (On × On))
146	143, 144, 145	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ({𝑎} × 𝑏) ⊆ (On × On))
147	146	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ (On × On))
148	81	fndmi 6611	. . . . . . . . . . . . . . . . . 18 ⊢ dom +no = (On × On)
149	147, 148	sseqtrrdi 3998	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ dom +no )
150		funimassov 7536	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ⊆ dom +no ) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On))
151	83, 149, 150	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On))
152	142, 151	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ On)
153		simprl 769	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
154		oveq2 7370	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑏 → (𝑐 +no 𝑡) = (𝑐 +no 𝑏))
155	154	eleq1d 2817	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
156	86, 155	ralsn 4647	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157	156	ralbii 3092	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
158	153, 157	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159		onss 7724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
160		snssi 4773	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → {𝑏} ⊆ On)
161		xpss12 5653	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ⊆ On ∧ {𝑏} ⊆ On) → (𝑎 × {𝑏}) ⊆ (On × On))
162	159, 160, 161	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 × {𝑏}) ⊆ (On × On))
163	162	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ (On × On))
164	163, 148	sseqtrrdi 3998	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ dom +no )
165		funimassov 7536	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ⊆ dom +no ) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
166	83, 164, 165	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
167	158, 166	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ On)
168	152, 167	unssd 4151	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169		ssorduni 7718	. . . . . . . . . . . . . 14 ⊢ ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170	168, 169	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171		vsnex 5391	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎} ∈ V
172	171, 86	xpex 7692	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑎} × 𝑏) ∈ V
173		funimaexg 6592	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
174	83, 172, 173	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ ({𝑎} × 𝑏)) ∈ V
175		vsnex 5391	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑏} ∈ V
176	84, 175	xpex 7692	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 × {𝑏}) ∈ V
177		funimaexg 6592	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
178	83, 176, 177	mp2an 690	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ (𝑎 × {𝑏})) ∈ V
179	174, 178	unex 7685	. . . . . . . . . . . . . . 15 ⊢ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180	179	uniex 7683	. . . . . . . . . . . . . 14 ⊢ ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181	180	elon 6331	. . . . . . . . . . . . 13 ⊢ (∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
182	170, 181	sylibr 233	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
183		onsucb 7757	. . . . . . . . . . . 12 ⊢ (∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
184	182, 183	sylib 217	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
185		onsucuni 7768	. . . . . . . . . . . . 13 ⊢ ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
186	168, 185	syl 17	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
187	186	unssad 4152	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188	186	unssbd 4153	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189		sseq2 3973	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190		sseq2 3973	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
191	189, 190	anbi12d 631	. . . . . . . . . . . 12 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))))
192	191	rspcev 3582	. . . . . . . . . . 11 ⊢ ((suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ∧ (( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
193	184, 187, 188, 192	syl12anc 835	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
194		onintrab2 7737	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
195	193, 194	sylib 217	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
196	136, 195	eqeltrd 2832	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
197	84, 86	op1std 7936	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (1^st ‘𝑡) = 𝑎)
198	197	sneqd 4603	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(1^st ‘𝑡)} = {𝑎})
199	84, 86	op2ndd 7937	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (2^nd ‘𝑡) = 𝑏)
200	198, 199	xpeq12d 5669	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1^st ‘𝑡)} × (2^nd ‘𝑡)) = ({𝑎} × 𝑏))
201	200	imaeq2d 6018	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202	201	sseq1d 3978	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203	199	sneqd 4603	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(2^nd ‘𝑡)} = {𝑏})
204	197, 203	xpeq12d 5669	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((1^st ‘𝑡) × {(2^nd ‘𝑡)}) = (𝑎 × {𝑏}))
205	204	imaeq2d 6018	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206	205	sseq1d 3978	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207	202, 206	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208	207	rabbidv 3413	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209	208	inteqd 4917	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210		imaeq1 6013	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211	210	sseq1d 3978	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212		imaeq1 6013	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213	212	sseq1d 3978	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥))
214	211, 213	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)))
215	214	rabbidv 3413	. . . . . . . . . 10 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216	215	inteqd 4917	. . . . . . . . 9 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
217		eqid 2731	. . . . . . . . 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 7519	. . . . . . . 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 1465	. . . . . . 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 2775	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
221	220, 195	eqeltrd 2832	. . . . 5 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) ∈ On)
222	221, 220	jca 512	. . . 4 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}))
223	222	ex 413	. . 3 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})))
224	76, 223	syl5 34	. 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 8620	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∀wral 3060 ∃wrex 3069 {crab 3405 Vcvv 3446 ∖ cdif 3910 ∪ cun 3911 ⊆ wss 3913 {csn 4591 ⟨cop 4597 ∪ cuni 4870 ∩ cint 4912 × cxp 5636 dom cdm 5638 ↾ cres 5640 “ cima 5641 Ord word 6321 Oncon0 6322 suc csuc 6324 Fun wfun 6495 Fn wfn 6496 ‘cfv 6501 (class class class)co 7362 ∈ cmpo 7364 1^st c1st 7924 2^nd c2nd 7925 +no cnadd 8616

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-rep 5247 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3352 df-rab 3406 df-v 3448 df-sbc 3743 df-csb 3859 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3932 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-int 4913 df-iun 4961 df-br 5111 df-opab 5173 df-mpt 5194 df-tr 5228 df-id 5536 df-eprel 5542 df-po 5550 df-so 5551 df-fr 5593 df-se 5594 df-we 5595 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6258 df-ord 6325 df-on 6326 df-suc 6328 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-ov 7365 df-oprab 7366 df-mpo 7367 df-1st 7926 df-2nd 7927 df-frecs 8217 df-nadd 8617

This theorem is referenced by: naddcl 8628 naddov 8629

W3C validator