Theorem tx1stc 23598

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 23391	. . 3 ⊢ (𝑅 ∈ 1stω → 𝑅 ∈ Top)
2		1stctop 23391	. . 3 ⊢ (𝑆 ∈ 1stω → 𝑆 ∈ Top)
3		txtop 23517	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 597	. 2 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ Top)
5		eqid 2737	. . . . . . . 8 ⊢ ∪ 𝑅 = ∪ 𝑅
6	5	1stcclb 23392	. . . . . . 7 ⊢ ((𝑅 ∈ 1stω ∧ 𝑢 ∈ ∪ 𝑅) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))))
7	6	ad2ant2r 748	. . . . . 6 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))))
8		eqid 2737	. . . . . . . 8 ⊢ ∪ 𝑆 = ∪ 𝑆
9	8	1stcclb 23392	. . . . . . 7 ⊢ ((𝑆 ∈ 1stω ∧ 𝑣 ∈ ∪ 𝑆) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
10	9	ad2ant2l 747	. . . . . 6 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
11		reeanv 3209	. . . . . . 7 ⊢ (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ (∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))))
12		an4 657	. . . . . . . . 9 ⊢ (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ↔ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))))
13		txopn 23550	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑚 ∈ 𝑅 ∧ 𝑛 ∈ 𝑆)) → (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
14	13	ralrimivva 3180	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
15	1, 2, 14	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
16	15	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
17		elpwi 4562	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ∈ 𝒫 𝑅 → 𝑎 ⊆ 𝑅)
18		ssralv 4003	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 ⊆ 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
19	17, 18	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ 𝒫 𝑅 → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
20		elpwi 4562	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝒫 𝑆 → 𝑏 ⊆ 𝑆)
21		ssralv 4003	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ⊆ 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
22	20, 21	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
23	22	ralimdv 3151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 ∈ 𝒫 𝑆 → (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
24	19, 23	sylan9 507	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆) → (∀𝑚 ∈ 𝑅 ∀𝑛 ∈ 𝑆 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆)))
25	16, 24	mpan9 506	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆))
26		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))
27	26	fmpo 8014	. . . . . . . . . . . . . . 15 ⊢ (∀𝑚 ∈ 𝑎 ∀𝑛 ∈ 𝑏 (𝑚 × 𝑛) ∈ (𝑅 ×t 𝑆) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
28	25, 27	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)⟶(𝑅 ×t 𝑆))
29	28	frnd 6671	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
30		ovex 7393	. . . . . . . . . . . . . 14 ⊢ (𝑅 ×t 𝑆) ∈ V
31	30	elpw2 5280	. . . . . . . . . . . . 13 ⊢ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ⊆ (𝑅 ×t 𝑆))
32	29, 31	sylibr 234	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
33	32	adantr 480	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆))
34		omelon 9559	. . . . . . . . . . . . . . 15 ⊢ ω ∈ On
35		xpct 9930	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ≼ ω)
36		ondomen 9951	. . . . . . . . . . . . . . 15 ⊢ ((ω ∈ On ∧ (𝑎 × 𝑏) ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
37	34, 35, 36	sylancr 588	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → (𝑎 × 𝑏) ∈ dom card)
38		vex 3445	. . . . . . . . . . . . . . . . 17 ⊢ 𝑚 ∈ V
39		vex 3445	. . . . . . . . . . . . . . . . 17 ⊢ 𝑛 ∈ V
40	38, 39	xpex 7700	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 × 𝑛) ∈ V
41	26, 40	fnmpoi 8016	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏)
42		dffn4 6753	. . . . . . . . . . . . . . 15 ⊢ ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) Fn (𝑎 × 𝑏) ↔ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)))
43	41, 42	mpbi 230	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))
44		fodomnum 9971	. . . . . . . . . . . . . 14 ⊢ ((𝑎 × 𝑏) ∈ dom card → ((𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)):(𝑎 × 𝑏)–onto→ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏)))
45	37, 43, 44	mpisyl 21	. . . . . . . . . . . . 13 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏))
46		domtr 8948	. . . . . . . . . . . . 13 ⊢ ((ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
47	45, 35, 46	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
48	47	ad2antrl 729	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω)
49	1, 2	anim12i 614	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
50	49	ad3antrrr 731	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑅 ∈ Top ∧ 𝑆 ∈ Top))
51		eltx 23516	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
52	50, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
53		eleq1 2825	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → (𝑤 ∈ (𝑟 × 𝑠) ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠)))
54	53	anbi1d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → ((𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
55	54	2rexbidv 3202	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = ⟨𝑢, 𝑣⟩ → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
56	55	rspccv 3574	. . . . . . . . . . . . . 14 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
57		r19.27v 3166	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))
58		r19.29 3100	. . . . . . . . . . . . . . . . . . 19 ⊢ ((∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
59		r19.29 3100	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
60		opelxp 5661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ↔ (𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠))
61		pm3.35 803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))
62		pm3.35 803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))
63	61, 62	anim12i 614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑢 ∈ 𝑟 ∧ (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑣 ∈ 𝑠 ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
64	63	an4s 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑢 ∈ 𝑟 ∧ 𝑣 ∈ 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
65	60, 64	sylanb 582	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
66	65	anim1i 616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
67	66	anasss 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
68	67	an12s 650	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
69	68	expl 457	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
70	69	reximdv 3152	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → (∃𝑠 ∈ 𝑆 ((𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
71	59, 70	syl5 34	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) → ((∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)))
72	71	impl 455	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
73	72	reximi 3075	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑟 ∈ 𝑅 (((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
74	58, 73	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑟 ∈ 𝑅 ((𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
75	57, 74	sylan 581	. . . . . . . . . . . . . . . . 17 ⊢ (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧))
76		reeanv 3209	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ↔ (∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
77		simpr1l 1232	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑝 ∈ 𝑎)
78		simpr1r 1233	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → 𝑞 ∈ 𝑏)
79		eqidd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) = (𝑝 × 𝑞))
80		xpeq1 5639	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑚 = 𝑝 → (𝑚 × 𝑛) = (𝑝 × 𝑛))
81	80	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑚 = 𝑝 → ((𝑝 × 𝑞) = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑛)))
82		xpeq2 5646	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑞 → (𝑝 × 𝑛) = (𝑝 × 𝑞))
83	82	eqeq2d 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑞 → ((𝑝 × 𝑞) = (𝑝 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑝 × 𝑞)))
84	81, 83	rspc2ev 3590	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏 ∧ (𝑝 × 𝑞) = (𝑝 × 𝑞)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
85	77, 78, 79, 84	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
86		vex 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑝 ∈ V
87		vex 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ 𝑞 ∈ V
88	86, 87	xpex 7700	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑝 × 𝑞) ∈ V
89		eqeq1 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑥 = (𝑝 × 𝑞) → (𝑥 = (𝑚 × 𝑛) ↔ (𝑝 × 𝑞) = (𝑚 × 𝑛)))
90	89	2rexbidv 3202	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑥 = (𝑝 × 𝑞) → (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛) ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛)))
91	88, 90	elab 3635	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)} ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 (𝑝 × 𝑞) = (𝑚 × 𝑛))
92	85, 91	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)})
93	26	rnmpo 7493	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) = {𝑥 ∣ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑏 𝑥 = (𝑚 × 𝑛)}
94	92, 93	eleqtrrdi 2848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)))
95		simpr2 1197	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))
96		opelxpi 5662	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 ∈ 𝑝 ∧ 𝑣 ∈ 𝑞) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
97	96	ad2ant2r 748	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
98	95, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞))
99		xpss12 5640	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑝 ⊆ 𝑟 ∧ 𝑞 ⊆ 𝑠) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
100	99	ad2ant2l 747	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
101	95, 100	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ (𝑟 × 𝑠))
102		simpr3 1198	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑟 × 𝑠) ⊆ 𝑧)
103	101, 102	sstrd 3945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → (𝑝 × 𝑞) ⊆ 𝑧)
104		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝑝 × 𝑞) → (⟨𝑢, 𝑣⟩ ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞)))
105		sseq1 3960	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑤 = (𝑝 × 𝑞) → (𝑤 ⊆ 𝑧 ↔ (𝑝 × 𝑞) ⊆ 𝑧))
106	104, 105	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 = (𝑝 × 𝑞) → ((⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)))
107	106	rspcev 3577	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑝 × 𝑞) ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∧ (⟨𝑢, 𝑣⟩ ∈ (𝑝 × 𝑞) ∧ (𝑝 × 𝑞) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))
108	94, 98, 103, 107	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) ∧ ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) ∧ ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))
109	108	3exp2 1356	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((𝑝 ∈ 𝑎 ∧ 𝑞 ∈ 𝑏) → (((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
110	109	rexlimdvv 3193	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (∃𝑝 ∈ 𝑎 ∃𝑞 ∈ 𝑏 ((𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
111	76, 110	biimtrrid 243	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) → ((𝑟 × 𝑠) ⊆ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
112	111	impd 410	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
113	112	rexlimdvva 3194	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 ((∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟) ∧ ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
114	75, 113	syl5 34	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → (((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) ∧ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧)) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
115	114	expd 415	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ (𝑎 ≼ ω ∧ 𝑏 ≼ ω)) → ((∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
116	115	impr 454	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑢, 𝑣⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
117	56, 116	syl9r 78	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (∀𝑤 ∈ 𝑧 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑤 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑧) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
118	52, 117	sylbid 240	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → (𝑧 ∈ (𝑅 ×t 𝑆) → (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
119	118	ralrimiv 3128	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
120		breq1 5102	. . . . . . . . . . . . 13 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (𝑦 ≼ ω ↔ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω))
121		rexeq 3293	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
122	121	imbi2d 340	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
123	122	ralbidv 3160	. . . . . . . . . . . . 13 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → (∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
124	120, 123	anbi12d 633	. . . . . . . . . . . 12 ⊢ (𝑦 = ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
125	124	rspcev 3577	. . . . . . . . . . 11 ⊢ ((ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ∈ 𝒫 (𝑅 ×t 𝑆) ∧ (ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛)) ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ ran (𝑚 ∈ 𝑎, 𝑛 ∈ 𝑏 ↦ (𝑚 × 𝑛))(⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
126	33, 48, 119, 125	syl12anc 837	. . . . . . . . . 10 ⊢ (((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) ∧ ((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠))))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
127	126	ex 412	. . . . . . . . 9 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ 𝑏 ≼ ω) ∧ (∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟)) ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
128	12, 127	biimtrid 242	. . . . . . . 8 ⊢ ((((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) ∧ (𝑎 ∈ 𝒫 𝑅 ∧ 𝑏 ∈ 𝒫 𝑆)) → (((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
129	128	rexlimdvva 3194	. . . . . . 7 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → (∃𝑎 ∈ 𝒫 𝑅∃𝑏 ∈ 𝒫 𝑆((𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ (𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
130	11, 129	biimtrrid 243	. . . . . 6 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ((∃𝑎 ∈ 𝒫 𝑅(𝑎 ≼ ω ∧ ∀𝑟 ∈ 𝑅 (𝑢 ∈ 𝑟 → ∃𝑝 ∈ 𝑎 (𝑢 ∈ 𝑝 ∧ 𝑝 ⊆ 𝑟))) ∧ ∃𝑏 ∈ 𝒫 𝑆(𝑏 ≼ ω ∧ ∀𝑠 ∈ 𝑆 (𝑣 ∈ 𝑠 → ∃𝑞 ∈ 𝑏 (𝑣 ∈ 𝑞 ∧ 𝑞 ⊆ 𝑠)))) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
131	7, 10, 130	mp2and 700	. . . . 5 ⊢ (((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) ∧ (𝑢 ∈ ∪ 𝑅 ∧ 𝑣 ∈ ∪ 𝑆)) → ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
132	131	ralrimivva 3180	. . . 4 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
133		eleq1 2825	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥 ∈ 𝑧 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑧))
134		eleq1 2825	. . . . . . . . . . 11 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (𝑥 ∈ 𝑤 ↔ ⟨𝑢, 𝑣⟩ ∈ 𝑤))
135	134	anbi1d 632	. . . . . . . . . 10 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
136	135	rexbidv 3161	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧) ↔ ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))
137	133, 136	imbi12d 344	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ (⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
138	137	ralbidv 3160	. . . . . . 7 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)) ↔ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
139	138	anbi2d 631	. . . . . 6 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → ((𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ (𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
140	139	rexbidv 3161	. . . . 5 ⊢ (𝑥 = ⟨𝑢, 𝑣⟩ → (∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
141	140	ralxp 5791	. . . 4 ⊢ (∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))) ↔ ∀𝑢 ∈ ∪ 𝑅∀𝑣 ∈ ∪ 𝑆∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(⟨𝑢, 𝑣⟩ ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (⟨𝑢, 𝑣⟩ ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
142	132, 141	sylibr 234	. . 3 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑥 ∈ (∪ 𝑅 × ∪ 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
143	5, 8	txuni 23540	. . . 4 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
144	1, 2, 143	syl2an 597	. . 3 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
145	142, 144	raleqtrdv 3299	. 2 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧))))
146		eqid 2737	. . 3 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
147	146	is1stc2 23390	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ 1stω ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 ∈ ∪ (𝑅 ×t 𝑆)∃𝑦 ∈ 𝒫 (𝑅 ×t 𝑆)(𝑦 ≼ ω ∧ ∀𝑧 ∈ (𝑅 ×t 𝑆)(𝑥 ∈ 𝑧 → ∃𝑤 ∈ 𝑦 (𝑥 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑧)))))
148	4, 145, 147	sylanbrc 584	1 ⊢ ((𝑅 ∈ 1stω ∧ 𝑆 ∈ 1stω) → (𝑅 ×t 𝑆) ∈ 1stω)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  {cab 2715  ∀wral 3052  ∃wrex 3061   ⊆ wss 3902  𝒫 cpw 4555  ⟨cop 4587  ∪ cuni 4864   class class class wbr 5099   × cxp 5623  dom cdm 5625  ran crn 5626  Oncon0 6318   Fn wfn 6488  ⟶wf 6489  –onto→wfo 6491  (class class class)co 7360   ∈ cmpo 7362  ωcom 7810   ≼ cdom 8885  cardccrd 9851  Topctop 22841  1^stωc1stc 23385   ×_t ctx 23508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682  ax-inf2 9554

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3351  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4904  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-se 5579  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-isom 6502  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-1st 7935  df-2nd 7936  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-er 8637  df-map 8769  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-oi 9419  df-card 9855  df-acn 9858  df-topgen 17367  df-top 22842  df-topon 22859  df-bases 22894  df-1stc 23387  df-tx 23510

This theorem is referenced by: (None)