Theorem nmulprop 36478

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 7388	. . . 4 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑞) = (𝑟 ·no 𝑞))
2	1	eleq1d 2837	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑞) ∈ On ↔ (𝑟 ·no 𝑞) ∈ On))
3		oveq1 7388	. . . . . . . . . 10 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑏) = (𝑟 ·no 𝑏))
4	3	oveq2d 7397	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)))
5	4	eleq1d 2837	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
6	5	ralbidv 3175	. . . . . . 7 ⊢ (𝑝 = 𝑟 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
7	6	raleqbi1dv 3320	. . . . . 6 ⊢ (𝑝 = 𝑟 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
8	7	rabbidv 3411	. . . . 5 ⊢ (𝑝 = 𝑟 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
9	8	inteqd 4900	. . . 4 ⊢ (𝑝 = 𝑟 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
10	1, 9	eqeq12d 2768	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
11	2, 10	anbi12d 640	. 2 ⊢ (𝑝 = 𝑟 → (((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
12		oveq2 7389	. . . 4 ⊢ (𝑞 = 𝑠 → (𝑟 ·no 𝑞) = (𝑟 ·no 𝑠))
13	12	eleq1d 2837	. . 3 ⊢ (𝑞 = 𝑠 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑟 ·no 𝑠) ∈ On))
14		oveq2 7389	. . . . . . . . . 10 ⊢ (𝑞 = 𝑠 → (𝑎 ·no 𝑞) = (𝑎 ·no 𝑠))
15	14	oveq1d 7396	. . . . . . . . 9 ⊢ (𝑞 = 𝑠 → ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) = ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)))
16	15	eleq1d 2837	. . . . . . . 8 ⊢ (𝑞 = 𝑠 → (((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
17	16	raleqbi1dv 3320	. . . . . . 7 ⊢ (𝑞 = 𝑠 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
18	17	ralbidv 3175	. . . . . 6 ⊢ (𝑞 = 𝑠 → (∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
19	18	rabbidv 3411	. . . . 5 ⊢ (𝑞 = 𝑠 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
20	19	inteqd 4900	. . . 4 ⊢ (𝑞 = 𝑠 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
21	12, 20	eqeq12d 2768	. . 3 ⊢ (𝑞 = 𝑠 → ((𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
22	13, 21	anbi12d 640	. 2 ⊢ (𝑞 = 𝑠 → (((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
23		oveq1 7388	. . . 4 ⊢ (𝑝 = 𝑟 → (𝑝 ·no 𝑠) = (𝑟 ·no 𝑠))
24	23	eleq1d 2837	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑟 ·no 𝑠) ∈ On))
25	3	oveq2d 7397	. . . . . . . . 9 ⊢ (𝑝 = 𝑟 → ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)))
26	25	eleq1d 2837	. . . . . . . 8 ⊢ (𝑝 = 𝑟 → (((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
27	26	ralbidv 3175	. . . . . . 7 ⊢ (𝑝 = 𝑟 → (∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
28	27	raleqbi1dv 3320	. . . . . 6 ⊢ (𝑝 = 𝑟 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
29	28	rabbidv 3411	. . . . 5 ⊢ (𝑝 = 𝑟 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
30	29	inteqd 4900	. . . 4 ⊢ (𝑝 = 𝑟 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
31	23, 30	eqeq12d 2768	. . 3 ⊢ (𝑝 = 𝑟 → ((𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
32	24, 31	anbi12d 640	. 2 ⊢ (𝑝 = 𝑟 → (((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
33		oveq1 7388	. . . 4 ⊢ (𝑝 = 𝐴 → (𝑝 ·no 𝑞) = (𝐴 ·no 𝑞))
34	33	eleq1d 2837	. . 3 ⊢ (𝑝 = 𝐴 → ((𝑝 ·no 𝑞) ∈ On ↔ (𝐴 ·no 𝑞) ∈ On))
35		oveq1 7388	. . . . . . . . . 10 ⊢ (𝑝 = 𝐴 → (𝑝 ·no 𝑏) = (𝐴 ·no 𝑏))
36	35	oveq2d 7397	. . . . . . . . 9 ⊢ (𝑝 = 𝐴 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) = ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)))
37	36	eleq1d 2837	. . . . . . . 8 ⊢ (𝑝 = 𝐴 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
38	37	ralbidv 3175	. . . . . . 7 ⊢ (𝑝 = 𝐴 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
39	38	raleqbi1dv 3320	. . . . . 6 ⊢ (𝑝 = 𝐴 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
40	39	rabbidv 3411	. . . . 5 ⊢ (𝑝 = 𝐴 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
41	40	inteqd 4900	. . . 4 ⊢ (𝑝 = 𝐴 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
42	33, 41	eqeq12d 2768	. . 3 ⊢ (𝑝 = 𝐴 → ((𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
43	34, 42	anbi12d 640	. 2 ⊢ (𝑝 = 𝐴 → (((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝐴 ·no 𝑞) ∈ On ∧ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
44		oveq2 7389	. . . 4 ⊢ (𝑞 = 𝐵 → (𝐴 ·no 𝑞) = (𝐴 ·no 𝐵))
45	44	eleq1d 2837	. . 3 ⊢ (𝑞 = 𝐵 → ((𝐴 ·no 𝑞) ∈ On ↔ (𝐴 ·no 𝐵) ∈ On))
46		oveq2 7389	. . . . . . . . . 10 ⊢ (𝑞 = 𝐵 → (𝑎 ·no 𝑞) = (𝑎 ·no 𝐵))
47	46	oveq1d 7396	. . . . . . . . 9 ⊢ (𝑞 = 𝐵 → ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) = ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)))
48	47	eleq1d 2837	. . . . . . . 8 ⊢ (𝑞 = 𝐵 → (((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
49	48	raleqbi1dv 3320	. . . . . . 7 ⊢ (𝑞 = 𝐵 → (∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
50	49	ralbidv 3175	. . . . . 6 ⊢ (𝑞 = 𝐵 → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
51	50	rabbidv 3411	. . . . 5 ⊢ (𝑞 = 𝐵 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
52	51	inteqd 4900	. . . 4 ⊢ (𝑞 = 𝐵 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
53	44, 52	eqeq12d 2768	. . 3 ⊢ (𝑞 = 𝐵 → ((𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))} ↔ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
54	45, 53	anbi12d 640	. 2 ⊢ (𝑞 = 𝐵 → (((𝐴 ·no 𝑞) ∈ On ∧ (𝐴 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) ↔ ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})))
55		simpl 485	. . . . 5 ⊢ (((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → (𝑟 ·no 𝑠) ∈ On)
56	55	2ralimi 3122	. . . 4 ⊢ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 ((𝑟 ·no 𝑠) ∈ On ∧ (𝑟 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → ∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On)
57		simpl 485	. . . . 5 ⊢ (((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → (𝑟 ·no 𝑞) ∈ On)
58	57	ralimi 3089	. . . 4 ⊢ (∀𝑟 ∈ 𝑝 ((𝑟 ·no 𝑞) ∈ On ∧ (𝑟 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑟 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑟 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
59		simpl 485	. . . . 5 ⊢ (((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → (𝑝 ·no 𝑠) ∈ On)
60	59	ralimi 3089	. . . 4 ⊢ (∀𝑠 ∈ 𝑞 ((𝑝 ·no 𝑠) ∈ On ∧ (𝑝 ·no 𝑠) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑠 ((𝑎 ·no 𝑠) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
61	56, 58, 60	3anim123i 1160	. . 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 36476	. . . . . . . . 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 8622	. . . . . . . 8 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝 ·no 𝑞) = (⟨𝑝, 𝑞⟩(𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))))
64	63	adantr 483	. . . . . . 7 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) = (⟨𝑝, 𝑞⟩(𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))))
65		opex 5421	. . . . . . . 8 ⊢ ⟨𝑝, 𝑞⟩ ∈ V
66		nmulfn 36477	. . . . . . . . . 10 ⊢ ·no Fn (On × On)
67		fnfun 6606	. . . . . . . . . 10 ⊢ ( ·no Fn (On × On) → Fun ·no )
68	66, 67	ax-mp 5	. . . . . . . . 9 ⊢ Fun ·no
69		vex 3448	. . . . . . . . . . . 12 ⊢ 𝑝 ∈ V
70	69	sucex 7774	. . . . . . . . . . 11 ⊢ suc 𝑝 ∈ V
71		vex 3448	. . . . . . . . . . . 12 ⊢ 𝑞 ∈ V
72	71	sucex 7774	. . . . . . . . . . 11 ⊢ suc 𝑞 ∈ V
73	70, 72	xpex 7721	. . . . . . . . . 10 ⊢ (suc 𝑝 × suc 𝑞) ∈ V
74	73	difexi 5276	. . . . . . . . 9 ⊢ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}) ∈ V
75		resfunexg 7184	. . . . . . . . 9 ⊢ ((Fun ·no ∧ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}) ∈ V) → ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V)
76	68, 74, 75	mp2an 700	. . . . . . . 8 ⊢ ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) ∈ V
77		elelsuc 6406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝑝 → 𝑎 ∈ suc 𝑝)
78	77	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑎 ∈ suc 𝑝)
79	78	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑎 ∈ suc 𝑝)
80	71	sucid 6415	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑞 ∈ suc 𝑞
81	80	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑞 ∈ suc 𝑞)
82	79, 81	opelxpd 5675	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑞⟩ ∈ (suc 𝑝 × suc 𝑞))
83		eloni 6341	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 ∈ On → Ord 𝑝)
84		ordirr 6349	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑝 → ¬ 𝑝 ∈ 𝑝)
85		elequ1 2139	. . . . . . . . . . . . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ∈ On ∧ 𝑎 ∈ 𝑝) → ¬ 𝑎 = 𝑝)
91	90	ad2ant2r 755	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ 𝑎 = 𝑝)
92	91	intnanrd 492	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑎 = 𝑝 ∧ 𝑞 = 𝑞))
93		opex 5421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑎, 𝑞⟩ ∈ V
94	93	elsn 4587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑎, 𝑞⟩ = ⟨𝑝, 𝑞⟩)
95		vex 3448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑎 ∈ V
96	95, 71	opth 5434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑞⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑎 = 𝑝 ∧ 𝑞 = 𝑞))
97	94, 96	bitr2i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩})
98	92, 97	sylnib 330	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑎, 𝑞⟩ ∈ {⟨𝑝, 𝑞⟩})
99	82, 98	eldifd 3906	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑞⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
100	99	fvresd 6872	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑞⟩) = ( ·no ‘⟨𝑎, 𝑞⟩))
101		df-ov 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑞⟩)
102		df-ov 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ·no 𝑞) = ( ·no ‘⟨𝑎, 𝑞⟩)
103	100, 101, 102	3eqtr4g 2812	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) = (𝑎 ·no 𝑞))
104	69	sucid 6415	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑝 ∈ suc 𝑝
105	104	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑝 ∈ suc 𝑝)
106		elelsuc 6406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ 𝑞 → 𝑏 ∈ suc 𝑞)
107	106	adantl 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑏 ∈ suc 𝑞)
108	107	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑏 ∈ suc 𝑞)
109	105, 108	opelxpd 5675	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑝, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
110		eloni 6341	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 ∈ On → Ord 𝑞)
111		ordirr 6349	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Ord 𝑞 → ¬ 𝑞 ∈ 𝑞)
112		elequ1 2139	. . . . . . . . . . . . . . . . . . . . . . . . . 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 409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑞 ∈ On ∧ 𝑏 ∈ 𝑞) → ¬ 𝑏 = 𝑞)
118	117	ad2ant2l 754	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ 𝑏 = 𝑞)
119	118	intnand 491	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑝 = 𝑝 ∧ 𝑏 = 𝑞))
120		opex 5421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑝, 𝑏⟩ ∈ V
121	120	elsn 4587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑝, 𝑏⟩ = ⟨𝑝, 𝑞⟩)
122		vex 3448	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑏 ∈ V
123	69, 122	opth 5434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑝, 𝑏⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑝 = 𝑝 ∧ 𝑏 = 𝑞))
124	121, 123	bitr2i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑝 ∧ 𝑏 = 𝑞) ↔ ⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
125	119, 124	sylnib 330	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑝, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
126	109, 125	eldifd 3906	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑝, 𝑏⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
127	126	fvresd 6872	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑝, 𝑏⟩) = ( ·no ‘⟨𝑝, 𝑏⟩))
128		df-ov 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑝, 𝑏⟩)
129		df-ov 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 ·no 𝑏) = ( ·no ‘⟨𝑝, 𝑏⟩)
130	127, 128, 129	3eqtr4g 2812	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (𝑝 ·no 𝑏))
131	103, 130	oveq12d 7399	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
132		sssucid 6413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑝 ⊆ suc 𝑝
133		sssucid 6413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑞 ⊆ suc 𝑞
134		xpss12 5651	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 ⊆ suc 𝑝 ∧ 𝑞 ⊆ suc 𝑞) → (𝑝 × 𝑞) ⊆ (suc 𝑝 × suc 𝑞))
135	132, 133, 134	mp2an 700	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 × 𝑞) ⊆ (suc 𝑝 × suc 𝑞)
136		opelxpi 5673	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → ⟨𝑎, 𝑏⟩ ∈ (𝑝 × 𝑞))
137	135, 136	sselid 3925	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → ⟨𝑎, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
138	137	adantl 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑏⟩ ∈ (suc 𝑝 × suc 𝑞))
139	118	intnand 491	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ (𝑎 = 𝑝 ∧ 𝑏 = 𝑞))
140		opex 5421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
141	140	elsn 4587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩} ↔ ⟨𝑎, 𝑏⟩ = ⟨𝑝, 𝑞⟩)
142	95, 122	opth 5434	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑝, 𝑞⟩ ↔ (𝑎 = 𝑝 ∧ 𝑏 = 𝑞))
143	141, 142	bitr2i 278	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 = 𝑝 ∧ 𝑏 = 𝑞) ↔ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
144	139, 143	sylnib 330	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ¬ ⟨𝑎, 𝑏⟩ ∈ {⟨𝑝, 𝑞⟩})
145	138, 144	eldifd 3906	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ⟨𝑎, 𝑏⟩ ∈ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))
146	145	fvresd 6872	. . . . . . . . . . . . . . . 16 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑏⟩) = ( ·no ‘⟨𝑎, 𝑏⟩))
147		df-ov 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))‘⟨𝑎, 𝑏⟩)
148		df-ov 7384	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 ·no 𝑏) = ( ·no ‘⟨𝑎, 𝑏⟩)
149	146, 147, 148	3eqtr4g 2812	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏) = (𝑎 ·no 𝑏))
150	149	oveq2d 7397	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) = (𝑥 +no (𝑎 ·no 𝑏)))
151	131, 150	eleq12d 2846	. . . . . . . . . . . . 13 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
152	151	2ralbidva 3214	. . . . . . . . . . . 12 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))))
153	152	rabbidv 3411	. . . . . . . . . . 11 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
154	153	inteqd 4900	. . . . . . . . . 10 ⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
155	154	adantr 483	. . . . . . . . 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 7388	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (𝑥 +no (𝑎 ·no 𝑏)) = (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
157	156	eleq2d 2838	. . . . . . . . . . . 12 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏))))
158	157	2ralbidv 3216	. . . . . . . . . . 11 ⊢ (𝑥 = suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏))))
159		ovex 7414	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ V
160	71, 159	iunex 7934	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ V
161	160	dfiun2 4979	. . . . . . . . . . . . 13 ⊢ ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))}
162	159	dfiun2 4979	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))}
163		oveq1 7388	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑟 = 𝑐 → (𝑟 ·no 𝑞) = (𝑐 ·no 𝑞))
164	163	eleq1d 2837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑟 = 𝑐 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑐 ·no 𝑞) ∈ On))
165		simplr2 1226	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
166	165	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
167		simplr 776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → 𝑐 ∈ 𝑝)
168	164, 166, 167	rspcdva 3573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑐 ·no 𝑞) ∈ On)
169		oveq2 7389	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑠 = 𝑑 → (𝑝 ·no 𝑠) = (𝑝 ·no 𝑑))
170	169	eleq1d 2837	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑠 = 𝑑 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑝 ·no 𝑑) ∈ On))
171		simplr3 1227	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
172	171	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
173		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → 𝑑 ∈ 𝑞)
174	170, 172, 173	rspcdva 3573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
175	168, 174	naddcld 8634	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
176		eleq1 2840	. . . . . . . . . . . . . . . . . . . . . 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 3153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → (∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
179	178	abssdv 4011	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
180	71	abrexex 7928	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑥 ∣ ∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ V
181	180	ssonunii 7749	. . . . . . . . . . . . . . . . . . 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 2856	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ 𝑐 ∈ 𝑝) → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
184		eleq1 2840	. . . . . . . . . . . . . . . . 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 3153	. . . . . . . . . . . . . . 15 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
187	186	abssdv 4011	. . . . . . . . . . . . . 14 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ⊆ On)
188	69	abrexex 7928	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∣ ∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑))} ∈ V
189	188	ssonunii 7749	. . . . . . . . . . . . . 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 2856	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On)
192		onsuc 7778	. . . . . . . . . . . 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 1226	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
195	164	rspccva 3571	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ 𝑐 ∈ 𝑝) → (𝑐 ·no 𝑞) ∈ On)
196	194, 195	sylan 588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → (𝑐 ·no 𝑞) ∈ On)
197	196	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑐 ·no 𝑞) ∈ On)
198		simplr3 1227	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
199	198	adantr 483	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
200	170	rspccva 3571	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
201	199, 200	sylan 588	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) ∧ 𝑑 ∈ 𝑞) → (𝑝 ·no 𝑑) ∈ On)
202	197, 201	naddcld 8634	. . . . . . . . . . . . . . . . . . . . . . . . 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 3153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) ∧ 𝑐 ∈ 𝑝) → (∃𝑑 ∈ 𝑞 𝑥 = ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
205	204	abssdv 4011	. . . . . . . . . . . . . . . . . . . . . 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 2856	. . . . . . . . . . . . . . . . . . . 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 3153	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (∃𝑐 ∈ 𝑝 𝑥 = ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) → 𝑥 ∈ On))
210	209	abssdv 4011	. . . . . . . . . . . . . . . . 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 2856	. . . . . . . . . . . . . . 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 7388	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 = 𝑎 → (𝑟 ·no 𝑠) = (𝑎 ·no 𝑠))
215	214	eleq1d 2837	. . . . . . . . . . . . . . 15 ⊢ (𝑟 = 𝑎 → ((𝑟 ·no 𝑠) ∈ On ↔ (𝑎 ·no 𝑠) ∈ On))
216		oveq2 7389	. . . . . . . . . . . . . . . 16 ⊢ (𝑠 = 𝑏 → (𝑎 ·no 𝑠) = (𝑎 ·no 𝑏))
217	216	eleq1d 2837	. . . . . . . . . . . . . . 15 ⊢ (𝑠 = 𝑏 → ((𝑎 ·no 𝑠) ∈ On ↔ (𝑎 ·no 𝑏) ∈ On))
218		simplr1 1225	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On)
219		simprl 778	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑎 ∈ 𝑝)
220		simprr 780	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → 𝑏 ∈ 𝑞)
221	215, 217, 218, 219, 220	rspc2dv 3587	. . . . . . . . . . . . . 14 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎 ·no 𝑏) ∈ On)
222		naddword1 8646	. . . . . . . . . . . . . 14 ⊢ ((suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ∈ On ∧ (𝑎 ·no 𝑏) ∈ On) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ⊆ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
223	213, 221, 222	syl2anc 592	. . . . . . . . . . . . 13 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ⊆ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
224		oveq1 7388	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑎 → (𝑐 ·no 𝑞) = (𝑎 ·no 𝑞))
225	224	oveq1d 7396	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
226	225	iuneq2d 4970	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
227	226	sseq2d 3959	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑))))
228		oveq2 7389	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑏 → (𝑝 ·no 𝑑) = (𝑝 ·no 𝑏))
229	228	oveq2d 7397	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 = 𝑏 → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) = ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
230	229	sseq2d 3959	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑏 → (((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)) ↔ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏))))
231		ssidd 3950	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)))
232	230, 220, 231	rspcedvdw 3575	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∃𝑑 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑑)))
233		ssiun 4994	. . . . . . . . . . . . . . . . 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 3575	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ∃𝑐 ∈ 𝑝 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ⊆ ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)))
236		ssiun 4994	. . . . . . . . . . . . . . 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 1205	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On)
239		simpl 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑎 ∈ 𝑝)
240		oveq1 7388	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑟 = 𝑎 → (𝑟 ·no 𝑞) = (𝑎 ·no 𝑞))
241	240	eleq1d 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑎 → ((𝑟 ·no 𝑞) ∈ On ↔ (𝑎 ·no 𝑞) ∈ On))
242	241	rspccva 3571	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ 𝑎 ∈ 𝑝) → (𝑎 ·no 𝑞) ∈ On)
243	238, 239, 242	syl2an 604	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑎 ·no 𝑞) ∈ On)
244		simpr3 1206	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)
245		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞) → 𝑏 ∈ 𝑞)
246		oveq2 7389	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑠 = 𝑏 → (𝑝 ·no 𝑠) = (𝑝 ·no 𝑏))
247	246	eleq1d 2837	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑏 → ((𝑝 ·no 𝑠) ∈ On ↔ (𝑝 ·no 𝑏) ∈ On))
248	247	rspccva 3571	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On ∧ 𝑏 ∈ 𝑞) → (𝑝 ·no 𝑏) ∈ On)
249	244, 245, 248	syl2an 604	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → (𝑝 ·no 𝑏) ∈ On)
250	243, 249	naddcld 8634	. . . . . . . . . . . . . . 15 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ On)
251		onsssuc 6423	. . . . . . . . . . . . . . 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 592	. . . . . . . . . . . . . 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 3928	. . . . . . . . . . . 12 ⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) ∧ (𝑎 ∈ 𝑝 ∧ 𝑏 ∈ 𝑞)) → ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
255	254	ralrimivva 3195	. . . . . . . . . . 11 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (suc ∪ 𝑐 ∈ 𝑝 ∪ 𝑑 ∈ 𝑞 ((𝑐 ·no 𝑞) +no (𝑝 ·no 𝑑)) +no (𝑎 ·no 𝑏)))
256	158, 193, 255	rspcedvdw 3575	. . . . . . . . . 10 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ∃𝑥 ∈ On ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏)))
257		onintrab2 7765	. . . . . . . . . 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 2852	. . . . . . . 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 7965	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → (1st ‘𝑣) = 𝑝)
261	69, 71	op2ndd 7966	. . . . . . . . . . 11 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → (2nd ‘𝑣) = 𝑞)
262	261	csbeq1d 3847	. . . . . . . . . 10 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → ⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
263	260, 262	csbeq12dv 3852	. . . . . . . . 9 ⊢ (𝑣 = ⟨𝑝, 𝑞⟩ → ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
264		oveq1 7388	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑝 → (𝑐𝑤𝑏) = (𝑝𝑤𝑏))
265	264	oveq2d 7397	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑝 → ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) = ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)))
266	265	eleq1d 2837	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑝 → (((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
267	266	ralbidv 3175	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑝 → (∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
268	267	raleqbi1dv 3320	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑝 → (∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
269	268	rabbidv 3411	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑝 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
270	269	inteqd 4900	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑝 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
271	270	csbeq2dv 3850	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝑝 → ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
272	69, 271	csbie 3878	. . . . . . . . . . 11 ⊢ ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
273		oveq2 7389	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 = 𝑞 → (𝑎𝑤𝑑) = (𝑎𝑤𝑞))
274	273	oveq1d 7396	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝑞 → ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) = ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)))
275	274	eleq1d 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 = 𝑞 → (((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
276	275	raleqbi1dv 3320	. . . . . . . . . . . . . . 15 ⊢ (𝑑 = 𝑞 → (∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
277	276	ralbidv 3175	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑞 → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))))
278	277	rabbidv 3411	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑞 → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
279	278	inteqd 4900	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑞 → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
280	71, 279	csbie 3878	. . . . . . . . . . 11 ⊢ ⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
281	272, 280	eqtri 2775	. . . . . . . . . 10 ⊢ ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}
282		oveq 7387	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑎𝑤𝑞) = (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞))
283		oveq 7387	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑝𝑤𝑏) = (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))
284	282, 283	oveq12d 7399	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) = ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)))
285		oveq 7387	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑎𝑤𝑏) = (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))
286	285	oveq2d 7397	. . . . . . . . . . . . . 14 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (𝑥 +no (𝑎𝑤𝑏)) = (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)))
287	284, 286	eleq12d 2846	. . . . . . . . . . . . 13 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))))
288	287	2ralbidv 3216	. . . . . . . . . . . 12 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → (∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏)) ↔ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))))
289	288	rabbidv 3411	. . . . . . . . . . 11 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
290	289	inteqd 4900	. . . . . . . . . 10 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎𝑤𝑞) +no (𝑝𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
291	281, 290	eqtrid 2799	. . . . . . . . 9 ⊢ (𝑤 = ( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩})) → ⦋𝑝 / 𝑐⦌⦋𝑞 / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))} = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑞) +no (𝑝( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏)) ∈ (𝑥 +no (𝑎( ·no ↾ ((suc 𝑝 × suc 𝑞) ∖ {⟨𝑝, 𝑞⟩}))𝑏))})
292		eqid 2752	. . . . . . . . 9 ⊢ (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))}) = (𝑣 ∈ V, 𝑤 ∈ V ↦ ⦋(1st ‘𝑣) / 𝑐⦌⦋(2nd ‘𝑣) / 𝑑⦌∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑐 ∀𝑏 ∈ 𝑑 ((𝑎𝑤𝑑) +no (𝑐𝑤𝑏)) ∈ (𝑥 +no (𝑎𝑤𝑏))})
293	263, 291, 292	ovmpog 7540	. . . . . . . 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 1476	. . . . . . 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 2791	. . . . . 6 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))})
296	295, 258	eqeltrd 2852	. . . . 5 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → (𝑝 ·no 𝑞) ∈ On)
297	296, 295	jca 518	. . . 4 ⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (∀𝑟 ∈ 𝑝 ∀𝑠 ∈ 𝑞 (𝑟 ·no 𝑠) ∈ On ∧ ∀𝑟 ∈ 𝑝 (𝑟 ·no 𝑞) ∈ On ∧ ∀𝑠 ∈ 𝑞 (𝑝 ·no 𝑠) ∈ On)) → ((𝑝 ·no 𝑞) ∈ On ∧ (𝑝 ·no 𝑞) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝑝 ∀𝑏 ∈ 𝑞 ((𝑎 ·no 𝑞) +no (𝑝 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))
298	297	ex 415	. . 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 8623	1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·no 𝐵) ∈ On ∧ (𝐴 ·no 𝐵) = ∩ {𝑥 ∈ On ∣ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 ((𝑎 ·no 𝐵) +no (𝐴 ·no 𝑏)) ∈ (𝑥 +no (𝑎 ·no 𝑏))}))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1095   = wceq 1550   ∈ wcel 2132  {cab 2730  ∀wral 3066  ∃wrex 3076  {crab 3404  Vcvv 3444  ⦋csb 3843   ∖ cdif 3892   ⊆ wss 3895  {csn 4572  ⟨cop 4578  ∪ cuni 4855  ∩ cint 4895  ∪ ciun 4939   × cxp 5634   ↾ cres 5638  Ord word 6330  Oncon0 6331  suc csuc 6333  Fun wfun 6500   Fn wfn 6501  ‘cfv 6506  (class class class)co 7381   ∈ cmpo 7383  1^st c1st 7953  2^nd c2nd 7954   +no cnadd 8619   ·_no cnmul 36475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-rep 5217  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-reu 3358  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-pss 3915  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-int 4896  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-tr 5198  df-id 5531  df-eprel 5536  df-po 5544  df-so 5545  df-fr 5589  df-se 5590  df-we 5591  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-pred 6273  df-ord 6334  df-on 6335  df-suc 6337  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-ov 7384  df-oprab 7385  df-mpo 7386  df-1st 7955  df-2nd 7956  df-frecs 8246  df-nadd 8620  df-nmul 36476

This theorem is referenced by:  nmulcl  36479  nmulval  36480