Theorem nmulprop 36580

Description: Show closure and value of natural multiplication. (Contributed by Scott Fenton, 2-Jun-2026.)

Assertion

Ref	Expression
nmulprop	⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))

Distinct variable groups:   𝐴,𝑎,𝑏,𝑥   𝐵,𝑎,𝑏,𝑥

Proof of Theorem nmulprop

Dummy variables 𝑐 𝑑 𝑝 𝑞 𝑟 𝑠 𝑡 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7418	. . . 4 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑞) = (𝑟 ·no 𝑞))
2	1	eleq1d 2854	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑞) ∈ On ↔ (𝑟 ·no 𝑞) ∈ On))
3		oveq1 7418	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑏) = (𝑟 ·no 𝑏))
4	3	oveq2d 7427	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)))
5	4	eleq1d 2854	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
6	5	ralbidv 3194	. . . . . . 7 ⊢ (𝑝 = 𝑟 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
7	6	raleqbi1dv 3339	. . . . . 6 ⊢ (𝑝 = 𝑟 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
8	7	rabbidv 3430	. . . . 5 ⊢ (𝑝 = 𝑟 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
9	8	inteqd 4921	. . . 4 ⊢ (𝑝 = 𝑟 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
10	1, 9	eqeq12d 2785	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
11	2, 10	anbi12d 643	. 2 ⊢ (𝑝 = 𝑟 → (((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
12		oveq2 7419	. . . 4 ⊢ (𝑞 = 𝑠 → (𝑟 ·no 𝑞) = (𝑟 ·no 𝑠))
13	12	eleq1d 2854	. . 3 ⊢ (𝑞 = 𝑠 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑟 ·no 𝑠) ∈ On))
14		oveq2 7419	. . . . . . . . . 10 ⊢ (𝑞 = 𝑠 → (𝑎 ·no 𝑞) = (𝑎 ·no 𝑠))
15	14	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑞 = 𝑠 → ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) = ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)))
16	15	eleq1d 2854	. . . . . . . 8 ⊢ (𝑞 = 𝑠 → (((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
17	16	raleqbi1dv 3339	. . . . . . 7 ⊢ (𝑞 = 𝑠 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
18	17	ralbidv 3194	. . . . . 6 ⊢ (𝑞 = 𝑠 → (∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
19	18	rabbidv 3430	. . . . 5 ⊢ (𝑞 = 𝑠 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
20	19	inteqd 4921	. . . 4 ⊢ (𝑞 = 𝑠 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
21	12, 20	eqeq12d 2785	. . 3 ⊢ (𝑞 = 𝑠 → ((𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
22	13, 21	anbi12d 643	. 2 ⊢ (𝑞 = 𝑠 → (((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
23		oveq1 7418	. . . 4 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑠) = (𝑟 ·no 𝑠))
24	23	eleq1d 2854	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑟 ·no 𝑠) ∈ On))
25	3	oveq2d 7427	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)))
26	25	eleq1d 2854	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
27	26	ralbidv 3194	. . . . . . 7 ⊢ (𝑝 = 𝑟 → (∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
28	27	raleqbi1dv 3339	. . . . . 6 ⊢ (𝑝 = 𝑟 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
29	28	rabbidv 3430	. . . . 5 ⊢ (𝑝 = 𝑟 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
30	29	inteqd 4921	. . . 4 ⊢ (𝑝 = 𝑟 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
31	23, 30	eqeq12d 2785	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
32	24, 31	anbi12d 643	. 2 ⊢ (𝑝 = 𝑟 → (((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
33		oveq1 7418	. . . 4 ⊢ (𝑝 = 𝐴 → (𝑝 ·no 𝑞) = (𝐴 ·no 𝑞))
34	33	eleq1d 2854	. . 3 ⊢ (𝑝 = 𝐴 → ((𝑝 ·no 𝑞) ∈ On ↔ (𝐴 ·no 𝑞) ∈ On))
35		oveq1 7418	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → (𝑝 ·no 𝑏) = (𝐴 ·no 𝑏))
36	35	oveq2d 7427	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)))
37	36	eleq1d 2854	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
38	37	ralbidv 3194	. . . . . . 7 ⊢ (𝑝 = 𝐴 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
39	38	raleqbi1dv 3339	. . . . . 6 ⊢ (𝑝 = 𝐴 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
40	39	rabbidv 3430	. . . . 5 ⊢ (𝑝 = 𝐴 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
41	40	inteqd 4921	. . . 4 ⊢ (𝑝 = 𝐴 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
42	33, 41	eqeq12d 2785	. . 3 ⊢ (𝑝 = 𝐴 → ((𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
43	34, 42	anbi12d 643	. 2 ⊢ (𝑝 = 𝐴 → (((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝐴 ·no 𝑞) ∈ On ∧ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
44		oveq2 7419	. . . 4 ⊢ (𝑞 = 𝐵 → (𝐴 ·no 𝑞) = (𝐴 ·no 𝐵))
45	44	eleq1d 2854	. . 3 ⊢ (𝑞 = 𝐵 → ((𝐴 ·no 𝑞) ∈ On ↔ (𝐴 ·no 𝐵) ∈ On))
46		oveq2 7419	. . . . . . . . . 10 ⊢ (𝑞 = 𝐵 → (𝑎 ·no 𝑞) = (𝑎 ·no 𝐵))
47	46	oveq1d 7426	. . . . . . . . 9 ⊢ (𝑞 = 𝐵 → ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) = ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)))
48	47	eleq1d 2854	. . . . . . . 8 ⊢ (𝑞 = 𝐵 → (((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
49	48	raleqbi1dv 3339	. . . . . . 7 ⊢ (𝑞 = 𝐵 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
50	49	ralbidv 3194	. . . . . 6 ⊢ (𝑞 = 𝐵 → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
51	50	rabbidv 3430	. . . . 5 ⊢ (𝑞 = 𝐵 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
52	51	inteqd 4921	. . . 4 ⊢ (𝑞 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
53	44, 52	eqeq12d 2785	. . 3 ⊢ (𝑞 = 𝐵 → ((𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
54	45, 53	anbi12d 643	. 2 ⊢ (𝑞 = 𝐵 → (((𝐴 ·no 𝑞) ∈ On ∧ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
55		simpl 487	. . . . 5 ⊢ (((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → (𝑟 ·no 𝑠) ∈ On)
56	55	2ralimi 3141	. . . 4 ⊢ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → ∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On)
57		simpl 487	. . . . 5 ⊢ (((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → (𝑟 ·no 𝑞) ∈ On)
58	57	ralimi 3108	. . . 4 ⊢ (∀𝑟 ∈ 𝑝 ((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
59		simpl 487	. . . . 5 ⊢ (((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → (𝑝 ·no 𝑠) ∈ On)
60	59	ralimi 3108	. . . 4 ⊢ (∀𝑠 ∈ 𝑞 ((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
61	56, 58, 60	3anim123i 1167	. . 3 ⊢ ((∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ∧ ∀𝑟 ∈ 𝑝 ((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ∧ ∀𝑠 ∈ 𝑞 ((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})) → (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On))
62		df-nmul 36578	. . . . . . . . 9 ⊢ ·no = frecs({⟨𝑡, 𝑢⟩ ∣ (𝑡 ∈ (On × On) ∧ 𝑢 ∈ (On × On) ∧ (((1st ‘𝑡) E (1st ‘𝑢) ∨ (1st ‘𝑡) = (1st ‘𝑢)) ∧ ((2nd ‘𝑡) E (2nd ‘𝑢) ∨ (2nd ‘𝑡) = (2nd ‘𝑢)) ∧ 𝑡 ≠ 𝑢))}, (On × On), (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}))
63	62	on2recsov 8653	. . . . . . . 8 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝 ·no 𝑞) = (⟨𝑝, 𝑞⟩(𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))))
64	63	adantr 485	. . . . . . 7 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) = (⟨𝑝, 𝑞⟩(𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))))
65		opex 5446	. . . . . . . 8 ⊢ ⟨𝑝, 𝑞⟩ ∈ V
66		nmulfn 36579	. . . . . . . . . 10 ⊢ ·no Fn (On × On)
67		fnfun 6636	. . . . . . . . . 10 ⊢ ( ·no Fn (On × On) → Fun ·no )
68	66, 67	ax-mp 5	. . . . . . . . 9 ⊢ Fun ·no
69		vex 3467	. . . . . . . . . . . 12 ⊢ 𝑝 ∈ V
70	69	sucex 7804	. . . . . . . . . . 11 ⊢ suc 𝑝 ∈ V
71		vex 3467	. . . . . . . . . . . 12 ⊢ 𝑞 ∈ V
72	71	sucex 7804	. . . . . . . . . . 11 ⊢ suc 𝑞 ∈ V
73	70, 72	xpex 7751	. . . . . . . . . 10 ⊢ (suc 𝑝 × suc 𝑞) ∈ V
74	73	difexi 5301	. . . . . . . . 9 ⊢ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}) ∈ V
75		resfunexg 7214	. . . . . . . . 9 ⊢ ((Fun ·no ∧ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}) ∈ V) → ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V)
76	68, 74, 75	mp2an 704	. . . . . . . 8 ⊢ ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V
77		elelsuc 6437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝑝 → 𝑎 ∈ suc 𝑝)
78	77	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑎 ∈ suc 𝑝)
79	78	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑎 ∈ suc 𝑝)
80	71	sucid 6446	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑞 ∈ suc 𝑞
81	80	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑞 ∈ suc 𝑞)
82	79, 81	opelxpd 5701	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑞⟩ ∈ (suc 𝑝 × suc 𝑞))
83		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ On → Ord 𝑝)
84		ordirr 6379	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑝 → ¬ 𝑝 ∈ 𝑝)
85		elequ1 2156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑝 → (𝑎 ∈ 𝑝 ↔ 𝑝 ∈ 𝑝))
86	85	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑝 → (¬ 𝑎 ∈ 𝑝 ↔ ¬ 𝑝 ∈ 𝑝))
87	86	biimprcd 253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑝 ∈ 𝑝 → (𝑎 = 𝑝 → ¬ 𝑎 ∈ 𝑝))
88	87	con2d 135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑝 ∈ 𝑝 → (𝑎 ∈ 𝑝 → ¬ 𝑎 = 𝑝))
89	83, 84, 88	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ On → (𝑎 ∈ 𝑝 → ¬ 𝑎 = 𝑝))
90	89	imp 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ On ∧ 𝑎 ∈ 𝑝) → ¬ 𝑎 = 𝑝)
91	90	ad2ant2r 759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ 𝑎 = 𝑝)
92	91	intnanrd 494	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑎 = 𝑝 ∧ 𝑞 = 𝑞))
93		opex 5446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑎, 𝑞⟩ ∈ V
94	93	elsn 4609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑎, 𝑞⟩ = ⟨𝑝, 𝑞⟩)
95		vex 3467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑎 ∈ V
96	95, 71	opth 5459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑞⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑎 = 𝑝 ∧ 𝑞 = 𝑞))
97	94, 96	bitr2i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩})
98	92, 97	sylnib 331	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩})
99	82, 98	eldifd 3924	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑞⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
100	99	fvresd 6902	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑞⟩) = ( ·no ‘⟨𝑎, 𝑞⟩))
101		df-ov 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑞⟩)
102		df-ov 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ·no 𝑞) = ( ·no ‘⟨𝑎, 𝑞⟩)
103	100, 101, 102	3eqtr4g 2829	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) = (𝑎 ·no 𝑞))
104	69	sucid 6446	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑝 ∈ suc 𝑝
105	104	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑝 ∈ suc 𝑝)
106		elelsuc 6437	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ 𝑞 → 𝑏 ∈ suc 𝑞)
107	106	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑏 ∈ suc 𝑞)
108	107	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑏 ∈ suc 𝑞)
109	105, 108	opelxpd 5701	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑝, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
110		eloni 6371	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ On → Ord 𝑞)
111		ordirr 6379	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑞 → ¬ 𝑞 ∈ 𝑞)
112		elequ1 2156	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = 𝑞 → (𝑏 ∈ 𝑞 ↔ 𝑞 ∈ 𝑞))
113	112	notbid 321	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = 𝑞 → (¬ 𝑏 ∈ 𝑞 ↔ ¬ 𝑞 ∈ 𝑞))
114	113	biimprcd 253	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑞 ∈ 𝑞 → (𝑏 = 𝑞 → ¬ 𝑏 ∈ 𝑞))
115	114	con2d 135	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑞 ∈ 𝑞 → (𝑏 ∈ 𝑞 → ¬ 𝑏 = 𝑞))
116	110, 111, 115	3syl 19	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 ∈ On → (𝑏 ∈ 𝑞 → ¬ 𝑏 = 𝑞))
117	116	imp 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑞 ∈ On ∧ 𝑏 ∈ 𝑞) → ¬ 𝑏 = 𝑞)
118	117	ad2ant2l 758	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ 𝑏 = 𝑞)
119	118	intnand 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑝 = 𝑝 ∧ 𝑏 = 𝑞))
120		opex 5446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑝, 𝑏⟩ ∈ V
121	120	elsn 4609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑝, 𝑏⟩ = ⟨𝑝, 𝑞⟩)
122		vex 3467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑏 ∈ V
123	69, 122	opth 5459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑝, 𝑏⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑝 = 𝑝 ∧ 𝑏 = 𝑞))
124	121, 123	bitr2i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑝 ∧ 𝑏 = 𝑞) ↔ ⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
125	119, 124	sylnib 331	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
126	109, 125	eldifd 3924	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑝, 𝑏⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
127	126	fvresd 6902	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑝, 𝑏⟩) = ( ·no ‘⟨𝑝, 𝑏⟩))
128		df-ov 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑝, 𝑏⟩)
129		df-ov 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ·no 𝑏) = ( ·no ‘⟨𝑝, 𝑏⟩)
130	127, 128, 129	3eqtr4g 2829	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (𝑝 ·no 𝑏))
131	103, 130	oveq12d 7429	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
132		sssucid 6444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑝 ⊆ suc 𝑝
133		sssucid 6444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑞 ⊆ suc 𝑞
134		xpss12 5677	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ⊆ suc 𝑝 ∧ 𝑞 ⊆ suc 𝑞) → (𝑝 × 𝑞) ⊆ (suc 𝑝 × suc 𝑞))
135	132, 133, 134	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 × 𝑞) ⊆ (suc 𝑝 × suc 𝑞)
136		opelxpi 5699	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → ⟨𝑎, 𝑏⟩ ∈ (𝑝 × 𝑞))
137	135, 136	sselid 3943	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → ⟨𝑎, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
138	137	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
139	118	intnand 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑎 = 𝑝 ∧ 𝑏 = 𝑞))
140		opex 5446	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
141	140	elsn 4609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑝, 𝑞⟩)
142	95, 122	opth 5459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑎 = 𝑝 ∧ 𝑏 = 𝑞))
143	141, 142	bitr2i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) ↔ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
144	139, 143	sylnib 331	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
145	138, 144	eldifd 3924	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑏⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
146	145	fvresd 6902	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑏⟩) = ( ·no ‘⟨𝑎, 𝑏⟩))
147		df-ov 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑏⟩)
148		df-ov 7414	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ·no 𝑏) = ( ·no ‘⟨𝑎, 𝑏⟩)
149	146, 147, 148	3eqtr4g 2829	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (𝑎 ·no 𝑏))
150	149	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) = (𝑥 +no (𝑎 ·no 𝑏)))
151	131, 150	eleq12d 2863	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
152	151	2ralbidva 3233	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
153	152	rabbidv 3430	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
154	153	inteqd 4921	. . . . . . . . . 10 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
155	154	adantr 485	. . . . . . . . 9 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
156		oveq1 7418	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (𝑥 +no (𝑎 ·no 𝑏)) = (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
157	156	eleq2d 2855	. . . . . . . . . . . 12 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏))))
158	157	2ralbidv 3235	. . . . . . . . . . 11 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏))))
159		ovex 7444	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ V
160	71, 159	iunex 7964	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ V
161	160	dfiun2 5000	. . . . . . . . . . . . 13 ⊢ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))}
162	159	dfiun2 5000	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))}
163		oveq1 7418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = 𝑐 → (𝑟 ·no 𝑞) = (𝑐 ·no 𝑞))
164	163	eleq1d 2854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑟 = 𝑐 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑐 ·no 𝑞) ∈ On))
165		simplr2 1233	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
166	165	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
167		simplr 780	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → 𝑐 ∈ 𝑝)
168	164, 166, 167	rspcdva 3591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑐 ·no 𝑞) ∈ On)
169		oveq2 7419	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑑 → (𝑝 ·no 𝑠) = (𝑝 ·no 𝑑))
170	169	eleq1d 2854	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑑 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑝 ·no 𝑑) ∈ On))
171		simplr3 1234	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
172	171	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
173		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → 𝑑 ∈ 𝑞)
174	170, 172, 173	rspcdva 3591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
175	168, 174	naddcld 8665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
176		eleq1 2857	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (𝑥 ∈ On ↔ ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On))
177	175, 176	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
178	177	rexlimdva 3172	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → (∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
179	178	abssdv 4029	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
180	71	abrexex 7958	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ V
181	180	ssonunii 7779	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On → ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
182	179, 181	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
183	162, 182	eqeltrid 2873	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
184		eleq1 2857	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (𝑥 ∈ On ↔ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On))
185	183, 184	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → (𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
186	185	rexlimdva 3172	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
187	186	abssdv 4029	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
188	69	abrexex 7958	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ V
189	188	ssonunii 7779	. . . . . . . . . . . . . 14 ⊢ ({𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On → ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
190	187, 189	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
191	161, 190	eqeltrid 2873	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
192		onsuc 7808	. . . . . . . . . . . 12 ⊢ (∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
193	191, 192	syl 18	. . . . . . . . . . 11 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
194		simplr2 1233	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
195	164	rspccva 3589	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ 𝑐 ∈ 𝑝) → (𝑐 ·no 𝑞) ∈ On)
196	194, 195	sylan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → (𝑐 ·no 𝑞) ∈ On)
197	196	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑐 ·no 𝑞) ∈ On)
198		simplr3 1234	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
199	198	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
200	170	rspccva 3589	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
201	199, 200	sylan 591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
202	197, 201	naddcld 8665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
203	202, 176	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
204	203	rexlimdva 3172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → (∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
205	204	abssdv 4029	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
206	205, 181	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
207	162, 206	eqeltrid 2873	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
208	207, 184	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → (𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
209	208	rexlimdva 3172	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
210	209	abssdv 4029	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
211	210, 189	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
212	161, 211	eqeltrid 2873	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
213	212, 192	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
214		oveq1 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ·no 𝑠) = (𝑎 ·no 𝑠))
215	214	eleq1d 2854	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → ((𝑟 ·no 𝑠) ∈ On ↔ (𝑎 ·no 𝑠) ∈ On))
216		oveq2 7419	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑏 → (𝑎 ·no 𝑠) = (𝑎 ·no 𝑏))
217	216	eleq1d 2854	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑏 → ((𝑎 ·no 𝑠) ∈ On ↔ (𝑎 ·no 𝑏) ∈ On))
218		simplr1 1232	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On)
219		simprl 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑎 ∈ 𝑝)
220		simprr 784	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑏 ∈ 𝑞)
221	215, 217, 218, 219, 220	rspc2dv 3605	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎 ·no 𝑏) ∈ On)
222		naddword1 8677	. . . . . . . . . . . . . 14 ⊢ ((suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On ∧ (𝑎 ·no 𝑏) ∈ On) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ⊆ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
223	213, 221, 222	syl2anc 595	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ⊆ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
224		oveq1 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → (𝑐 ·no 𝑞) = (𝑎 ·no 𝑞))
225	224	oveq1d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
226	225	iuneq2d 4991	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
227	226	sseq2d 3977	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑))))
228		oveq2 7419	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑏 → (𝑝 ·no 𝑑) = (𝑝 ·no 𝑏))
229	228	oveq2d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
230	229	sseq2d 3977	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏))))
231		ssidd 3968	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
232	230, 220, 231	rspcedvdw 3593	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∃𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
233		ssiun 5015	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
234	232, 233	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
235	227, 219, 234	rspcedvdw 3593	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∃𝑐 ∈ 𝑝 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
236		ssiun 5015	. . . . . . . . . . . . . . 15 ⊢ (∃𝑐 ∈ 𝑝 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
237	235, 236	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
238		simpr2 1212	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
239		simpl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑎 ∈ 𝑝)
240		oveq1 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝑟 ·no 𝑞) = (𝑎 ·no 𝑞))
241	240	eleq1d 2854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑎 ·no 𝑞) ∈ On))
242	241	rspccva 3589	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ 𝑎 ∈ 𝑝) → (𝑎 ·no 𝑞) ∈ On)
243	238, 239, 242	syl2an 607	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎 ·no 𝑞) ∈ On)
244		simpr3 1213	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
245		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑏 ∈ 𝑞)
246		oveq2 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑏 → (𝑝 ·no 𝑠) = (𝑝 ·no 𝑏))
247	246	eleq1d 2854	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑏 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑝 ·no 𝑏) ∈ On))
248	247	rspccva 3589	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On ∧ 𝑏 ∈ 𝑞) → (𝑝 ·no 𝑏) ∈ On)
249	244, 245, 248	syl2an 607	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑝 ·no 𝑏) ∈ On)
250	243, 249	naddcld 8665	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ On)
251		onsssuc 6454	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ On ∧ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On) → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))))
252	250, 212, 251	syl2anc 595	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))))
253	237, 252	mpbid 235	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
254	223, 253	sseldd 3946	. . . . . . . . . . . 12 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
255	254	ralrimivva 3214	. . . . . . . . . . 11 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
256	158, 193, 255	rspcedvdw 3593	. . . . . . . . . 10 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∃𝑥 ∈ On ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)))
257		onintrab2 7795	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ∈ On)
258	256, 257	sylib 221	. . . . . . . . 9 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ∈ On)
259	155, 258	eqeltrd 2869	. . . . . . . 8 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} ∈ On)
260	69, 71	op1std 7995	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → (1st ‘𝑣) = 𝑝)
261	69, 71	op2ndd 7996	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → (2nd ‘𝑣) = 𝑞)
262	261	csbeq1d 3865	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → ⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
263	260, 262	csbeq12dv 3870	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
264		oveq1 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑝 → (𝑐𝑤𝑏) = (𝑝𝑤𝑏))
265	264	oveq2d 7427	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑝 → ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) = ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)))
266	265	eleq1d 2854	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑝 → (((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
267	266	ralbidv 3194	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑝 → (∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
268	267	raleqbi1dv 3339	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑝 → (∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
269	268	rabbidv 3430	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑝 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
270	269	inteqd 4921	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑝 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
271	270	csbeq2dv 3868	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑝 → ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
272	69, 271	csbie 3896	. . . . . . . . . . 11 ⊢ ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
273		oveq2 7419	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑞 → (𝑎𝑤𝑑) = (𝑎𝑤𝑞))
274	273	oveq1d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑞 → ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) = ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)))
275	274	eleq1d 2854	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑞 → (((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
276	275	raleqbi1dv 3339	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑞 → (∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
277	276	ralbidv 3194	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑞 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
278	277	rabbidv 3430	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑞 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
279	278	inteqd 4921	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑞 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
280	71, 279	csbie 3896	. . . . . . . . . . 11 ⊢ ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
281	272, 280	eqtri 2792	. . . . . . . . . 10 ⊢ ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
282		oveq 7417	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑎𝑤𝑞) = (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞))
283		oveq 7417	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑝𝑤𝑏) = (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))
284	282, 283	oveq12d 7429	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) = ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)))
285		oveq 7417	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑎𝑤𝑏) = (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))
286	285	oveq2d 7427	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑥 +no (𝑎𝑤𝑏)) = (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)))
287	284, 286	eleq12d 2863	. . . . . . . . . . . . 13 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))))
288	287	2ralbidv 3235	. . . . . . . . . . . 12 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))))
289	288	rabbidv 3430	. . . . . . . . . . 11 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
290	289	inteqd 4921	. . . . . . . . . 10 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
291	281, 290	eqtrid 2816	. . . . . . . . 9 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
292		eqid 2769	. . . . . . . . 9 ⊢ (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}) = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
293	263, 291, 292	ovmpog 7570	. . . . . . . 8 ⊢ ((⟨𝑝, 𝑞⟩ ∈ V ∧ ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V ∧ ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} ∈ On) → (⟨𝑝, 𝑞⟩(𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
294	65, 76, 259, 293	mp3an12i 1491	. . . . . . 7 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (⟨𝑝, 𝑞⟩(𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
295	64, 294, 155	3eqtrd 2808	. . . . . 6 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
296	295, 258	eqeltrd 2869	. . . . 5 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) ∈ On)
297	296, 295	jca 520	. . . 4 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
298	297	ex 417	. . 3 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On) → ((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
299	61, 298	syl5 35	. 2 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ∧ ∀𝑟 ∈ 𝑝 ((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ∧ ∀𝑠 ∈ 𝑞 ((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})) → ((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
300	11, 22, 32, 43, 54, 299	on2ind 8654	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))

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

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

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

This theorem is referenced by:  nmulcl  36581  nmulval  36582