Metamath Proof Explorer

Theorem txcls

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

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

Proof

Step Hyp Ref Expression
1 topontop ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑅 ∈ Top )
2 1 ad2antrr ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝑅 ∈ Top )
3 simprl ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝐴 ⊆ 𝑋 )
4 toponuni ⊢ ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝑅 )
5 4 ad2antrr ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝑋 = ∪ 𝑅 )
6 3 5 sseqtrd ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝐴 ⊆ ∪ 𝑅 )
7 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
8 7 clscld ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅 ) → ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Clsd ‘ 𝑅 ) )
9 2 6 8 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Clsd ‘ 𝑅 ) )
10 topontop ⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑆 ∈ Top )
11 10 ad2antlr ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝑆 ∈ Top )
12 simprr ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝐵 ⊆ 𝑌 )
13 toponuni ⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝑆 )
14 13 ad2antlr ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝑌 = ∪ 𝑆 )
15 12 14 sseqtrd ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝐵 ⊆ ∪ 𝑆 )
16 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
17 16 clscld ⊢ ( ( 𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆 ) → ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ∈ ( Clsd ‘ 𝑆 ) )
18 11 15 17 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ∈ ( Clsd ‘ 𝑆 ) )
19 txcld ⊢ ( ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∈ ( Clsd ‘ 𝑅 ) ∧ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ∈ ( Clsd ‘ 𝑆 ) ) → ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) )
20 9 18 19 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) )
21 7 sscls ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅 ) → 𝐴 ⊆ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) )
22 2 6 21 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝐴 ⊆ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) )
23 16 sscls ⊢ ( ( 𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆 ) → 𝐵 ⊆ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) )
24 11 15 23 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → 𝐵 ⊆ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) )
25 xpss12 ⊢ ( ( 𝐴 ⊆ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝐵 ⊆ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) → ( 𝐴 × 𝐵 ) ⊆ ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) )
26 22 24 25 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( 𝐴 × 𝐵 ) ⊆ ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) )
27 eqid ⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 )
28 27 clsss2 ⊢ ( ( ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ∈ ( Clsd ‘ ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝐴 × 𝐵 ) ⊆ ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) ⊆ ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) )
29 20 26 28 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) ⊆ ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) )
30 relxp ⊢ Rel ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) )
31 30 a1i ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → Rel ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) )
32 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) )
33 eltx ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑢 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑢 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) )
34 33 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( 𝑢 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑧 ∈ 𝑢 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) )
35 eleq1 ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑧 ∈ ( 𝑟 × 𝑠 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ) )
36 35 anbi1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( 𝑧 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) )
37 36 2rexbidv ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) )
38 37 rspccva ⊢ ( ( ∀ 𝑧 ∈ 𝑢 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑢 ) → ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) )
39 2 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝑅 ∈ Top )
40 6 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝐴 ⊆ ∪ 𝑅 )
41 simplrl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) )
42 simprll ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝑟 ∈ 𝑅 )
43 simprrl ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) )
44 opelxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ↔ ( 𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠 ) )
45 43 44 sylib ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ( 𝑥 ∈ 𝑟 ∧ 𝑦 ∈ 𝑠 ) )
46 45 simpld ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝑥 ∈ 𝑟 )
47 7 clsndisj ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅 ∧ 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑥 ∈ 𝑟 ) ) → ( 𝑟 ∩ 𝐴 ) ≠ ∅ )
48 39 40 41 42 46 47 syl32anc ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ( 𝑟 ∩ 𝐴 ) ≠ ∅ )
49 n0 ⊢ ( ( 𝑟 ∩ 𝐴 ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) )
50 48 49 sylib ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ∃ 𝑧 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) )
51 11 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝑆 ∈ Top )
52 15 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝐵 ⊆ ∪ 𝑆 )
53 simplrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) )
54 simprlr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝑠 ∈ 𝑆 )
55 45 simprd ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → 𝑦 ∈ 𝑠 )
56 16 clsndisj ⊢ ( ( ( 𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆 ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ∧ ( 𝑠 ∈ 𝑆 ∧ 𝑦 ∈ 𝑠 ) ) → ( 𝑠 ∩ 𝐵 ) ≠ ∅ )
57 51 52 53 54 55 56 syl32anc ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ( 𝑠 ∩ 𝐵 ) ≠ ∅ )
58 n0 ⊢ ( ( 𝑠 ∩ 𝐵 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) )
59 57 58 sylib ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ∃ 𝑤 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) )
60 exdistrv ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) ↔ ( ∃ 𝑧 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ ∃ 𝑤 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) )
61 opelxpi ⊢ ( ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) )
62 inxp ⊢ ( ( 𝑟 × 𝑠 ) ∩ ( 𝐴 × 𝐵 ) ) = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) )
63 61 62 eleqtrrdi ⊢ ( ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( ( 𝑟 × 𝑠 ) ∩ ( 𝐴 × 𝐵 ) ) )
64 63 elin1d ⊢ ( ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑟 × 𝑠 ) )
65 simprrr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ( 𝑟 × 𝑠 ) ⊆ 𝑢 )
66 65 sselda ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝑟 × 𝑠 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑢 )
67 64 66 sylan2 ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑢 )
68 63 elin2d ⊢ ( ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐴 × 𝐵 ) )
69 68 adantl ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) ) → ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐴 × 𝐵 ) )
70 inelcm ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ ∈ 𝑢 ∧ ⟨ 𝑧 , 𝑤 ⟩ ∈ ( 𝐴 × 𝐵 ) ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ )
71 67 69 70 syl2anc ⊢ ( ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) ∧ ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ )
72 71 ex ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ( ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) )
73 72 exlimdvv ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ( ∃ 𝑧 ∃ 𝑤 ( 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) )
74 60 73 biimtrrid ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ( ( ∃ 𝑧 𝑧 ∈ ( 𝑟 ∩ 𝐴 ) ∧ ∃ 𝑤 𝑤 ∈ ( 𝑠 ∩ 𝐵 ) ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) )
75 50 59 74 mp2and ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ) ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ )
76 75 expr ⊢ ( ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) )
77 76 rexlimdvva ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) )
78 38 77 syl5 ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( ( ∀ 𝑧 ∈ 𝑢 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑢 ) → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) )
79 78 expd ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( ∀ 𝑧 ∈ 𝑢 ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( 𝑧 ∈ ( 𝑟 × 𝑠 ) ∧ ( 𝑟 × 𝑠 ) ⊆ 𝑢 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑢 → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) ) )
80 34 79 sylbid ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( 𝑢 ∈ ( 𝑅 ×t 𝑆 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑢 → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) ) )
81 80 ralrimiv ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ∀ 𝑢 ∈ ( 𝑅 ×t 𝑆 ) ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑢 → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) )
82 txtopon ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
83 82 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
84 topontop ⊢ ( ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
85 83 84 syl ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
86 xpss12 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝑋 × 𝑌 ) )
87 86 ad2antlr ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝑋 × 𝑌 ) )
88 toponuni ⊢ ( ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
89 83 88 syl ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
90 87 89 sseqtrd ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( 𝐴 × 𝐵 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) )
91 7 clsss3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝐴 ⊆ ∪ 𝑅 ) → ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ⊆ ∪ 𝑅 )
92 2 6 91 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ⊆ ∪ 𝑅 )
93 92 5 sseqtrrd ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ⊆ 𝑋 )
94 93 sselda ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ) → 𝑥 ∈ 𝑋 )
95 94 adantrr ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → 𝑥 ∈ 𝑋 )
96 16 clsss3 ⊢ ( ( 𝑆 ∈ Top ∧ 𝐵 ⊆ ∪ 𝑆 ) → ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ⊆ ∪ 𝑆 )
97 11 15 96 syl2anc ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ⊆ ∪ 𝑆 )
98 97 14 sseqtrrd ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ⊆ 𝑌 )
99 98 sselda ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) → 𝑦 ∈ 𝑌 )
100 99 adantrl ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → 𝑦 ∈ 𝑌 )
101 95 100 opelxpd ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝑋 × 𝑌 ) )
102 101 89 eleqtrd ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ ( 𝑅 ×t 𝑆 ) )
103 27 elcls ⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( 𝐴 × 𝐵 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ ( 𝑅 ×t 𝑆 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑢 ∈ ( 𝑅 ×t 𝑆 ) ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑢 → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) ) )
104 85 90 102 103 syl3anc ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) ↔ ∀ 𝑢 ∈ ( 𝑅 ×t 𝑆 ) ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑢 → ( 𝑢 ∩ ( 𝐴 × 𝐵 ) ) ≠ ∅ ) ) )
105 81 104 mpbird ⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) ∧ ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) )
106 105 ex ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( 𝑥 ∈ ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) ∧ 𝑦 ∈ ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) ) )
107 32 106 biimtrid ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) ) )
108 31 107 relssdv ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) ⊆ ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) )
109 29 108 eqssd ⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌 ) ) → ( ( cls ‘ ( 𝑅 ×t 𝑆 ) ) ‘ ( 𝐴 × 𝐵 ) ) = ( ( ( cls ‘ 𝑅 ) ‘ 𝐴 ) × ( ( cls ‘ 𝑆 ) ‘ 𝐵 ) ) )