Theorem nmulprop 36545

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 7403	. . . 4 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑞) = (𝑟 ·no 𝑞))
2	1	eleq1d 2848	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑞) ∈ On ↔ (𝑟 ·no 𝑞) ∈ On))
3		oveq1 7403	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑏) = (𝑟 ·no 𝑏))
4	3	oveq2d 7412	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)))
5	4	eleq1d 2848	. . . . . . . 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 3422	. . . . 5 ⊢ (𝑝 = 𝑟 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
9	8	inteqd 4911	. . . 4 ⊢ (𝑝 = 𝑟 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
10	1, 9	eqeq12d 2779	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
11	2, 10	anbi12d 641	. 2 ⊢ (𝑝 = 𝑟 → (((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
12		oveq2 7404	. . . 4 ⊢ (𝑞 = 𝑠 → (𝑟 ·no 𝑞) = (𝑟 ·no 𝑠))
13	12	eleq1d 2848	. . 3 ⊢ (𝑞 = 𝑠 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑟 ·no 𝑠) ∈ On))
14		oveq2 7404	. . . . . . . . . 10 ⊢ (𝑞 = 𝑠 → (𝑎 ·no 𝑞) = (𝑎 ·no 𝑠))
15	14	oveq1d 7411	. . . . . . . . 9 ⊢ (𝑞 = 𝑠 → ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) = ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)))
16	15	eleq1d 2848	. . . . . . . 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 3422	. . . . 5 ⊢ (𝑞 = 𝑠 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
20	19	inteqd 4911	. . . 4 ⊢ (𝑞 = 𝑠 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
21	12, 20	eqeq12d 2779	. . 3 ⊢ (𝑞 = 𝑠 → ((𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
22	13, 21	anbi12d 641	. 2 ⊢ (𝑞 = 𝑠 → (((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
23		oveq1 7403	. . . 4 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑠) = (𝑟 ·no 𝑠))
24	23	eleq1d 2848	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑟 ·no 𝑠) ∈ On))
25	3	oveq2d 7412	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)))
26	25	eleq1d 2848	. . . . . . . 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 3422	. . . . 5 ⊢ (𝑝 = 𝑟 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
30	29	inteqd 4911	. . . 4 ⊢ (𝑝 = 𝑟 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
31	23, 30	eqeq12d 2779	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
32	24, 31	anbi12d 641	. 2 ⊢ (𝑝 = 𝑟 → (((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
33		oveq1 7403	. . . 4 ⊢ (𝑝 = 𝐴 → (𝑝 ·no 𝑞) = (𝐴 ·no 𝑞))
34	33	eleq1d 2848	. . 3 ⊢ (𝑝 = 𝐴 → ((𝑝 ·no 𝑞) ∈ On ↔ (𝐴 ·no 𝑞) ∈ On))
35		oveq1 7403	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → (𝑝 ·no 𝑏) = (𝐴 ·no 𝑏))
36	35	oveq2d 7412	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)))
37	36	eleq1d 2848	. . . . . . . 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 3422	. . . . 5 ⊢ (𝑝 = 𝐴 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
41	40	inteqd 4911	. . . 4 ⊢ (𝑝 = 𝐴 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
42	33, 41	eqeq12d 2779	. . 3 ⊢ (𝑝 = 𝐴 → ((𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
43	34, 42	anbi12d 641	. 2 ⊢ (𝑝 = 𝐴 → (((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝐴 ·no 𝑞) ∈ On ∧ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
44		oveq2 7404	. . . 4 ⊢ (𝑞 = 𝐵 → (𝐴 ·no 𝑞) = (𝐴 ·no 𝐵))
45	44	eleq1d 2848	. . 3 ⊢ (𝑞 = 𝐵 → ((𝐴 ·no 𝑞) ∈ On ↔ (𝐴 ·no 𝐵) ∈ On))
46		oveq2 7404	. . . . . . . . . 10 ⊢ (𝑞 = 𝐵 → (𝑎 ·no 𝑞) = (𝑎 ·no 𝐵))
47	46	oveq1d 7411	. . . . . . . . 9 ⊢ (𝑞 = 𝐵 → ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) = ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)))
48	47	eleq1d 2848	. . . . . . . 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 3422	. . . . 5 ⊢ (𝑞 = 𝐵 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
52	51	inteqd 4911	. . . 4 ⊢ (𝑞 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
53	44, 52	eqeq12d 2779	. . 3 ⊢ (𝑞 = 𝐵 → ((𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
54	45, 53	anbi12d 641	. 2 ⊢ (𝑞 = 𝐵 → (((𝐴 ·no 𝑞) ∈ On ∧ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
55		simpl 486	. . . . 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 486	. . . . 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 486	. . . . 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 1165	. . 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 36543	. . . . . . . . 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 8638	. . . . . . . 8 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝 ·no 𝑞) = (⟨𝑝, 𝑞⟩(𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))))
64	63	adantr 484	. . . . . . 7 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) = (⟨𝑝, 𝑞⟩(𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))))
65		opex 5432	. . . . . . . 8 ⊢ ⟨𝑝, 𝑞⟩ ∈ V
66		nmulfn 36544	. . . . . . . . . 10 ⊢ ·no Fn (On × On)
67		fnfun 6621	. . . . . . . . . 10 ⊢ ( ·no Fn (On × On) → Fun ·no )
68	66, 67	ax-mp 5	. . . . . . . . 9 ⊢ Fun ·no
69		vex 3459	. . . . . . . . . . . 12 ⊢ 𝑝 ∈ V
70	69	sucex 7789	. . . . . . . . . . 11 ⊢ suc 𝑝 ∈ V
71		vex 3459	. . . . . . . . . . . 12 ⊢ 𝑞 ∈ V
72	71	sucex 7789	. . . . . . . . . . 11 ⊢ suc 𝑞 ∈ V
73	70, 72	xpex 7736	. . . . . . . . . 10 ⊢ (suc 𝑝 × suc 𝑞) ∈ V
74	73	difexi 5287	. . . . . . . . 9 ⊢ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}) ∈ V
75		resfunexg 7199	. . . . . . . . 9 ⊢ ((Fun ·no ∧ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}) ∈ V) → ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V)
76	68, 74, 75	mp2an 702	. . . . . . . 8 ⊢ ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V
77		elelsuc 6421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝑝 → 𝑎 ∈ suc 𝑝)
78	77	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑎 ∈ suc 𝑝)
79	78	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑎 ∈ suc 𝑝)
80	71	sucid 6430	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑞 ∈ suc 𝑞
81	80	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑞 ∈ suc 𝑞)
82	79, 81	opelxpd 5687	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑞⟩ ∈ (suc 𝑝 × suc 𝑞))
83		eloni 6356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ On → Ord 𝑝)
84		ordirr 6364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑝 → ¬ 𝑝 ∈ 𝑝)
85		elequ1 2150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑝 → (𝑎 ∈ 𝑝 ↔ 𝑝 ∈ 𝑝))
86	85	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑝 → (¬ 𝑎 ∈ 𝑝 ↔ ¬ 𝑝 ∈ 𝑝))
87	86	biimprcd 252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑝 ∈ 𝑝 → (𝑎 = 𝑝 → ¬ 𝑎 ∈ 𝑝))
88	87	con2d 134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑝 ∈ 𝑝 → (𝑎 ∈ 𝑝 → ¬ 𝑎 = 𝑝))
89	83, 84, 88	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑝 ∈ On → (𝑎 ∈ 𝑝 → ¬ 𝑎 = 𝑝))
90	89	imp 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ On ∧ 𝑎 ∈ 𝑝) → ¬ 𝑎 = 𝑝)
91	90	ad2ant2r 757	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ 𝑎 = 𝑝)
92	91	intnanrd 493	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑎 = 𝑝 ∧ 𝑞 = 𝑞))
93		opex 5432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑎, 𝑞⟩ ∈ V
94	93	elsn 4598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑎, 𝑞⟩ = ⟨𝑝, 𝑞⟩)
95		vex 3459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑎 ∈ V
96	95, 71	opth 5445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑞⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑎 = 𝑝 ∧ 𝑞 = 𝑞))
97	94, 96	bitr2i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩})
98	92, 97	sylnib 330	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩})
99	82, 98	eldifd 3916	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑞⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
100	99	fvresd 6887	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑞⟩) = ( ·no ‘⟨𝑎, 𝑞⟩))
101		df-ov 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑞⟩)
102		df-ov 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ·no 𝑞) = ( ·no ‘⟨𝑎, 𝑞⟩)
103	100, 101, 102	3eqtr4g 2823	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) = (𝑎 ·no 𝑞))
104	69	sucid 6430	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑝 ∈ suc 𝑝
105	104	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑝 ∈ suc 𝑝)
106		elelsuc 6421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ 𝑞 → 𝑏 ∈ suc 𝑞)
107	106	adantl 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑏 ∈ suc 𝑞)
108	107	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑏 ∈ suc 𝑞)
109	105, 108	opelxpd 5687	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑝, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
110		eloni 6356	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ On → Ord 𝑞)
111		ordirr 6364	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑞 → ¬ 𝑞 ∈ 𝑞)
112		elequ1 2150	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = 𝑞 → (𝑏 ∈ 𝑞 ↔ 𝑞 ∈ 𝑞))
113	112	notbid 320	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = 𝑞 → (¬ 𝑏 ∈ 𝑞 ↔ ¬ 𝑞 ∈ 𝑞))
114	113	biimprcd 252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑞 ∈ 𝑞 → (𝑏 = 𝑞 → ¬ 𝑏 ∈ 𝑞))
115	114	con2d 134	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (¬ 𝑞 ∈ 𝑞 → (𝑏 ∈ 𝑞 → ¬ 𝑏 = 𝑞))
116	110, 111, 115	3syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑞 ∈ On → (𝑏 ∈ 𝑞 → ¬ 𝑏 = 𝑞))
117	116	imp 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑞 ∈ On ∧ 𝑏 ∈ 𝑞) → ¬ 𝑏 = 𝑞)
118	117	ad2ant2l 756	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ 𝑏 = 𝑞)
119	118	intnand 492	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑝 = 𝑝 ∧ 𝑏 = 𝑞))
120		opex 5432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑝, 𝑏⟩ ∈ V
121	120	elsn 4598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑝, 𝑏⟩ = ⟨𝑝, 𝑞⟩)
122		vex 3459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑏 ∈ V
123	69, 122	opth 5445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑝, 𝑏⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑝 = 𝑝 ∧ 𝑏 = 𝑞))
124	121, 123	bitr2i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑝 ∧ 𝑏 = 𝑞) ↔ ⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
125	119, 124	sylnib 330	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
126	109, 125	eldifd 3916	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑝, 𝑏⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
127	126	fvresd 6887	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑝, 𝑏⟩) = ( ·no ‘⟨𝑝, 𝑏⟩))
128		df-ov 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑝, 𝑏⟩)
129		df-ov 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ·no 𝑏) = ( ·no ‘⟨𝑝, 𝑏⟩)
130	127, 128, 129	3eqtr4g 2823	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (𝑝 ·no 𝑏))
131	103, 130	oveq12d 7414	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
132		sssucid 6428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑝 ⊆ suc 𝑝
133		sssucid 6428	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑞 ⊆ suc 𝑞
134		xpss12 5663	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ⊆ suc 𝑝 ∧ 𝑞 ⊆ suc 𝑞) → (𝑝 × 𝑞) ⊆ (suc 𝑝 × suc 𝑞))
135	132, 133, 134	mp2an 702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 × 𝑞) ⊆ (suc 𝑝 × suc 𝑞)
136		opelxpi 5685	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → ⟨𝑎, 𝑏⟩ ∈ (𝑝 × 𝑞))
137	135, 136	sselid 3935	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → ⟨𝑎, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
138	137	adantl 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
139	118	intnand 492	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑎 = 𝑝 ∧ 𝑏 = 𝑞))
140		opex 5432	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
141	140	elsn 4598	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑝, 𝑞⟩)
142	95, 122	opth 5445	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑎 = 𝑝 ∧ 𝑏 = 𝑞))
143	141, 142	bitr2i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) ↔ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
144	139, 143	sylnib 330	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
145	138, 144	eldifd 3916	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑏⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
146	145	fvresd 6887	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑏⟩) = ( ·no ‘⟨𝑎, 𝑏⟩))
147		df-ov 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑏⟩)
148		df-ov 7399	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ·no 𝑏) = ( ·no ‘⟨𝑎, 𝑏⟩)
149	146, 147, 148	3eqtr4g 2823	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (𝑎 ·no 𝑏))
150	149	oveq2d 7412	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) = (𝑥 +no (𝑎 ·no 𝑏)))
151	131, 150	eleq12d 2857	. . . . . . . . . . . . 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 3422	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
154	153	inteqd 4911	. . . . . . . . . 10 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
155	154	adantr 484	. . . . . . . . 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 7403	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (𝑥 +no (𝑎 ·no 𝑏)) = (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
157	156	eleq2d 2849	. . . . . . . . . . . 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 7429	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ V
160	71, 159	iunex 7949	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ V
161	160	dfiun2 4990	. . . . . . . . . . . . 13 ⊢ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))}
162	159	dfiun2 4990	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))}
163		oveq1 7403	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = 𝑐 → (𝑟 ·no 𝑞) = (𝑐 ·no 𝑞))
164	163	eleq1d 2848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑟 = 𝑐 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑐 ·no 𝑞) ∈ On))
165		simplr2 1231	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
166	165	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
167		simplr 778	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → 𝑐 ∈ 𝑝)
168	164, 166, 167	rspcdva 3583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑐 ·no 𝑞) ∈ On)
169		oveq2 7404	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑑 → (𝑝 ·no 𝑠) = (𝑝 ·no 𝑑))
170	169	eleq1d 2848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑑 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑝 ·no 𝑑) ∈ On))
171		simplr3 1232	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
172	171	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
173		simpr 488	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → 𝑑 ∈ 𝑞)
174	170, 172, 173	rspcdva 3583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
175	168, 174	naddcld 8650	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
176		eleq1 2851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (𝑥 ∈ On ↔ ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On))
177	175, 176	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . 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 4021	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
180	71	abrexex 7943	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ V
181	180	ssonunii 7764	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On → ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
182	179, 181	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
183	162, 182	eqeltrid 2867	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
184		eleq1 2851	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (𝑥 ∈ On ↔ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On))
185	183, 184	syl5ibrcom 249	. . . . . . . . . . . . . . . 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 4021	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
188	69	abrexex 7943	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ V
189	188	ssonunii 7764	. . . . . . . . . . . . . 14 ⊢ ({𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On → ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
190	187, 189	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
191	161, 190	eqeltrid 2867	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
192		onsuc 7793	. . . . . . . . . . . 12 ⊢ (∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
193	191, 192	syl 17	. . . . . . . . . . 11 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
194		simplr2 1231	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
195	164	rspccva 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ 𝑐 ∈ 𝑝) → (𝑐 ·no 𝑞) ∈ On)
196	194, 195	sylan 589	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → (𝑐 ·no 𝑞) ∈ On)
197	196	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑐 ·no 𝑞) ∈ On)
198		simplr3 1232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
199	198	adantr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
200	170	rspccva 3581	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
201	199, 200	sylan 589	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
202	197, 201	naddcld 8650	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
203	202, 176	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . . 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 4021	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
206	205, 181	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
207	162, 206	eqeltrid 2867	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
208	207, 184	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . 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 4021	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
211	210, 189	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ On)
212	161, 211	eqeltrid 2867	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
213	212, 192	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
214		oveq1 7403	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ·no 𝑠) = (𝑎 ·no 𝑠))
215	214	eleq1d 2848	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → ((𝑟 ·no 𝑠) ∈ On ↔ (𝑎 ·no 𝑠) ∈ On))
216		oveq2 7404	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑏 → (𝑎 ·no 𝑠) = (𝑎 ·no 𝑏))
217	216	eleq1d 2848	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑏 → ((𝑎 ·no 𝑠) ∈ On ↔ (𝑎 ·no 𝑏) ∈ On))
218		simplr1 1230	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On)
219		simprl 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑎 ∈ 𝑝)
220		simprr 782	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑏 ∈ 𝑞)
221	215, 217, 218, 219, 220	rspc2dv 3597	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎 ·no 𝑏) ∈ On)
222		naddword1 8662	. . . . . . . . . . . . . 14 ⊢ ((suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On ∧ (𝑎 ·no 𝑏) ∈ On) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ⊆ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
223	213, 221, 222	syl2anc 593	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ⊆ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
224		oveq1 7403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → (𝑐 ·no 𝑞) = (𝑎 ·no 𝑞))
225	224	oveq1d 7411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
226	225	iuneq2d 4981	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
227	226	sseq2d 3969	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑))))
228		oveq2 7404	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑏 → (𝑝 ·no 𝑑) = (𝑝 ·no 𝑏))
229	228	oveq2d 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
230	229	sseq2d 3969	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏))))
231		ssidd 3960	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
232	230, 220, 231	rspcedvdw 3585	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∃𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
233		ssiun 5005	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
234	232, 233	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
235	227, 219, 234	rspcedvdw 3585	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∃𝑐 ∈ 𝑝 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
236		ssiun 5005	. . . . . . . . . . . . . . 15 ⊢ (∃𝑐 ∈ 𝑝 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
237	235, 236	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
238		simpr2 1210	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
239		simpl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑎 ∈ 𝑝)
240		oveq1 7403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝑟 ·no 𝑞) = (𝑎 ·no 𝑞))
241	240	eleq1d 2848	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑎 ·no 𝑞) ∈ On))
242	241	rspccva 3581	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ 𝑎 ∈ 𝑝) → (𝑎 ·no 𝑞) ∈ On)
243	238, 239, 242	syl2an 605	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎 ·no 𝑞) ∈ On)
244		simpr3 1211	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
245		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑏 ∈ 𝑞)
246		oveq2 7404	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑏 → (𝑝 ·no 𝑠) = (𝑝 ·no 𝑏))
247	246	eleq1d 2848	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑏 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑝 ·no 𝑏) ∈ On))
248	247	rspccva 3581	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On ∧ 𝑏 ∈ 𝑞) → (𝑝 ·no 𝑏) ∈ On)
249	244, 245, 248	syl2an 605	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑝 ·no 𝑏) ∈ On)
250	243, 249	naddcld 8650	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ On)
251		onsssuc 6438	. . . . . . . . . . . . . . 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 593	. . . . . . . . . . . . . 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 234	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
254	223, 253	sseldd 3938	. . . . . . . . . . . 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 3585	. . . . . . . . . 10 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∃𝑥 ∈ On ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)))
257		onintrab2 7780	. . . . . . . . . 10 ⊢ (∃𝑥 ∈ On ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ∈ On)
258	256, 257	sylib 220	. . . . . . . . 9 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ∈ On)
259	155, 258	eqeltrd 2863	. . . . . . . 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 7980	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → (1st ‘𝑣) = 𝑝)
261	69, 71	op2ndd 7981	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → (2nd ‘𝑣) = 𝑞)
262	261	csbeq1d 3857	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → ⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
263	260, 262	csbeq12dv 3862	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
264		oveq1 7403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑝 → (𝑐𝑤𝑏) = (𝑝𝑤𝑏))
265	264	oveq2d 7412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑝 → ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) = ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)))
266	265	eleq1d 2848	. . . . . . . . . . . . . . . . 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 3422	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑝 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
270	269	inteqd 4911	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑝 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
271	270	csbeq2dv 3860	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑝 → ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
272	69, 271	csbie 3888	. . . . . . . . . . 11 ⊢ ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
273		oveq2 7404	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑞 → (𝑎𝑤𝑑) = (𝑎𝑤𝑞))
274	273	oveq1d 7411	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑞 → ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) = ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)))
275	274	eleq1d 2848	. . . . . . . . . . . . . . . 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 3422	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑞 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
279	278	inteqd 4911	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑞 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
280	71, 279	csbie 3888	. . . . . . . . . . 11 ⊢ ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
281	272, 280	eqtri 2786	. . . . . . . . . 10 ⊢ ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
282		oveq 7402	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑎𝑤𝑞) = (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞))
283		oveq 7402	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑝𝑤𝑏) = (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))
284	282, 283	oveq12d 7414	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) = ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)))
285		oveq 7402	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑎𝑤𝑏) = (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))
286	285	oveq2d 7412	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑥 +no (𝑎𝑤𝑏)) = (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)))
287	284, 286	eleq12d 2857	. . . . . . . . . . . . 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 3422	. . . . . . . . . . 11 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
290	289	inteqd 4911	. . . . . . . . . 10 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
291	281, 290	eqtrid 2810	. . . . . . . . 9 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
292		eqid 2763	. . . . . . . . 9 ⊢ (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}) = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
293	263, 291, 292	ovmpog 7555	. . . . . . . 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 1487	. . . . . . 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 2802	. . . . . 6 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
296	295, 258	eqeltrd 2863	. . . . 5 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) ∈ On)
297	296, 295	jca 519	. . . 4 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
298	297	ex 416	. . 3 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On) → ((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
299	61, 298	syl5 34	. 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 8639	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143  {cab 2741  ∀wral 3077  ∃wrex 3087  {crab 3415  Vcvv 3455  ⦋csb 3853   ∖ cdif 3902   ⊆ wss 3905  {csn 4583  ⟨cop 4589  ∪ cuni 4866  ∩ cint 4906  ∪ ciun 4950   × cxp 5646   ↾ cres 5650  Ord word 6345  Oncon0 6346  suc csuc 6348  Fun wfun 6515   Fn wfn 6516  ‘cfv 6521  (class class class)co 7396   ∈ cmpo 7398  1^st c1st 7968  2^nd c2nd 7969   +no cnadd 8635   ·_no cnmul 36542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-tr 5209  df-id 5543  df-eprel 5548  df-po 5556  df-so 5557  df-fr 5601  df-se 5602  df-we 5603  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-pred 6288  df-ord 6349  df-on 6350  df-suc 6352  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-frecs 8262  df-nadd 8636  df-nmul 36543

This theorem is referenced by:  nmulcl  36546  nmulval  36547