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 8688

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 7412	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
2	1	eleq1d 2819	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3		sneq 4611	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → {𝑎} = {𝑐})
4	3	xpeq1d 5683	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
5	4	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
6	5	sseq1d 3990	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7		xpeq1 5668	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
8	7	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
9	8	sseq1d 3990	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
10	6, 9	anbi12d 632	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
11	10	rabbidv 3423	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
12	11	inteqd 4927	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
13	1, 12	eqeq12d 2751	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}))
14	2, 13	anbi12d 632	. 2 ⊢ (𝑎 = 𝑐 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})))
15		oveq2 7413	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
16	15	eleq1d 2819	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17		xpeq2 5675	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
18	17	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
19	18	sseq1d 3990	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20		sneq 4611	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → {𝑏} = {𝑑})
21	20	xpeq2d 5684	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
22	21	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
23	22	sseq1d 3990	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
24	19, 23	anbi12d 632	. . . . . 6 ⊢ (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
25	24	rabbidv 3423	. . . . 5 ⊢ (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
26	25	inteqd 4927	. . . 4 ⊢ (𝑏 = 𝑑 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
27	15, 26	eqeq12d 2751	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
28	16, 27	anbi12d 632	. 2 ⊢ (𝑏 = 𝑑 → (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
29		oveq1 7412	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
30	29	eleq1d 2819	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
31	3	xpeq1d 5683	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
32	31	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
33	32	sseq1d 3990	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34		xpeq1 5668	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
35	34	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
36	35	sseq1d 3990	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
37	33, 36	anbi12d 632	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
38	37	rabbidv 3423	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
39	38	inteqd 4927	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
40	29, 39	eqeq12d 2751	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
41	30, 40	anbi12d 632	. 2 ⊢ (𝑎 = 𝑐 → (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
42		oveq1 7412	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
43	42	eleq1d 2819	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44		sneq 4611	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
45	44	xpeq1d 5683	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
46	45	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
47	46	sseq1d 3990	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48		xpeq1 5668	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
49	48	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
50	49	sseq1d 3990	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
51	47, 50	anbi12d 632	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
52	51	rabbidv 3423	. . . . 5 ⊢ (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
53	52	inteqd 4927	. . . 4 ⊢ (𝑎 = 𝐴 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
54	42, 53	eqeq12d 2751	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}))
55	43, 54	anbi12d 632	. 2 ⊢ (𝑎 = 𝐴 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})))
56		oveq2 7413	. . . 4 ⊢ (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
57	56	eleq1d 2819	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58		xpeq2 5675	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
59	58	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
60	59	sseq1d 3990	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61		sneq 4611	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
62	61	xpeq2d 5684	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
63	62	imaeq2d 6047	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
64	63	sseq1d 3990	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
65	60, 64	anbi12d 632	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
66	65	rabbidv 3423	. . . . 5 ⊢ (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
67	66	inteqd 4927	. . . 4 ⊢ (𝑏 = 𝐵 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
68	56, 67	eqeq12d 2751	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
69	57, 68	anbi12d 632	. 2 ⊢ (𝑏 = 𝐵 → (((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})))
70		simpl 482	. . . . . 6 ⊢ (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → (𝑐 +no 𝑏) ∈ On)
71	70	ralimi 3073	. . . . 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 482	. . . . . 6 ⊢ (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → (𝑎 +no 𝑑) ∈ On)
74	73	ralimi 3073	. . . . 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 511	. . 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 8678	. . . . . . . . 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 8680	. . . . . . . 8 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
79	78	adantr 480	. . . . . . 7 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = (⟨𝑎, 𝑏⟩(𝑡 ∈ V, 𝑓 ∈ V ↦ ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)})( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))))
80		opex 5439	. . . . . . . 8 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
81		naddfn 8687	. . . . . . . . . 10 ⊢ +no Fn (On × On)
82		fnfun 6638	. . . . . . . . . 10 ⊢ ( +no Fn (On × On) → Fun +no )
83	81, 82	ax-mp 5	. . . . . . . . 9 ⊢ Fun +no
84		vex 3463	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
85	84	sucex 7800	. . . . . . . . . . 11 ⊢ suc 𝑎 ∈ V
86		vex 3463	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
87	86	sucex 7800	. . . . . . . . . . 11 ⊢ suc 𝑏 ∈ V
88	85, 87	xpex 7747	. . . . . . . . . 10 ⊢ (suc 𝑎 × suc 𝑏) ∈ V
89	88	difexi 5300	. . . . . . . . 9 ⊢ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V
90		resfunexg 7207	. . . . . . . . 9 ⊢ ((Fun +no ∧ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V) → ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V)
91	83, 89, 90	mp2an 692	. . . . . . . 8 ⊢ ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V
92		eloni 6362	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ On → Ord 𝑏)
93	92	ad2antlr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94		ordirr 6370	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑏 → ¬ 𝑏 ∈ 𝑏)
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏 ∈ 𝑏)
96	95	olcd 874	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
97		ianor 983	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
98		opelxp 5690	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏))
99	97, 98	xchnxbir 333	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
100	96, 99	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
101	84	sucid 6436	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ suc 𝑎
102		snssi 4784	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎} ⊆ suc 𝑎
104		sssucid 6434	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ⊆ suc 𝑏
105		xpss12 5669	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑎} ⊆ suc 𝑎 ∧ 𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106	103, 104, 105	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107		ssdifsn 4764	. . . . . . . . . . . . . . . 16 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ (({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏)))
108	106, 107	mpbiran 709	. . . . . . . . . . . . . . 15 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
109	100, 108	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
110		resima2 6003	. . . . . . . . . . . . . 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 3990	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113		eloni 6362	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ On → Ord 𝑎)
114	113	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115		ordirr 6370	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
116	114, 115	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎 ∈ 𝑎)
117	116	orcd 873	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118		ianor 983	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119		opelxp 5690	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}))
120	118, 119	xchnxbir 333	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121	117, 120	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122		sssucid 6434	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ⊆ suc 𝑎
123	86	sucid 6436	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ suc 𝑏
124		snssi 4784	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} ⊆ suc 𝑏
126		xpss12 5669	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127	122, 125, 126	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128		ssdifsn 4764	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏})))
129	127, 128	mpbiran 709	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
130	121, 129	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
131		resima2 6003	. . . . . . . . . . . . . 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 3990	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
134	112, 133	anbi12d 632	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)))
135	134	rabbidv 3423	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136	135	inteqd 4927	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
137		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
138		oveq1 7412	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (𝑡 +no 𝑑) = (𝑎 +no 𝑑))
139	138	eleq1d 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140	139	ralbidv 3163	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → (∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On))
141	84, 140	ralsn 4657	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
142	137, 141	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On)
143		snssi 4784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → {𝑎} ⊆ On)
144		onss 7779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → 𝑏 ⊆ On)
145		xpss12 5669	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑎} ⊆ On ∧ 𝑏 ⊆ On) → ({𝑎} × 𝑏) ⊆ (On × On))
146	143, 144, 145	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ({𝑎} × 𝑏) ⊆ (On × On))
147	146	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ (On × On))
148	81	fndmi 6642	. . . . . . . . . . . . . . . . . 18 ⊢ dom +no = (On × On)
149	147, 148	sseqtrrdi 4000	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ dom +no )
150		funimassov 7584	. . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ On)
153		simprl 770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
154		oveq2 7413	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑏 → (𝑐 +no 𝑡) = (𝑐 +no 𝑏))
155	154	eleq1d 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
156	86, 155	ralsn 4657	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157	156	ralbii 3082	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
158	153, 157	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159		onss 7779	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
160		snssi 4784	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → {𝑏} ⊆ On)
161		xpss12 5669	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ⊆ On ∧ {𝑏} ⊆ On) → (𝑎 × {𝑏}) ⊆ (On × On))
162	159, 160, 161	syl2an 596	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 × {𝑏}) ⊆ (On × On))
163	162	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ (On × On))
164	163, 148	sseqtrrdi 4000	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ dom +no )
165		funimassov 7584	. . . . . . . . . . . . . . . . 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 257	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ On)
168	152, 167	unssd 4167	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169		ssorduni 7773	. . . . . . . . . . . . . 14 ⊢ ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170	168, 169	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171		vsnex 5404	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎} ∈ V
172	171, 86	xpex 7747	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑎} × 𝑏) ∈ V
173		funimaexg 6623	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
174	83, 172, 173	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ ({𝑎} × 𝑏)) ∈ V
175		vsnex 5404	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑏} ∈ V
176	84, 175	xpex 7747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 × {𝑏}) ∈ V
177		funimaexg 6623	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
178	83, 176, 177	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ (𝑎 × {𝑏})) ∈ V
179	174, 178	unex 7738	. . . . . . . . . . . . . . 15 ⊢ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180	179	uniex 7735	. . . . . . . . . . . . . 14 ⊢ ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181	180	elon 6361	. . . . . . . . . . . . 13 ⊢ (∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
182	170, 181	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
183		onsucb 7811	. . . . . . . . . . . 12 ⊢ (∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
184	182, 183	sylib 218	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
185		onsucuni 7822	. . . . . . . . . . . . 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 4168	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188	186	unssbd 4169	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189		sseq2 3985	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190		sseq2 3985	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
191	189, 190	anbi12d 632	. . . . . . . . . . . 12 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))))
192	191	rspcev 3601	. . . . . . . . . . 11 ⊢ ((suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ∧ (( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
193	184, 187, 188, 192	syl12anc 836	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
194		onintrab2 7791	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
195	193, 194	sylib 218	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
196	136, 195	eqeltrd 2834	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
197	84, 86	op1std 7998	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (1^st ‘𝑡) = 𝑎)
198	197	sneqd 4613	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(1^st ‘𝑡)} = {𝑎})
199	84, 86	op2ndd 7999	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (2^nd ‘𝑡) = 𝑏)
200	198, 199	xpeq12d 5685	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1^st ‘𝑡)} × (2^nd ‘𝑡)) = ({𝑎} × 𝑏))
201	200	imaeq2d 6047	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202	201	sseq1d 3990	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203	199	sneqd 4613	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(2^nd ‘𝑡)} = {𝑏})
204	197, 203	xpeq12d 5685	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((1^st ‘𝑡) × {(2^nd ‘𝑡)}) = (𝑎 × {𝑏}))
205	204	imaeq2d 6047	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206	205	sseq1d 3990	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207	202, 206	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208	207	rabbidv 3423	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209	208	inteqd 4927	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210		imaeq1 6042	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211	210	sseq1d 3990	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212		imaeq1 6042	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213	212	sseq1d 3990	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥))
214	211, 213	anbi12d 632	. . . . . . . . . . 11 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)))
215	214	rabbidv 3423	. . . . . . . . . 10 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216	215	inteqd 4927	. . . . . . . . 9 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
217		eqid 2735	. . . . . . . . 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 7566	. . . . . . . 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 1467	. . . . . . 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 2774	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
221	220, 195	eqeltrd 2834	. . . . 5 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) ∈ On)
222	221, 220	jca 511	. . . 4 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}))
223	222	ex 412	. . 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 8681	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2108 ∀wral 3051 ∃wrex 3060 {crab 3415 Vcvv 3459 ∖ cdif 3923 ∪ cun 3924 ⊆ wss 3926 {csn 4601 ⟨cop 4607 ∪ cuni 4883 ∩ cint 4922 × cxp 5652 dom cdm 5654 ↾ cres 5656 “ cima 5657 Ord word 6351 Oncon0 6352 suc csuc 6354 Fun wfun 6525 Fn wfn 6526 ‘cfv 6531 (class class class)co 7405 ∈ cmpo 7407 1^st c1st 7986 2^nd c2nd 7987 +no cnadd 8677

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7408 df-oprab 7409 df-mpo 7410 df-1st 7988 df-2nd 7989 df-frecs 8280 df-nadd 8678

This theorem is referenced by: naddcl 8689 naddov 8690

W3C validator