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 8691

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 7422	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
2	1	eleq1d 2814	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3		sneq 4635	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → {𝑎} = {𝑐})
4	3	xpeq1d 5702	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
5	4	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
6	5	sseq1d 4010	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7		xpeq1 5687	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
8	7	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
9	8	sseq1d 4010	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
10	6, 9	anbi12d 631	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
11	10	rabbidv 3436	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
12	11	inteqd 4950	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
13	1, 12	eqeq12d 2744	. . 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 7423	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
16	15	eleq1d 2814	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17		xpeq2 5694	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
18	17	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
19	18	sseq1d 4010	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20		sneq 4635	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → {𝑏} = {𝑑})
21	20	xpeq2d 5703	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
22	21	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
23	22	sseq1d 4010	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
24	19, 23	anbi12d 631	. . . . . 6 ⊢ (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
25	24	rabbidv 3436	. . . . 5 ⊢ (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
26	25	inteqd 4950	. . . 4 ⊢ (𝑏 = 𝑑 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
27	15, 26	eqeq12d 2744	. . 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 7422	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
30	29	eleq1d 2814	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
31	3	xpeq1d 5702	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
32	31	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
33	32	sseq1d 4010	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34		xpeq1 5687	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
35	34	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
36	35	sseq1d 4010	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
37	33, 36	anbi12d 631	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
38	37	rabbidv 3436	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
39	38	inteqd 4950	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
40	29, 39	eqeq12d 2744	. . 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 7422	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
43	42	eleq1d 2814	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44		sneq 4635	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
45	44	xpeq1d 5702	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
46	45	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
47	46	sseq1d 4010	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48		xpeq1 5687	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
49	48	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
50	49	sseq1d 4010	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
51	47, 50	anbi12d 631	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
52	51	rabbidv 3436	. . . . 5 ⊢ (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
53	52	inteqd 4950	. . . 4 ⊢ (𝑎 = 𝐴 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
54	42, 53	eqeq12d 2744	. . 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 7423	. . . 4 ⊢ (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
57	56	eleq1d 2814	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58		xpeq2 5694	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
59	58	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
60	59	sseq1d 4010	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61		sneq 4635	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
62	61	xpeq2d 5703	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
63	62	imaeq2d 6058	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
64	63	sseq1d 4010	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
65	60, 64	anbi12d 631	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
66	65	rabbidv 3436	. . . . 5 ⊢ (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
67	66	inteqd 4950	. . . 4 ⊢ (𝑏 = 𝐵 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
68	56, 67	eqeq12d 2744	. . 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 482	. . . . . 6 ⊢ (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → (𝑐 +no 𝑏) ∈ On)
71	70	ralimi 3079	. . . . 5 ⊢ (∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
72	71	3ad2ant2 1132	. . . 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 3079	. . . . 5 ⊢ (∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
75	74	3ad2ant3 1133	. . . 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 8681	. . . . . . . . 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 8683	. . . . . . . 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 5461	. . . . . . . 8 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
81		naddfn 8690	. . . . . . . . . 10 ⊢ +no Fn (On × On)
82		fnfun 6649	. . . . . . . . . 10 ⊢ ( +no Fn (On × On) → Fun +no )
83	81, 82	ax-mp 5	. . . . . . . . 9 ⊢ Fun +no
84		vex 3474	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
85	84	sucex 7804	. . . . . . . . . . 11 ⊢ suc 𝑎 ∈ V
86		vex 3474	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
87	86	sucex 7804	. . . . . . . . . . 11 ⊢ suc 𝑏 ∈ V
88	85, 87	xpex 7750	. . . . . . . . . 10 ⊢ (suc 𝑎 × suc 𝑏) ∈ V
89	88	difexi 5325	. . . . . . . . 9 ⊢ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V
90		resfunexg 7222	. . . . . . . . 9 ⊢ ((Fun +no ∧ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V) → ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V)
91	83, 89, 90	mp2an 691	. . . . . . . 8 ⊢ ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V
92		eloni 6374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ On → Ord 𝑏)
93	92	ad2antlr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94		ordirr 6382	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑏 → ¬ 𝑏 ∈ 𝑏)
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏 ∈ 𝑏)
96	95	olcd 873	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
97		ianor 980	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
98		opelxp 5709	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏))
99	97, 98	xchnxbir 333	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
100	96, 99	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
101	84	sucid 6446	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ suc 𝑎
102		snssi 4808	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎} ⊆ suc 𝑎
104		sssucid 6444	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ⊆ suc 𝑏
105		xpss12 5688	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑎} ⊆ suc 𝑎 ∧ 𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106	103, 104, 105	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107		ssdifsn 4788	. . . . . . . . . . . . . . . 16 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ (({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏)))
108	106, 107	mpbiran 708	. . . . . . . . . . . . . . 15 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
109	100, 108	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
110		resima2 6015	. . . . . . . . . . . . . 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 4010	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113		eloni 6374	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ On → Ord 𝑎)
114	113	ad2antrr 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115		ordirr 6382	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
116	114, 115	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎 ∈ 𝑎)
117	116	orcd 872	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118		ianor 980	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119		opelxp 5709	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}))
120	118, 119	xchnxbir 333	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121	117, 120	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122		sssucid 6444	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ⊆ suc 𝑎
123	86	sucid 6446	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ suc 𝑏
124		snssi 4808	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} ⊆ suc 𝑏
126		xpss12 5688	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127	122, 125, 126	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128		ssdifsn 4788	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏})))
129	127, 128	mpbiran 708	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
130	121, 129	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
131		resima2 6015	. . . . . . . . . . . . . 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 4010	. . . . . . . . . . . 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 3436	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136	135	inteqd 4950	. . . . . . . . 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 7422	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (𝑡 +no 𝑑) = (𝑎 +no 𝑑))
139	138	eleq1d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140	139	ralbidv 3173	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → (∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On))
141	84, 140	ralsn 4682	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
142	137, 141	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On)
143		snssi 4808	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → {𝑎} ⊆ On)
144		onss 7782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → 𝑏 ⊆ On)
145		xpss12 5688	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑎} ⊆ On ∧ 𝑏 ⊆ On) → ({𝑎} × 𝑏) ⊆ (On × On))
146	143, 144, 145	syl2an 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ({𝑎} × 𝑏) ⊆ (On × On))
147	146	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ (On × On))
148	81	fndmi 6653	. . . . . . . . . . . . . . . . . 18 ⊢ dom +no = (On × On)
149	147, 148	sseqtrrdi 4030	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ dom +no )
150		funimassov 7593	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ⊆ dom +no ) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On))
151	83, 149, 150	sylancr 586	. . . . . . . . . . . . . . . 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 7423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑏 → (𝑐 +no 𝑡) = (𝑐 +no 𝑏))
155	154	eleq1d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
156	86, 155	ralsn 4682	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157	156	ralbii 3089	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
158	153, 157	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159		onss 7782	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
160		snssi 4808	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → {𝑏} ⊆ On)
161		xpss12 5688	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ⊆ On ∧ {𝑏} ⊆ On) → (𝑎 × {𝑏}) ⊆ (On × On))
162	159, 160, 161	syl2an 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 × {𝑏}) ⊆ (On × On))
163	162	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ (On × On))
164	163, 148	sseqtrrdi 4030	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ dom +no )
165		funimassov 7593	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ⊆ dom +no ) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
166	83, 164, 165	sylancr 586	. . . . . . . . . . . . . . . 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 4183	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169		ssorduni 7776	. . . . . . . . . . . . . 14 ⊢ ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170	168, 169	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171		vsnex 5426	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎} ∈ V
172	171, 86	xpex 7750	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑎} × 𝑏) ∈ V
173		funimaexg 6634	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
174	83, 172, 173	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ ({𝑎} × 𝑏)) ∈ V
175		vsnex 5426	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑏} ∈ V
176	84, 175	xpex 7750	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 × {𝑏}) ∈ V
177		funimaexg 6634	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
178	83, 176, 177	mp2an 691	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ (𝑎 × {𝑏})) ∈ V
179	174, 178	unex 7743	. . . . . . . . . . . . . . 15 ⊢ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180	179	uniex 7741	. . . . . . . . . . . . . 14 ⊢ ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181	180	elon 6373	. . . . . . . . . . . . 13 ⊢ (∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
182	170, 181	sylibr 233	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
183		onsucb 7815	. . . . . . . . . . . 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 7826	. . . . . . . . . . . . 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 4184	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188	186	unssbd 4185	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189		sseq2 4005	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190		sseq2 4005	. . . . . . . . . . . . 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 3608	. . . . . . . . . . 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 7795	. . . . . . . . . 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 2829	. . . . . . . 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 4637	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(1^st ‘𝑡)} = {𝑎})
199	84, 86	op2ndd 7999	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (2^nd ‘𝑡) = 𝑏)
200	198, 199	xpeq12d 5704	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1^st ‘𝑡)} × (2^nd ‘𝑡)) = ({𝑎} × 𝑏))
201	200	imaeq2d 6058	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202	201	sseq1d 4010	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203	199	sneqd 4637	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(2^nd ‘𝑡)} = {𝑏})
204	197, 203	xpeq12d 5704	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((1^st ‘𝑡) × {(2^nd ‘𝑡)}) = (𝑎 × {𝑏}))
205	204	imaeq2d 6058	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206	205	sseq1d 4010	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207	202, 206	anbi12d 631	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208	207	rabbidv 3436	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209	208	inteqd 4950	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210		imaeq1 6053	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211	210	sseq1d 4010	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212		imaeq1 6053	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213	212	sseq1d 4010	. . . . . . . . . . . 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 3436	. . . . . . . . . 10 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216	215	inteqd 4950	. . . . . . . . 9 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
217		eqid 2728	. . . . . . . . 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 7575	. . . . . . . 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 1462	. . . . . . 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 2772	. . . . . 6 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
221	220, 195	eqeltrd 2829	. . . . 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 8684	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 846 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ∀wral 3057 ∃wrex 3066 {crab 3428 Vcvv 3470 ∖ cdif 3942 ∪ cun 3943 ⊆ wss 3945 {csn 4625 ⟨cop 4631 ∪ cuni 4904 ∩ cint 4945 × cxp 5671 dom cdm 5673 ↾ cres 5675 “ cima 5676 Ord word 6363 Oncon0 6364 suc csuc 6366 Fun wfun 6537 Fn wfn 6538 ‘cfv 6543 (class class class)co 7415 ∈ cmpo 7417 1^st c1st 7986 2^nd c2nd 7987 +no cnadd 8680

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2699 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5360 ax-pr 5424 ax-un 7735

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3or 1086 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2530 df-eu 2559 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2937 df-ral 3058 df-rex 3067 df-reu 3373 df-rab 3429 df-v 3472 df-sbc 3776 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3964 df-nul 4320 df-if 4526 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4905 df-int 4946 df-iun 4994 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-se 5629 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6300 df-ord 6367 df-on 6368 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-ov 7418 df-oprab 7419 df-mpo 7420 df-1st 7988 df-2nd 7989 df-frecs 8281 df-nadd 8681

This theorem is referenced by: naddcl 8692 naddov 8693

W3C validator

	
		OSZAR »