Theorem nmulprop 36636

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 7417	. . . 4 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑞) = (𝑟 ·no 𝑞))
2	1	eleq1d 2846	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑞) ∈ On ↔ (𝑟 ·no 𝑞) ∈ On))
3		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑏) = (𝑟 ·no 𝑏))
4	3	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)))
5	4	eleq1d 2846	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
6	5	ralbidv 3186	. . . . . . 7 ⊢ (𝑝 = 𝑟 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
7	6	raleqbi1dv 3331	. . . . . 6 ⊢ (𝑝 = 𝑟 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
8	7	rabbidv 3421	. . . . 5 ⊢ (𝑝 = 𝑟 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
9	8	inteqd 4916	. . . 4 ⊢ (𝑝 = 𝑟 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
10	1, 9	eqeq12d 2777	. . 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 7418	. . . 4 ⊢ (𝑞 = 𝑠 → (𝑟 ·no 𝑞) = (𝑟 ·no 𝑠))
13	12	eleq1d 2846	. . 3 ⊢ (𝑞 = 𝑠 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑟 ·no 𝑠) ∈ On))
14		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑞 = 𝑠 → (𝑎 ·no 𝑞) = (𝑎 ·no 𝑠))
15	14	oveq1d 7425	. . . . . . . . 9 ⊢ (𝑞 = 𝑠 → ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) = ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)))
16	15	eleq1d 2846	. . . . . . . 8 ⊢ (𝑞 = 𝑠 → (((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
17	16	raleqbi1dv 3331	. . . . . . 7 ⊢ (𝑞 = 𝑠 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
18	17	ralbidv 3186	. . . . . 6 ⊢ (𝑞 = 𝑠 → (∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
19	18	rabbidv 3421	. . . . 5 ⊢ (𝑞 = 𝑠 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
20	19	inteqd 4916	. . . 4 ⊢ (𝑞 = 𝑠 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
21	12, 20	eqeq12d 2777	. . 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 7417	. . . 4 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑠) = (𝑟 ·no 𝑠))
24	23	eleq1d 2846	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑟 ·no 𝑠) ∈ On))
25	3	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)))
26	25	eleq1d 2846	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
27	26	ralbidv 3186	. . . . . . 7 ⊢ (𝑝 = 𝑟 → (∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
28	27	raleqbi1dv 3331	. . . . . 6 ⊢ (𝑝 = 𝑟 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
29	28	rabbidv 3421	. . . . 5 ⊢ (𝑝 = 𝑟 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
30	29	inteqd 4916	. . . 4 ⊢ (𝑝 = 𝑟 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
31	23, 30	eqeq12d 2777	. . 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 7417	. . . 4 ⊢ (𝑝 = 𝐴 → (𝑝 ·no 𝑞) = (𝐴 ·no 𝑞))
34	33	eleq1d 2846	. . 3 ⊢ (𝑝 = 𝐴 → ((𝑝 ·no 𝑞) ∈ On ↔ (𝐴 ·no 𝑞) ∈ On))
35		oveq1 7417	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → (𝑝 ·no 𝑏) = (𝐴 ·no 𝑏))
36	35	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)))
37	36	eleq1d 2846	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
38	37	ralbidv 3186	. . . . . . 7 ⊢ (𝑝 = 𝐴 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
39	38	raleqbi1dv 3331	. . . . . 6 ⊢ (𝑝 = 𝐴 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
40	39	rabbidv 3421	. . . . 5 ⊢ (𝑝 = 𝐴 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
41	40	inteqd 4916	. . . 4 ⊢ (𝑝 = 𝐴 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
42	33, 41	eqeq12d 2777	. . 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 7418	. . . 4 ⊢ (𝑞 = 𝐵 → (𝐴 ·no 𝑞) = (𝐴 ·no 𝐵))
45	44	eleq1d 2846	. . 3 ⊢ (𝑞 = 𝐵 → ((𝐴 ·no 𝑞) ∈ On ↔ (𝐴 ·no 𝐵) ∈ On))
46		oveq2 7418	. . . . . . . . . 10 ⊢ (𝑞 = 𝐵 → (𝑎 ·no 𝑞) = (𝑎 ·no 𝐵))
47	46	oveq1d 7425	. . . . . . . . 9 ⊢ (𝑞 = 𝐵 → ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) = ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)))
48	47	eleq1d 2846	. . . . . . . 8 ⊢ (𝑞 = 𝐵 → (((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
49	48	raleqbi1dv 3331	. . . . . . 7 ⊢ (𝑞 = 𝐵 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
50	49	ralbidv 3186	. . . . . 6 ⊢ (𝑞 = 𝐵 → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
51	50	rabbidv 3421	. . . . 5 ⊢ (𝑞 = 𝐵 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
52	51	inteqd 4916	. . . 4 ⊢ (𝑞 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
53	44, 52	eqeq12d 2777	. . 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 3133	. . . 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 3100	. . . 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 3100	. . . 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 36634	. . . . . . . . 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 5445	. . . . . . . 8 ⊢ ⟨𝑝, 𝑞⟩ ∈ V
66		nmulfn 36635	. . . . . . . . . 10 ⊢ ·no Fn (On × On)
67		fnfun 6635	. . . . . . . . . 10 ⊢ ( ·no Fn (On × On) → Fun ·no )
68	66, 67	ax-mp 5	. . . . . . . . 9 ⊢ Fun ·no
69		vex 3457	. . . . . . . . . . . 12 ⊢ 𝑝 ∈ V
70	69	sucex 7804	. . . . . . . . . . 11 ⊢ suc 𝑝 ∈ V
71		vex 3457	. . . . . . . . . . . 12 ⊢ 𝑞 ∈ V
72	71	sucex 7804	. . . . . . . . . . 11 ⊢ suc 𝑞 ∈ V
73	70, 72	xpex 7751	. . . . . . . . . 10 ⊢ (suc 𝑝 × suc 𝑞) ∈ V
74	73	difexi 5300	. . . . . . . . 9 ⊢ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}) ∈ V
75		resfunexg 7213	. . . . . . . . 9 ⊢ ((Fun ·no ∧ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}) ∈ V) → ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V)
76	68, 74, 75	mp2an 704	. . . . . . . 8 ⊢ ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V
77		elelsuc 6436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝑝 → 𝑎 ∈ suc 𝑝)
78	77	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑎 ∈ suc 𝑝)
79	78	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑎 ∈ suc 𝑝)
80	71	sucid 6445	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑞 ∈ suc 𝑞
81	80	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑞 ∈ suc 𝑞)
82	79, 81	opelxpd 5700	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑞⟩ ∈ (suc 𝑝 × suc 𝑞))
83		eloni 6370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ On → Ord 𝑝)
84		ordirr 6378	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑝 → ¬ 𝑝 ∈ 𝑝)
85		elequ1 2148	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑎, 𝑞⟩ ∈ V
94	93	elsn 4603	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑎, 𝑞⟩ = ⟨𝑝, 𝑞⟩)
95		vex 3457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑎 ∈ V
96	95, 71	opth 5458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑞⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑎 = 𝑝 ∧ 𝑞 = 𝑞))
97	94, 96	bitr2i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩})
98	92, 97	sylnib 331	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩})
99	82, 98	eldifd 3915	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑞⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
100	99	fvresd 6901	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑞⟩) = ( ·no ‘⟨𝑎, 𝑞⟩))
101		df-ov 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑞⟩)
102		df-ov 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ·no 𝑞) = ( ·no ‘⟨𝑎, 𝑞⟩)
103	100, 101, 102	3eqtr4g 2821	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) = (𝑎 ·no 𝑞))
104	69	sucid 6445	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑝 ∈ suc 𝑝
105	104	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑝 ∈ suc 𝑝)
106		elelsuc 6436	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ 𝑞 → 𝑏 ∈ suc 𝑞)
107	106	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑏 ∈ suc 𝑞)
108	107	adantl 486	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑏 ∈ suc 𝑞)
109	105, 108	opelxpd 5700	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑝, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
110		eloni 6370	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ On → Ord 𝑞)
111		ordirr 6378	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑞 → ¬ 𝑞 ∈ 𝑞)
112		elequ1 2148	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑝, 𝑏⟩ ∈ V
121	120	elsn 4603	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑝, 𝑏⟩ = ⟨𝑝, 𝑞⟩)
122		vex 3457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑏 ∈ V
123	69, 122	opth 5458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑝, 𝑏⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑝 = 𝑝 ∧ 𝑏 = 𝑞))
124	121, 123	bitr2i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑝 ∧ 𝑏 = 𝑞) ↔ ⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
125	119, 124	sylnib 331	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
126	109, 125	eldifd 3915	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑝, 𝑏⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
127	126	fvresd 6901	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑝, 𝑏⟩) = ( ·no ‘⟨𝑝, 𝑏⟩))
128		df-ov 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑝, 𝑏⟩)
129		df-ov 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ·no 𝑏) = ( ·no ‘⟨𝑝, 𝑏⟩)
130	127, 128, 129	3eqtr4g 2821	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (𝑝 ·no 𝑏))
131	103, 130	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
132		sssucid 6443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑝 ⊆ suc 𝑝
133		sssucid 6443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑞 ⊆ suc 𝑞
134		xpss12 5676	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ⊆ suc 𝑝 ∧ 𝑞 ⊆ suc 𝑞) → (𝑝 × 𝑞) ⊆ (suc 𝑝 × suc 𝑞))
135	132, 133, 134	mp2an 704	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 × 𝑞) ⊆ (suc 𝑝 × suc 𝑞)
136		opelxpi 5698	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → ⟨𝑎, 𝑏⟩ ∈ (𝑝 × 𝑞))
137	135, 136	sselid 3934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → ⟨𝑎, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
138	137	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
139	118	intnand 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑎 = 𝑝 ∧ 𝑏 = 𝑞))
140		opex 5445	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
141	140	elsn 4603	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑝, 𝑞⟩)
142	95, 122	opth 5458	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑎 = 𝑝 ∧ 𝑏 = 𝑞))
143	141, 142	bitr2i 279	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) ↔ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
144	139, 143	sylnib 331	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
145	138, 144	eldifd 3915	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑏⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
146	145	fvresd 6901	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑏⟩) = ( ·no ‘⟨𝑎, 𝑏⟩))
147		df-ov 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑏⟩)
148		df-ov 7413	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ·no 𝑏) = ( ·no ‘⟨𝑎, 𝑏⟩)
149	146, 147, 148	3eqtr4g 2821	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (𝑎 ·no 𝑏))
150	149	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) = (𝑥 +no (𝑎 ·no 𝑏)))
151	131, 150	eleq12d 2855	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
152	151	2ralbidva 3225	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
153	152	rabbidv 3421	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
154	153	inteqd 4916	. . . . . . . . . 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 7417	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (𝑥 +no (𝑎 ·no 𝑏)) = (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
157	156	eleq2d 2847	. . . . . . . . . . . 12 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏))))
158	157	2ralbidv 3227	. . . . . . . . . . 11 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏))))
159		ovex 7443	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ V
160	71, 159	iunex 7964	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ V
161	160	dfiun2 4995	. . . . . . . . . . . . 13 ⊢ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))}
162	159	dfiun2 4995	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))}
163		oveq1 7417	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = 𝑐 → (𝑟 ·no 𝑞) = (𝑐 ·no 𝑞))
164	163	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . . . 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 3581	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑐 ·no 𝑞) ∈ On)
169		oveq2 7418	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑑 → (𝑝 ·no 𝑠) = (𝑝 ·no 𝑑))
170	169	eleq1d 2846	. . . . . . . . . . . . . . . . . . . . . . . 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 3581	. . . . . . . . . . . . . . . . . . . . . . 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 2849	. . . . . . . . . . . . . . . . . . . . . 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 3164	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → (∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
179	178	abssdv 4020	. . . . . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
184		eleq1 2849	. . . . . . . . . . . . . . . . 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 3164	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
187	186	abssdv 4020	. . . . . . . . . . . . . 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 2865	. . . . . . . . . . . 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 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → (∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
205	204	abssdv 4020	. . . . . . . . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . . . . . . . . . . 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 3164	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
210	209	abssdv 4020	. . . . . . . . . . . . . . . . 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 2865	. . . . . . . . . . . . . . 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 7417	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ·no 𝑠) = (𝑎 ·no 𝑠))
215	214	eleq1d 2846	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → ((𝑟 ·no 𝑠) ∈ On ↔ (𝑎 ·no 𝑠) ∈ On))
216		oveq2 7418	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑏 → (𝑎 ·no 𝑠) = (𝑎 ·no 𝑏))
217	216	eleq1d 2846	. . . . . . . . . . . . . . 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 3595	. . . . . . . . . . . . . 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 7417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → (𝑐 ·no 𝑞) = (𝑎 ·no 𝑞))
225	224	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
226	225	iuneq2d 4986	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
227	226	sseq2d 3968	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑))))
228		oveq2 7418	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑏 → (𝑝 ·no 𝑑) = (𝑝 ·no 𝑏))
229	228	oveq2d 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
230	229	sseq2d 3968	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏))))
231		ssidd 3959	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
232	230, 220, 231	rspcedvdw 3583	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∃𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
233		ssiun 5010	. . . . . . . . . . . . . . . . 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 3583	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∃𝑐 ∈ 𝑝 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
236		ssiun 5010	. . . . . . . . . . . . . . 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 7417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝑟 ·no 𝑞) = (𝑎 ·no 𝑞))
241	240	eleq1d 2846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑎 ·no 𝑞) ∈ On))
242	241	rspccva 3579	. . . . . . . . . . . . . . . . 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 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑏 → (𝑝 ·no 𝑠) = (𝑝 ·no 𝑏))
247	246	eleq1d 2846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑏 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑝 ·no 𝑏) ∈ On))
248	247	rspccva 3579	. . . . . . . . . . . . . . . . 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 6453	. . . . . . . . . . . . . . 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 3937	. . . . . . . . . . . 12 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
255	254	ralrimivva 3206	. . . . . . . . . . 11 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
256	158, 193, 255	rspcedvdw 3583	. . . . . . . . . 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 2861	. . . . . . . 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 3856	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → ⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
263	260, 262	csbeq12dv 3861	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
264		oveq1 7417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑝 → (𝑐𝑤𝑏) = (𝑝𝑤𝑏))
265	264	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑝 → ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) = ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)))
266	265	eleq1d 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑝 → (((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
267	266	ralbidv 3186	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑝 → (∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
268	267	raleqbi1dv 3331	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑝 → (∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
269	268	rabbidv 3421	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑝 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
270	269	inteqd 4916	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑝 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
271	270	csbeq2dv 3859	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑝 → ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
272	69, 271	csbie 3887	. . . . . . . . . . 11 ⊢ ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
273		oveq2 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑞 → (𝑎𝑤𝑑) = (𝑎𝑤𝑞))
274	273	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑞 → ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) = ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)))
275	274	eleq1d 2846	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑞 → (((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
276	275	raleqbi1dv 3331	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑞 → (∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
277	276	ralbidv 3186	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑞 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
278	277	rabbidv 3421	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑞 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
279	278	inteqd 4916	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑞 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
280	71, 279	csbie 3887	. . . . . . . . . . 11 ⊢ ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
281	272, 280	eqtri 2784	. . . . . . . . . 10 ⊢ ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
282		oveq 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑎𝑤𝑞) = (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞))
283		oveq 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑝𝑤𝑏) = (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))
284	282, 283	oveq12d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) = ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)))
285		oveq 7416	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑎𝑤𝑏) = (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))
286	285	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑥 +no (𝑎𝑤𝑏)) = (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)))
287	284, 286	eleq12d 2855	. . . . . . . . . . . . 13 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))))
288	287	2ralbidv 3227	. . . . . . . . . . . 12 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))))
289	288	rabbidv 3421	. . . . . . . . . . 11 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
290	289	inteqd 4916	. . . . . . . . . 10 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
291	281, 290	eqtrid 2808	. . . . . . . . 9 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
292		eqid 2761	. . . . . . . . 9 ⊢ (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}) = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
293	263, 291, 292	ovmpog 7569	. . . . . . . 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 1492	. . . . . . 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 2800	. . . . . 6 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
296	295, 258	eqeltrd 2861	. . . . 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 1568   ∈ wcel 2141  {cab 2739  ∀wral 3077  ∃wrex 3087  {crab 3414  Vcvv 3453  ⦋csb 3852   ∖ cdif 3901   ⊆ wss 3904  {csn 4588  ⟨cop 4594  ∪ cuni 4871  ∩ cint 4911  ∪ ciun 4955   × cxp 5659   ↾ cres 5663  Ord word 6359  Oncon0 6360  suc csuc 6362  Fun wfun 6530   Fn wfn 6531  ‘cfv 6536  (class class class)co 7410   ∈ cmpo 7412  1^st c1st 7983  2^nd c2nd 7984   +no cnadd 8650   ·_no cnmul 36633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5237  ax-sep 5256  ax-nul 5268  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-pss 3924  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-int 4912  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7985  df-2nd 7986  df-frecs 8277  df-nadd 8651  df-nmul 36634

This theorem is referenced by:  nmulcl  36637  nmulval  36638