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 )