This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clsconn

Description: The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion clsconn ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ Conn )

Proof

Step Hyp Ref Expression
1 simpll3 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ) → ( 𝐽 ↾t 𝐴 ) ∈ Conn )
2 simpll1 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
3 simpll2 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝐴 ⊆ 𝑋 )
4 simplrl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝑥 ∈ 𝐽 )
5 simplrr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝑦 ∈ 𝐽 )
6 simprl1 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ )
7 n0 ⊢ ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
8 6 7 sylib ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ∃ 𝑧 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
9 2 adantr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
11 9 10 syl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐽 ∈ Top )
12 3 adantr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐴 ⊆ 𝑋 )
13 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
14 9 13 syl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑋 = ∪ 𝐽 )
15 12 14 sseqtrd ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐴 ⊆ ∪ 𝐽 )
16 simpr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
17 16 elin2d ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
18 4 adantr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑥 ∈ 𝐽 )
19 16 elin1d ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑧 ∈ 𝑥 )
20 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
21 20 clsndisj ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑧 ∈ 𝑥 ) ) → ( 𝑥 ∩ 𝐴 ) ≠ ∅ )
22 11 15 17 18 19 21 syl32anc ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ( 𝑥 ∩ 𝐴 ) ≠ ∅ )
23 8 22 exlimddv ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( 𝑥 ∩ 𝐴 ) ≠ ∅ )
24 simprl2 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ )
25 n0 ⊢ ( ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
26 24 25 sylib ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ∃ 𝑧 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
27 2 adantr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
28 27 10 syl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐽 ∈ Top )
29 3 adantr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐴 ⊆ 𝑋 )
30 27 13 syl ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑋 = ∪ 𝐽 )
31 29 30 sseqtrd ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝐴 ⊆ ∪ 𝐽 )
32 simpr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
33 32 elin2d ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
34 5 adantr ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑦 ∈ 𝐽 )
35 32 elin1d ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → 𝑧 ∈ 𝑦 )
36 20 clsndisj ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑧 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∧ ( 𝑦 ∈ 𝐽 ∧ 𝑧 ∈ 𝑦 ) ) → ( 𝑦 ∩ 𝐴 ) ≠ ∅ )
37 28 31 33 34 35 36 syl32anc ⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) ∧ 𝑧 ∈ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ( 𝑦 ∩ 𝐴 ) ≠ ∅ )
38 26 37 exlimddv ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( 𝑦 ∩ 𝐴 ) ≠ ∅ )
39 simprl3 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) )
40 2 10 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝐽 ∈ Top )
41 2 13 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝑋 = ∪ 𝐽 )
42 3 41 sseqtrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝐴 ⊆ ∪ 𝐽 )
43 20 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ) → 𝐴 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
44 40 42 43 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝐴 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) )
45 44 sscond ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ⊆ ( 𝑋 ∖ 𝐴 ) )
46 39 45 sstrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ 𝐴 ) )
47 ssv ⊢ 𝑋 ⊆ V
48 ssdif ⊢ ( 𝑋 ⊆ V → ( 𝑋 ∖ 𝐴 ) ⊆ ( V ∖ 𝐴 ) )
49 47 48 ax-mp ⊢ ( 𝑋 ∖ 𝐴 ) ⊆ ( V ∖ 𝐴 )
50 46 49 sstrdi ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( 𝑥 ∩ 𝑦 ) ⊆ ( V ∖ 𝐴 ) )
51 disj2 ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( V ∖ 𝐴 ) )
52 50 51 sylibr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝐴 ) = ∅ )
53 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) )
54 44 53 sstrd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → 𝐴 ⊆ ( 𝑥 ∪ 𝑦 ) )
55 2 3 4 5 23 38 52 54 nconnsubb ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn )
56 55 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) → ¬ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) )
57 1 56 mt2d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) ) → ¬ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) )
58 57 ex ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ¬ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) )
59 58 ralrimivva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ¬ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) )
60 simp1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
61 13 sseq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ∪ 𝐽 ) )
62 61 biimpa ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 ⊆ ∪ 𝐽 )
63 20 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ∪ 𝐽 )
64 10 62 63 syl2an2r ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ∪ 𝐽 )
65 13 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → 𝑋 = ∪ 𝐽 )
66 64 65 sseqtrrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 )
67 66 3adant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) → ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 )
68 connsub ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ 𝑋 ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ¬ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) )
69 60 67 68 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑦 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑋 ∖ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ) → ¬ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ⊆ ( 𝑥 ∪ 𝑦 ) ) ) )
70 59 69 mpbird ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝐴 ) ∈ Conn ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) ∈ Conn )