Theorem tx1stc 21862

Description: The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.)

Assertion

Ref	Expression
tx1stc	⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ×t 𝑆) ∈ 1st𝜔)

Proof of Theorem tx1stc

Dummy variables 𝑎 𝑏 𝑚 𝑛 𝑝 𝑞 𝑟 𝑠 𝑢 𝑣 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1stctop 21655	. . 3 ⊢ (𝑅 ∈ 1st𝜔 → 𝑅 ∈ Top)
2		1stctop 21655	. . 3 ⊢ (𝑆 ∈ 1st𝜔 → 𝑆 ∈ Top)
3		txtop 21781	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 589	. 2 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ×t 𝑆) ∈ Top)
5		eqid 2778	. . . . . . . 8 ⊢ ∪ 𝑅 = ∪ 𝑅
6	5	1stcclb 21656	. . . . . . 7 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑢 ∈ ∪ 𝑅) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))))
7	6	ad2ant2r 737	. . . . . 6 ⊢ (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))))
8		eqid 2778	. . . . . . . 8 ⊢ ∪ 𝑆 = ∪ 𝑆
9	8	1stcclb 21656	. . . . . . 7 ⊢ ((𝑆 ∈ 1st𝜔 ∧ 𝑣 ∈ ∪ 𝑆) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
10	9	ad2ant2l 736	. . . . . 6 ⊢ (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
11		reeanv 3293	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))))
12		an4 646	. . . . . . . . 9 ⊢ (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))))
13		txopn 21814	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚 ∈ 𝑅 ∧ 𝑛 ∈ 𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
14	13	ralrimivva 3153	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
15	1, 2, 14	syl2an 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
16	15	adantr 474	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
17		elpwi 4389	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ 𝒫 𝑅 → 𝑎 ⊆ 𝑅)
18		ssralv 3885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ⊆ 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
19	17, 18	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ 𝒫 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
20		elpwi 4389	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝒫 𝑆 → 𝑏 ⊆ 𝑆)
21		ssralv 3885	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ⊆ 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
23	22	ralimdv 3145	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
24	19, 23	sylan9 503	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆) → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
25	16, 24	mpan9 502	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
26		eqid 2778	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))
27	26	fmpt2 7517	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
28	25, 27	sylib 210	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
29	28	frnd 6298	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
30		ovex 6954	. . . . . . . . . . . . . 14 ⊢ (𝑅 ×t 𝑆) ∈ V
31	30	elpw2 5062	. . . . . . . . . . . . 13 ⊢ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
32	29, 31	sylibr 226	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
33	32	adantr 474	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
34		omelon 8840	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
35		vex 3401	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑏 ∈ V
36	35	xpdom1 8347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ≼ ω → (𝑎 × 𝑏) ≼ (ω × 𝑏))
37		omex 8837	. . . . . . . . . . . . . . . . . 18 ⊢ ω ∈ V
38	37	xpdom2 8343	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ≼ ω → (ω × 𝑏) ≼ (ω × ω))
39		domtr 8294	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑎 × 𝑏) ≼ (ω × 𝑏) ∧ (ω × 𝑏) ≼ (ω × ω)) → (𝑎 × 𝑏) ≼ (ω × ω))
40	36, 38, 39	syl2an 589	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ (ω × ω))
41		xpomen 9171	. . . . . . . . . . . . . . . 16 ⊢ (ω × ω) ≈ ω
42		domentr 8300	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 × 𝑏) ≼ (ω × ω) ∧ (ω × ω) ≈ ω) → (𝑎 × 𝑏) ≼ ω)
43	40, 41, 42	sylancl 580	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω)
44		ondomen 9193	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ On ∧ (𝑎 × 𝑏) ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
45	34, 43, 44	sylancr 581	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
46		vex 3401	. . . . . . . . . . . . . . . . 17 ⊢ 𝑚 ∈ V
47		vex 3401	. . . . . . . . . . . . . . . . 17 ⊢ 𝑛 ∈ V
48	46, 47	xpex 7240	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 × 𝑛) ∈ V
49	26, 48	fnmpt2i 7519	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏)
50		dffn4 6372	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)))
51	49, 50	mpbi 222	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))
52		fodomnum 9213	. . . . . . . . . . . . . 14 ⊢ ((𝑎 × 𝑏) ∈ dom card → ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)))
53	45, 51, 52	mpisyl 21	. . . . . . . . . . . . 13 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))
54		domtr 8294	. . . . . . . . . . . . 13 ⊢ ((ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
55	53, 43, 54	syl2anc 579	. . . . . . . . . . . 12 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
56	55	ad2antrl 718	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
57	1, 2	anim12i 606	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
58	57	ad3antrrr 720	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
59		eltx 21780	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
60	58, 59	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
61		eleq1 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠)))
62	61	anbi1d 623	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
63	62	2rexbidv 3242	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
64	63	rspccv 3508	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
65		r19.27v 3256	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
66		r19.29 3258	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
67		r19.29 3258	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
68		opelxp 5391	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ↔ (𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠))
69		pm3.35 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))
70		pm3.35 793	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))
71	69, 70	anim12i 606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
72	71	an4s 650	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
73	68, 72	sylanb 576	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
74	73	anim1i 608	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
75	74	anasss 460	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
76	75	an12s 639	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
77	76	expl 451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
78	77	reximdv 3197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
79	67, 78	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
80	79	impl 449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
81	80	reximi 3192	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
82	66, 81	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
83	65, 82	sylan 575	. . . . . . . . . . . . . . . . 17 ⊢ (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
84		reeanv 3293	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ↔ (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
85		simpr1l 1262	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝 ∈ 𝑎)
86		simpr1r 1264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞 ∈ 𝑏)
87		eqidd 2779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞))
88		xpeq1 5369	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛))
89	88	eqeq2d 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛)))
90		xpeq2 5376	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞))
91	90	eqeq2d 2788	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞)))
92	89, 91	rspc2ev 3526	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
93	85, 86, 87, 92	syl3anc 1439	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
94		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑝 ∈ V
95		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑞 ∈ V
96	94, 95	xpex 7240	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 × 𝑞) ∈ V
97		eqeq1 2782	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛)))
98	97	2rexbidv 3242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑝 × 𝑞) → (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)))
99	96, 98	elab 3558	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
100	93, 99	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)})
101	26	rnmpt2 7047	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)}
102	100, 101	syl6eleqr 2870	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)))
103		simpr2 1207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
104		opelxpi 5392	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ 𝑝 ∧ 𝑣 ∈ 𝑞) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
105	104	ad2ant2r 737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
106	103, 105	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
107		xpss12 5370	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ⊆ 𝑟 ∧ 𝑞 ⊆ 𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
108	107	ad2ant2l 736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
109	103, 108	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
110		simpr3 1209	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧)
111	109, 110	sstrd 3831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧)
112		eleq2 2848	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝑝 × 𝑞) → (⟨𝑢, 𝑣⟩ ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞)))
113		sseq1 3845	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝑝 × 𝑞) → (𝑤 ⊆ 𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧))
114	112, 113	anbi12d 624	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑝 × 𝑞) → ((⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)))
115	114	rspcev 3511	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))
116	102, 106, 111, 115	syl12anc 827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))
117	116	3exp2 1416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) → (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
118	117	rexlimdvv 3220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
119	84, 118	syl5bir 235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
120	119	impd 400	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
121	120	rexlimdvva 3221	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
122	83, 121	syl5 34	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
123	122	expd 406	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
124	123	impr 448	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
125	64, 124	syl9r 78	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
126	60, 125	sylbid 232	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
127	126	ralrimiv 3147	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
128		breq1 4889	. . . . . . . . . . . . 13 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω))
129		rexeq 3331	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
130	129	imbi2d 332	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
131	130	ralbidv 3168	. . . . . . . . . . . . 13 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
132	128, 131	anbi12d 624	. . . . . . . . . . . 12 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
133	132	rspcev 3511	. . . . . . . . . . 11 ⊢ ((ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
134	33, 56, 127, 133	syl12anc 827	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
135	134	ex 403	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
136	12, 135	syl5bi 234	. . . . . . . 8 ⊢ ((((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
137	136	rexlimdvva 3221	. . . . . . 7 ⊢ (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
138	11, 137	syl5bir 235	. . . . . 6 ⊢ (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
139	7, 10, 138	mp2and 689	. . . . 5 ⊢ (((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
140	139	ralrimivva 3153	. . . 4 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
141		eleq1 2847	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥 ∈ 𝑧 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑧))
142		eleq1 2847	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥 ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑤))
143	142	anbi1d 623	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
144	143	rexbidv 3237	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
145	141, 144	imbi12d 336	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
146	145	ralbidv 3168	. . . . . . 7 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
147	146	anbi2d 622	. . . . . 6 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
148	147	rexbidv 3237	. . . . 5 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
149	148	ralxp 5509	. . . 4 ⊢ (∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
150	140, 149	sylibr 226	. . 3 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
151	5, 8	txuni 21804	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
152	1, 2, 151	syl2an 589	. . . 4 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
153	152	raleqdv 3340	. . 3 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
154	150, 153	mpbid 224	. 2 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
155		eqid 2778	. . 3 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
156	155	is1stc2 21654	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ 1st𝜔 ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
157	4, 154, 156	sylanbrc 578	1 ⊢ ((𝑅 ∈ 1st𝜔 ∧ 𝑆 ∈ 1st𝜔) → (𝑅 ×t 𝑆) ∈ 1st𝜔)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107  {cab 2763  ∀wral 3090  ∃wrex 3091   ⊆ wss 3792  𝒫 cpw 4379  ⟨cop 4404  ∪ cuni 4671   class class class wbr 4886   × cxp 5353  dom cdm 5355  ran crn 5356  Oncon0 5976   Fn wfn 6130  ⟶wf 6131  –onto→wfo 6133  (class class class)co 6922   ↦ cmpt2 6924  ωcom 7343   ≈ cen 8238   ≼ cdom 8239  cardccrd 9094  Topctop 21105  1^st𝜔c1stc 21649   ×_t ctx 21772

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-oadd 7847  df-er 8026  df-map 8142  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-oi 8704  df-card 9098  df-acn 9101  df-topgen 16490  df-top 21106  df-topon 21123  df-bases 21158  df-1stc 21651  df-tx 21774

This theorem is referenced by: (None)