Theorem txcls 23498

Description: Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.)

Assertion

Ref	Expression
txcls	⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))

Proof of Theorem txcls

Dummy variables 𝑠 𝑟 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		topontop 22807	. . . . . 6 ⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑅 ∈ Top)
2	1	ad2antrr 726	. . . . 5 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑅 ∈ Top)
3		simprl 770	. . . . . 6 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ 𝑋)
4		toponuni 22808	. . . . . . 7 ⊢ (𝑅 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝑅)
5	4	ad2antrr 726	. . . . . 6 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑋 = ∪ 𝑅)
6	3, 5	sseqtrd 3986	. . . . 5 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ ∪ 𝑅)
7		eqid 2730	. . . . . 6 ⊢ ∪ 𝑅 = ∪ 𝑅
8	7	clscld 22941	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅) → ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅))
9	2, 6, 8	syl2anc 584	. . . 4 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅))
10		topontop 22807	. . . . . 6 ⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑆 ∈ Top)
11	10	ad2antlr 727	. . . . 5 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑆 ∈ Top)
12		simprr 772	. . . . . 6 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ 𝑌)
13		toponuni 22808	. . . . . . 7 ⊢ (𝑆 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝑆)
14	13	ad2antlr 727	. . . . . 6 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝑌 = ∪ 𝑆)
15	12, 14	sseqtrd 3986	. . . . 5 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ ∪ 𝑆)
16		eqid 2730	. . . . . 6 ⊢ ∪ 𝑆 = ∪ 𝑆
17	16	clscld 22941	. . . . 5 ⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆) → ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆))
18	11, 15, 17	syl2anc 584	. . . 4 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆))
19		txcld 23497	. . . 4 ⊢ ((((cls‘𝑅)‘𝐴) ∈ (Clsd‘𝑅) ∧ ((cls‘𝑆)‘𝐵) ∈ (Clsd‘𝑆)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)))
20	9, 18, 19	syl2anc 584	. . 3 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)))
21	7	sscls 22950	. . . . 5 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅) → 𝐴 ⊆ ((cls‘𝑅)‘𝐴))
22	2, 6, 21	syl2anc 584	. . . 4 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐴 ⊆ ((cls‘𝑅)‘𝐴))
23	16	sscls 22950	. . . . 5 ⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆) → 𝐵 ⊆ ((cls‘𝑆)‘𝐵))
24	11, 15, 23	syl2anc 584	. . . 4 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → 𝐵 ⊆ ((cls‘𝑆)‘𝐵))
25		xpss12 5656	. . . 4 ⊢ ((𝐴 ⊆ ((cls‘𝑅)‘𝐴) ∧ 𝐵 ⊆ ((cls‘𝑆)‘𝐵)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
26	22, 24, 25	syl2anc 584	. . 3 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
27		eqid 2730	. . . 4 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
28	27	clsss2 22966	. . 3 ⊢ (((((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ∈ (Clsd‘(𝑅 ×t 𝑆)) ∧ (𝐴 × 𝐵) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
29	20, 26, 28	syl2anc 584	. 2 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ⊆ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
30		relxp 5659	. . . 4 ⊢ Rel (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵))
31	30	a1i 11	. . 3 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → Rel (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))
32		opelxp 5677	. . . 4 ⊢ (⟨𝑥, 𝑦⟩ ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ↔ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)))
33		eltx 23462	. . . . . . . . 9 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)))
34	33	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)))
35		eleq1 2817	. . . . . . . . . . . . 13 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝑧 ∈ (𝑟 × 𝑠) ↔ ⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠)))
36	35	anbi1d 631	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)))
37	36	2rexbidv 3203	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ↔ ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢)))
38	37	rspccva 3590	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑢) → ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))
39	2	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑅 ∈ Top)
40	6	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐴 ⊆ ∪ 𝑅)
41		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ ((cls‘𝑅)‘𝐴))
42		simprll 778	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑟 ∈ 𝑅)
43		simprrl 780	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠))
44		opelxp 5677	. . . . . . . . . . . . . . . . 17 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ↔ (𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠))
45	43, 44	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠))
46	45	simpld 494	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑥 ∈ 𝑟)
47	7	clsndisj 22969	. . . . . . . . . . . . . . 15 ⊢ (((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅 ∧ 𝑥 ∈ ((cls‘𝑅)‘𝐴)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑥 ∈ 𝑟)) → (𝑟 ∩ 𝐴) ≠ ∅)
48	39, 40, 41, 42, 46, 47	syl32anc 1380	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 ∩ 𝐴) ≠ ∅)
49		n0 4319	. . . . . . . . . . . . . 14 ⊢ ((𝑟 ∩ 𝐴) ≠ ∅ ↔ ∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴))
50	48, 49	sylib 218	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴))
51	11	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑆 ∈ Top)
52	15	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝐵 ⊆ ∪ 𝑆)
53		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ ((cls‘𝑆)‘𝐵))
54		simprlr 779	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑠 ∈ 𝑆)
55	45	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → 𝑦 ∈ 𝑠)
56	16	clsndisj 22969	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆 ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) ∧ (𝑠 ∈ 𝑆 ∧ 𝑦 ∈ 𝑠)) → (𝑠 ∩ 𝐵) ≠ ∅)
57	51, 52, 53, 54, 55, 56	syl32anc 1380	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑠 ∩ 𝐵) ≠ ∅)
58		n0 4319	. . . . . . . . . . . . . 14 ⊢ ((𝑠 ∩ 𝐵) ≠ ∅ ↔ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵))
59	57, 58	sylib 218	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵))
60		exdistrv 1955	. . . . . . . . . . . . . 14 ⊢ (∃𝑧∃𝑤(𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) ↔ (∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)))
61		opelxpi 5678	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → ⟨𝑧, 𝑤⟩ ∈ ((𝑟 ∩ 𝐴) × (𝑠 ∩ 𝐵)))
62		inxp 5798	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)) = ((𝑟 ∩ 𝐴) × (𝑠 ∩ 𝐵))
63	61, 62	eleqtrrdi 2840	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → ⟨𝑧, 𝑤⟩ ∈ ((𝑟 × 𝑠) ∩ (𝐴 × 𝐵)))
64	63	elin1d 4170	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → ⟨𝑧, 𝑤⟩ ∈ (𝑟 × 𝑠))
65		simprrr 781	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑟 × 𝑠) ⊆ 𝑢)
66	65	sselda 3949	. . . . . . . . . . . . . . . . . 18 ⊢ ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ ⟨𝑧, 𝑤⟩ ∈ (𝑟 × 𝑠)) → ⟨𝑧, 𝑤⟩ ∈ 𝑢)
67	64, 66	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → ⟨𝑧, 𝑤⟩ ∈ 𝑢)
68	63	elin2d 4171	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → ⟨𝑧, 𝑤⟩ ∈ (𝐴 × 𝐵))
69	68	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → ⟨𝑧, 𝑤⟩ ∈ (𝐴 × 𝐵))
70		inelcm 4431	. . . . . . . . . . . . . . . . 17 ⊢ ((⟨𝑧, 𝑤⟩ ∈ 𝑢 ∧ ⟨𝑧, 𝑤⟩ ∈ (𝐴 × 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)
71	67, 69, 70	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) ∧ (𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)
72	71	ex 412	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
73	72	exlimdvv 1934	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (∃𝑧∃𝑤(𝑧 ∈ (𝑟 ∩ 𝐴) ∧ 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
74	60, 73	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → ((∃𝑧 𝑧 ∈ (𝑟 ∩ 𝐴) ∧ ∃𝑤 𝑤 ∈ (𝑠 ∩ 𝐵)) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
75	50, 59, 74	mp2and 699	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ ((𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆) ∧ (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢))) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)
76	75	expr 456	. . . . . . . . . . 11 ⊢ (((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
77	76	rexlimdvva 3195	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (⟨𝑥, 𝑦⟩ ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
78	38, 77	syl5 34	. . . . . . . . 9 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ((∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝑢) → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
79	78	expd 415	. . . . . . . 8 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (∀𝑧 ∈ 𝑢 ∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (𝑧 ∈ (𝑟 × 𝑠) ∧ (𝑟 × 𝑠) ⊆ 𝑢) → (⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)))
80	34, 79	sylbid 240	. . . . . . 7 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑢 ∈ (𝑅 ×t 𝑆) → (⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)))
81	80	ralrimiv 3125	. . . . . 6 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ∀𝑢 ∈ (𝑅 ×t 𝑆)(⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅))
82		txtopon 23485	. . . . . . . . 9 ⊢ ((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)))
83	82	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)))
84		topontop 22807	. . . . . . . 8 ⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑅 ×t 𝑆) ∈ Top)
85	83, 84	syl 17	. . . . . . 7 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑅 ×t 𝑆) ∈ Top)
86		xpss12 5656	. . . . . . . . 9 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
87	86	ad2antlr 727	. . . . . . . 8 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
88		toponuni 22808	. . . . . . . . 9 ⊢ ((𝑅 ×t 𝑆) ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
89	83, 88	syl 17	. . . . . . . 8 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝑋 × 𝑌) = ∪ (𝑅 ×t 𝑆))
90	87, 89	sseqtrd 3986	. . . . . . 7 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (𝐴 × 𝐵) ⊆ ∪ (𝑅 ×t 𝑆))
91	7	clsss3 22953	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅) → ((cls‘𝑅)‘𝐴) ⊆ ∪ 𝑅)
92	2, 6, 91	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ ∪ 𝑅)
93	92, 5	sseqtrrd 3987	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑅)‘𝐴) ⊆ 𝑋)
94	93	sselda 3949	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ 𝑥 ∈ ((cls‘𝑅)‘𝐴)) → 𝑥 ∈ 𝑋)
95	94	adantrr 717	. . . . . . . . 9 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑥 ∈ 𝑋)
96	16	clsss3 22953	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆) → ((cls‘𝑆)‘𝐵) ⊆ ∪ 𝑆)
97	11, 15, 96	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ ∪ 𝑆)
98	97, 14	sseqtrrd 3987	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘𝑆)‘𝐵) ⊆ 𝑌)
99	98	sselda 3949	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → 𝑦 ∈ 𝑌)
100	99	adantrl 716	. . . . . . . . 9 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → 𝑦 ∈ 𝑌)
101	95, 100	opelxpd 5680	. . . . . . . 8 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ⟨𝑥, 𝑦⟩ ∈ (𝑋 × 𝑌))
102	101, 89	eleqtrd 2831	. . . . . . 7 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ⟨𝑥, 𝑦⟩ ∈ ∪ (𝑅 ×t 𝑆))
103	27	elcls 22967	. . . . . . 7 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝐴 × 𝐵) ⊆ ∪ (𝑅 ×t 𝑆) ∧ ⟨𝑥, 𝑦⟩ ∈ ∪ (𝑅 ×t 𝑆)) → (⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)))
104	85, 90, 102, 103	syl3anc 1373	. . . . . 6 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → (⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) ↔ ∀𝑢 ∈ (𝑅 ×t 𝑆)(⟨𝑥, 𝑦⟩ ∈ 𝑢 → (𝑢 ∩ (𝐴 × 𝐵)) ≠ ∅)))
105	81, 104	mpbird 257	. . . . 5 ⊢ ((((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) ∧ (𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵))) → ⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))
106	105	ex 412	. . . 4 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((𝑥 ∈ ((cls‘𝑅)‘𝐴) ∧ 𝑦 ∈ ((cls‘𝑆)‘𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))))
107	32, 106	biimtrid 242	. . 3 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (⟨𝑥, 𝑦⟩ ∈ (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) → ⟨𝑥, 𝑦⟩ ∈ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵))))
108	31, 107	relssdv 5754	. 2 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)) ⊆ ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)))
109	29, 108	eqssd 3967	1 ⊢ (((𝑅 ∈ (TopOn‘𝑋) ∧ 𝑆 ∈ (TopOn‘𝑌)) ∧ (𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌)) → ((cls‘(𝑅 ×t 𝑆))‘(𝐴 × 𝐵)) = (((cls‘𝑅)‘𝐴) × ((cls‘𝑆)‘𝐵)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054   ∩ cin 3916   ⊆ wss 3917  ∅c0 4299  ⟨cop 4598  ∪ cuni 4874   × cxp 5639  Rel wrel 5646  ‘cfv 6514  (class class class)co 7390  Topctop 22787  TopOnctopon 22804  Clsdccld 22910  clsccl 22912   ×_t ctx 23454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4914  df-iun 4960  df-iin 4961  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-1st 7971  df-2nd 7972  df-topgen 17413  df-top 22788  df-topon 22805  df-bases 22840  df-cld 22913  df-ntr 22914  df-cls 22915  df-tx 23456

This theorem is referenced by:  clssubg  24003