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 8612

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 7374	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑏) = (𝑐 +no 𝑏))
2	1	eleq1d 2821	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
3		sneq 4577	. . . . . . . . . 10 ⊢ (𝑎 = 𝑐 → {𝑎} = {𝑐})
4	3	xpeq1d 5660	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑏) = ({𝑐} × 𝑏))
5	4	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝑐} × 𝑏)))
6	5	sseq1d 3953	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥))
7		xpeq1 5645	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑏}) = (𝑐 × {𝑏}))
8	7	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝑐 × {𝑏})))
9	8	sseq1d 3953	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥))
10	6, 9	anbi12d 633	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)))
11	10	rabbidv 3396	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
12	11	inteqd 4894	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})
13	1, 12	eqeq12d 2752	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}))
14	2, 13	anbi12d 633	. 2 ⊢ (𝑎 = 𝑐 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)})))
15		oveq2 7375	. . . 4 ⊢ (𝑏 = 𝑑 → (𝑐 +no 𝑏) = (𝑐 +no 𝑑))
16	15	eleq1d 2821	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
17		xpeq2 5652	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → ({𝑐} × 𝑏) = ({𝑐} × 𝑑))
18	17	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ ({𝑐} × 𝑏)) = ( +no “ ({𝑐} × 𝑑)))
19	18	sseq1d 3953	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
20		sneq 4577	. . . . . . . . . 10 ⊢ (𝑏 = 𝑑 → {𝑏} = {𝑑})
21	20	xpeq2d 5661	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (𝑐 × {𝑏}) = (𝑐 × {𝑑}))
22	21	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ( +no “ (𝑐 × {𝑏})) = ( +no “ (𝑐 × {𝑑})))
23	22	sseq1d 3953	. . . . . . 7 ⊢ (𝑏 = 𝑑 → (( +no “ (𝑐 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
24	19, 23	anbi12d 633	. . . . . 6 ⊢ (𝑏 = 𝑑 → ((( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
25	24	rabbidv 3396	. . . . 5 ⊢ (𝑏 = 𝑑 → {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
26	25	inteqd 4894	. . . 4 ⊢ (𝑏 = 𝑑 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
27	15, 26	eqeq12d 2752	. . 3 ⊢ (𝑏 = 𝑑 → ((𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
28	16, 27	anbi12d 633	. 2 ⊢ (𝑏 = 𝑑 → (((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
29		oveq1 7374	. . . 4 ⊢ (𝑎 = 𝑐 → (𝑎 +no 𝑑) = (𝑐 +no 𝑑))
30	29	eleq1d 2821	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) ∈ On ↔ (𝑐 +no 𝑑) ∈ On))
31	3	xpeq1d 5660	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → ({𝑎} × 𝑑) = ({𝑐} × 𝑑))
32	31	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ ({𝑎} × 𝑑)) = ( +no “ ({𝑐} × 𝑑)))
33	32	sseq1d 3953	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ↔ ( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥))
34		xpeq1 5645	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 × {𝑑}) = (𝑐 × {𝑑}))
35	34	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ( +no “ (𝑎 × {𝑑})) = ( +no “ (𝑐 × {𝑑})))
36	35	sseq1d 3953	. . . . . . 7 ⊢ (𝑎 = 𝑐 → (( +no “ (𝑎 × {𝑑})) ⊆ 𝑥 ↔ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥))
37	33, 36	anbi12d 633	. . . . . 6 ⊢ (𝑎 = 𝑐 → ((( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥) ↔ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)))
38	37	rabbidv 3396	. . . . 5 ⊢ (𝑎 = 𝑐 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
39	38	inteqd 4894	. . . 4 ⊢ (𝑎 = 𝑐 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})
40	29, 39	eqeq12d 2752	. . 3 ⊢ (𝑎 = 𝑐 → ((𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)} ↔ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)}))
41	30, 40	anbi12d 633	. 2 ⊢ (𝑎 = 𝑐 → (((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) ↔ ((𝑐 +no 𝑑) ∈ On ∧ (𝑐 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑑})) ⊆ 𝑥)})))
42		oveq1 7374	. . . 4 ⊢ (𝑎 = 𝐴 → (𝑎 +no 𝑏) = (𝐴 +no 𝑏))
43	42	eleq1d 2821	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) ∈ On ↔ (𝐴 +no 𝑏) ∈ On))
44		sneq 4577	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → {𝑎} = {𝐴})
45	44	xpeq1d 5660	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ({𝑎} × 𝑏) = ({𝐴} × 𝑏))
46	45	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ ({𝑎} × 𝑏)) = ( +no “ ({𝐴} × 𝑏)))
47	46	sseq1d 3953	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥))
48		xpeq1 5645	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (𝑎 × {𝑏}) = (𝐴 × {𝑏}))
49	48	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ( +no “ (𝑎 × {𝑏})) = ( +no “ (𝐴 × {𝑏})))
50	49	sseq1d 3953	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥))
51	47, 50	anbi12d 633	. . . . . 6 ⊢ (𝑎 = 𝐴 → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)))
52	51	rabbidv 3396	. . . . 5 ⊢ (𝑎 = 𝐴 → {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
53	52	inteqd 4894	. . . 4 ⊢ (𝑎 = 𝐴 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})
54	42, 53	eqeq12d 2752	. . 3 ⊢ (𝑎 = 𝐴 → ((𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)}))
55	43, 54	anbi12d 633	. 2 ⊢ (𝑎 = 𝐴 → (((𝑎 +no 𝑏) ∈ On ∧ (𝑎 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)}) ↔ ((𝐴 +no 𝑏) ∈ On ∧ (𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)})))
56		oveq2 7375	. . . 4 ⊢ (𝑏 = 𝐵 → (𝐴 +no 𝑏) = (𝐴 +no 𝐵))
57	56	eleq1d 2821	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) ∈ On ↔ (𝐴 +no 𝐵) ∈ On))
58		xpeq2 5652	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ({𝐴} × 𝑏) = ({𝐴} × 𝐵))
59	58	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ ({𝐴} × 𝑏)) = ( +no “ ({𝐴} × 𝐵)))
60	59	sseq1d 3953	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥))
61		sneq 4577	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → {𝑏} = {𝐵})
62	61	xpeq2d 5661	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (𝐴 × {𝑏}) = (𝐴 × {𝐵}))
63	62	imaeq2d 6025	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ( +no “ (𝐴 × {𝑏})) = ( +no “ (𝐴 × {𝐵})))
64	63	sseq1d 3953	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (( +no “ (𝐴 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥))
65	60, 64	anbi12d 633	. . . . . 6 ⊢ (𝑏 = 𝐵 → ((( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)))
66	65	rabbidv 3396	. . . . 5 ⊢ (𝑏 = 𝐵 → {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
67	66	inteqd 4894	. . . 4 ⊢ (𝑏 = 𝐵 → ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})
68	56, 67	eqeq12d 2752	. . 3 ⊢ (𝑏 = 𝐵 → ((𝐴 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝑏})) ⊆ 𝑥)} ↔ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}))
69	57, 68	anbi12d 633	. 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 3074	. . . . 5 ⊢ (∀𝑐 ∈ 𝑎 ((𝑐 +no 𝑏) ∈ On ∧ (𝑐 +no 𝑏) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑐} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑐 × {𝑏})) ⊆ 𝑥)}) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
72	71	3ad2ant2 1135	. . . 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 3074	. . . . 5 ⊢ (∀𝑑 ∈ 𝑏 ((𝑎 +no 𝑑) ∈ On ∧ (𝑎 +no 𝑑) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑑)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑑})) ⊆ 𝑥)}) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
75	74	3ad2ant3 1136	. . . 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 8602	. . . . . . . . 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 8604	. . . . . . . 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 5416	. . . . . . . 8 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
81		naddfn 8611	. . . . . . . . . 10 ⊢ +no Fn (On × On)
82		fnfun 6598	. . . . . . . . . 10 ⊢ ( +no Fn (On × On) → Fun +no )
83	81, 82	ax-mp 5	. . . . . . . . 9 ⊢ Fun +no
84		vex 3433	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
85	84	sucex 7760	. . . . . . . . . . 11 ⊢ suc 𝑎 ∈ V
86		vex 3433	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
87	86	sucex 7760	. . . . . . . . . . 11 ⊢ suc 𝑏 ∈ V
88	85, 87	xpex 7707	. . . . . . . . . 10 ⊢ (suc 𝑎 × suc 𝑏) ∈ V
89	88	difexi 5271	. . . . . . . . 9 ⊢ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V
90		resfunexg 7170	. . . . . . . . 9 ⊢ ((Fun +no ∧ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ∈ V) → ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V)
91	83, 89, 90	mp2an 693	. . . . . . . 8 ⊢ ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) ∈ V
92		eloni 6333	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ On → Ord 𝑏)
93	92	ad2antlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑏)
94		ordirr 6341	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑏 → ¬ 𝑏 ∈ 𝑏)
95	93, 94	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑏 ∈ 𝑏)
96	95	olcd 875	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
97		ianor 984	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
98		opelxp 5667	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (𝑎 ∈ {𝑎} ∧ 𝑏 ∈ 𝑏))
99	97, 98	xchnxbir 333	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏) ↔ (¬ 𝑎 ∈ {𝑎} ∨ ¬ 𝑏 ∈ 𝑏))
100	96, 99	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
101	84	sucid 6407	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑎 ∈ suc 𝑎
102		snssi 4729	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ suc 𝑎 → {𝑎} ⊆ suc 𝑎)
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑎} ⊆ suc 𝑎
104		sssucid 6405	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ⊆ suc 𝑏
105		xpss12 5646	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑎} ⊆ suc 𝑎 ∧ 𝑏 ⊆ suc 𝑏) → ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏))
106	103, 104, 105	mp2an 693	. . . . . . . . . . . . . . . 16 ⊢ ({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏)
107		ssdifsn 4733	. . . . . . . . . . . . . . . 16 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ (({𝑎} × 𝑏) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏)))
108	106, 107	mpbiran 710	. . . . . . . . . . . . . . 15 ⊢ (({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ ({𝑎} × 𝑏))
109	100, 108	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
110		resima2 5981	. . . . . . . . . . . . . 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 3953	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥))
113		eloni 6333	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ On → Ord 𝑎)
114	113	ad2antrr 727	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord 𝑎)
115		ordirr 6341	. . . . . . . . . . . . . . . . . 18 ⊢ (Ord 𝑎 → ¬ 𝑎 ∈ 𝑎)
116	114, 115	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ 𝑎 ∈ 𝑎)
117	116	orcd 874	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
118		ianor 984	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
119		opelxp 5667	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (𝑎 ∈ 𝑎 ∧ 𝑏 ∈ {𝑏}))
120	118, 119	xchnxbir 333	. . . . . . . . . . . . . . . 16 ⊢ (¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}) ↔ (¬ 𝑎 ∈ 𝑎 ∨ ¬ 𝑏 ∈ {𝑏}))
121	117, 120	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
122		sssucid 6405	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ⊆ suc 𝑎
123	86	sucid 6407	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ suc 𝑏
124		snssi 4729	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ suc 𝑏 → {𝑏} ⊆ suc 𝑏)
125	123, 124	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ {𝑏} ⊆ suc 𝑏
126		xpss12 5646	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ⊆ suc 𝑎 ∧ {𝑏} ⊆ suc 𝑏) → (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏))
127	122, 125, 126	mp2an 693	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏)
128		ssdifsn 4733	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑎 × {𝑏}) ⊆ (suc 𝑎 × suc 𝑏) ∧ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏})))
129	127, 128	mpbiran 710	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}) ↔ ¬ ⟨𝑎, 𝑏⟩ ∈ (𝑎 × {𝑏}))
130	121, 129	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩}))
131		resima2 5981	. . . . . . . . . . . . . 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 3953	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
134	112, 133	anbi12d 633	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)))
135	134	rabbidv 3396	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
136	135	inteqd 4894	. . . . . . . . 9 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥)})
137		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
138		oveq1 7374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑎 → (𝑡 +no 𝑑) = (𝑎 +no 𝑑))
139	138	eleq1d 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑎 → ((𝑡 +no 𝑑) ∈ On ↔ (𝑎 +no 𝑑) ∈ On))
140	139	ralbidv 3160	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 = 𝑎 → (∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On))
141	84, 140	ralsn 4625	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On ↔ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)
142	137, 141	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On)
143		snssi 4729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → {𝑎} ⊆ On)
144		onss 7739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → 𝑏 ⊆ On)
145		xpss12 5646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑎} ⊆ On ∧ 𝑏 ⊆ On) → ({𝑎} × 𝑏) ⊆ (On × On))
146	143, 144, 145	syl2an 597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ({𝑎} × 𝑏) ⊆ (On × On))
147	146	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ (On × On))
148	81	fndmi 6602	. . . . . . . . . . . . . . . . . 18 ⊢ dom +no = (On × On)
149	147, 148	sseqtrrdi 3963	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ({𝑎} × 𝑏) ⊆ dom +no )
150		funimassov 7544	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ⊆ dom +no ) → (( +no “ ({𝑎} × 𝑏)) ⊆ On ↔ ∀𝑡 ∈ {𝑎}∀𝑑 ∈ 𝑏 (𝑡 +no 𝑑) ∈ On))
151	83, 149, 150	sylancr 588	. . . . . . . . . . . . . . . 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 771	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
154		oveq2 7375	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑡 = 𝑏 → (𝑐 +no 𝑡) = (𝑐 +no 𝑏))
155	154	eleq1d 2821	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 = 𝑏 → ((𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On))
156	86, 155	ralsn 4625	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ (𝑐 +no 𝑏) ∈ On)
157	156	ralbii 3083	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On ↔ ∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On)
158	153, 157	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On)
159		onss 7739	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ On → 𝑎 ⊆ On)
160		snssi 4729	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ On → {𝑏} ⊆ On)
161		xpss12 5646	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ⊆ On ∧ {𝑏} ⊆ On) → (𝑎 × {𝑏}) ⊆ (On × On))
162	159, 160, 161	syl2an 597	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → (𝑎 × {𝑏}) ⊆ (On × On))
163	162	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ (On × On))
164	163, 148	sseqtrrdi 3963	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (𝑎 × {𝑏}) ⊆ dom +no )
165		funimassov 7544	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ⊆ dom +no ) → (( +no “ (𝑎 × {𝑏})) ⊆ On ↔ ∀𝑐 ∈ 𝑎 ∀𝑡 ∈ {𝑏} (𝑐 +no 𝑡) ∈ On))
166	83, 164, 165	sylancr 588	. . . . . . . . . . . . . . . 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 4132	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On)
169		ssorduni 7733	. . . . . . . . . . . . . 14 ⊢ ((( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ⊆ On → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
170	168, 169	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
171		vsnex 5377	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑎} ∈ V
172	171, 86	xpex 7707	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑎} × 𝑏) ∈ V
173		funimaexg 6585	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ ({𝑎} × 𝑏) ∈ V) → ( +no “ ({𝑎} × 𝑏)) ∈ V)
174	83, 172, 173	mp2an 693	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ ({𝑎} × 𝑏)) ∈ V
175		vsnex 5377	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑏} ∈ V
176	84, 175	xpex 7707	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 × {𝑏}) ∈ V
177		funimaexg 6585	. . . . . . . . . . . . . . . . 17 ⊢ ((Fun +no ∧ (𝑎 × {𝑏}) ∈ V) → ( +no “ (𝑎 × {𝑏})) ∈ V)
178	83, 176, 177	mp2an 693	. . . . . . . . . . . . . . . 16 ⊢ ( +no “ (𝑎 × {𝑏})) ∈ V
179	174, 178	unex 7698	. . . . . . . . . . . . . . 15 ⊢ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
180	179	uniex 7695	. . . . . . . . . . . . . 14 ⊢ ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ V
181	180	elon 6332	. . . . . . . . . . . . 13 ⊢ (∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ↔ Ord ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
182	170, 181	sylibr 234	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On)
183		onsucb 7768	. . . . . . . . . . . 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 7779	. . . . . . . . . . . . 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 4133	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
188	186	unssbd 4134	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))
189		sseq2 3948	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ ( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
190		sseq2 3948	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → (( +no “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏})))))
191	189, 190	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑥 = suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) → ((( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ (( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))))
192	191	rspcev 3564	. . . . . . . . . . 11 ⊢ ((suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∈ On ∧ (( +no “ ({𝑎} × 𝑏)) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))) ∧ ( +no “ (𝑎 × {𝑏})) ⊆ suc ∪ (( +no “ ({𝑎} × 𝑏)) ∪ ( +no “ (𝑎 × {𝑏}))))) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
193	184, 187, 188, 192	syl12anc 837	. . . . . . . . . 10 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∃𝑥 ∈ On (( +no “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ ( +no “ (𝑎 × {𝑏})) ⊆ 𝑥))
194		onintrab2 7751	. . . . . . . . . 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 2836	. . . . . . . 8 ⊢ (((𝑎 ∈ On ∧ 𝑏 ∈ On) ∧ (∀𝑐 ∈ 𝑎 (𝑐 +no 𝑏) ∈ On ∧ ∀𝑑 ∈ 𝑏 (𝑎 +no 𝑑) ∈ On)) → ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)} ∈ On)
197	84, 86	op1std 7952	. . . . . . . . . . . . . . . 16 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (1^st ‘𝑡) = 𝑎)
198	197	sneqd 4579	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(1^st ‘𝑡)} = {𝑎})
199	84, 86	op2ndd 7953	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (2^nd ‘𝑡) = 𝑏)
200	198, 199	xpeq12d 5662	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ({(1^st ‘𝑡)} × (2^nd ‘𝑡)) = ({𝑎} × 𝑏))
201	200	imaeq2d 6025	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) = (𝑓 “ ({𝑎} × 𝑏)))
202	201	sseq1d 3953	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ↔ (𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥))
203	199	sneqd 4579	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {(2^nd ‘𝑡)} = {𝑏})
204	197, 203	xpeq12d 5662	. . . . . . . . . . . . . 14 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((1^st ‘𝑡) × {(2^nd ‘𝑡)}) = (𝑎 × {𝑏}))
205	204	imaeq2d 6025	. . . . . . . . . . . . 13 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) = (𝑓 “ (𝑎 × {𝑏})))
206	205	sseq1d 3953	. . . . . . . . . . . 12 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ((𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥 ↔ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥))
207	202, 206	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥) ↔ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)))
208	207	rabbidv 3396	. . . . . . . . . 10 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
209	208	inteqd 4894	. . . . . . . . 9 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({(1^st ‘𝑡)} × (2^nd ‘𝑡))) ⊆ 𝑥 ∧ (𝑓 “ ((1^st ‘𝑡) × {(2^nd ‘𝑡)})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)})
210		imaeq1 6020	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ ({𝑎} × 𝑏)) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)))
211	210	sseq1d 3953	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥))
212		imaeq1 6020	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (𝑓 “ (𝑎 × {𝑏})) = (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})))
213	212	sseq1d 3953	. . . . . . . . . . . 12 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ((𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥 ↔ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥))
214	211, 213	anbi12d 633	. . . . . . . . . . 11 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → (((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥) ↔ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)))
215	214	rabbidv 3396	. . . . . . . . . 10 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
216	215	inteqd 4894	. . . . . . . . 9 ⊢ (𝑓 = ( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) → ∩ {𝑥 ∈ On ∣ ((𝑓 “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (𝑓 “ (𝑎 × {𝑏})) ⊆ 𝑥)} = ∩ {𝑥 ∈ On ∣ ((( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ ({𝑎} × 𝑏)) ⊆ 𝑥 ∧ (( +no ↾ ((suc 𝑎 × suc 𝑏) ∖ {⟨𝑎, 𝑏⟩})) “ (𝑎 × {𝑏})) ⊆ 𝑥)})
217		eqid 2736	. . . . . . . . 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 7526	. . . . . . . 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 1468	. . . . . . 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 2836	. . . . 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 8605	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 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ∀wral 3051 ∃wrex 3061 {crab 3389 Vcvv 3429 ∖ cdif 3886 ∪ cun 3887 ⊆ wss 3889 {csn 4567 ⟨cop 4573 ∪ cuni 4850 ∩ cint 4889 × cxp 5629 dom cdm 5631 ↾ cres 5633 “ cima 5634 Ord word 6322 Oncon0 6323 suc csuc 6325 Fun wfun 6492 Fn wfn 6493 ‘cfv 6498 (class class class)co 7367 ∈ cmpo 7369 1^st c1st 7940 2^nd c2nd 7941 +no cnadd 8601

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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-ov 7370 df-oprab 7371 df-mpo 7372 df-1st 7942 df-2nd 7943 df-frecs 8231 df-nadd 8602

This theorem is referenced by: naddcl 8613 naddov 8614

W3C validator