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

Metamath Proof Explorer

Theorem dfconn2

Description: An alternate definition of connectedness. (Contributed by Jeff Hankins, 9-Jul-2009) (Proof shortened by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion dfconn2 ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 simpll ⊢ ( ( ( 𝐽 ∈ Conn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝐽 ∈ Conn )
3 simplrl ⊢ ( ( ( 𝐽 ∈ Conn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑥 ∈ 𝐽 )
4 simpr1 ⊢ ( ( ( 𝐽 ∈ Conn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑥 ≠ ∅ )
5 simplrr ⊢ ( ( ( 𝐽 ∈ Conn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑦 ∈ 𝐽 )
6 simpr2 ⊢ ( ( ( 𝐽 ∈ Conn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑦 ≠ ∅ )
7 simpr3 ⊢ ( ( ( 𝐽 ∈ Conn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
8 1 2 3 4 5 6 7 conndisj ⊢ ( ( ( 𝐽 ∈ Conn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 )
9 8 ex ⊢ ( ( 𝐽 ∈ Conn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) )
10 9 ralrimivva ⊢ ( 𝐽 ∈ Conn → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) )
11 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
12 1 cldopn ⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 )
13 12 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 )
14 df-3an ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
15 ineq2 ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) )
16 disjdif ⊢ ( 𝑥 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅
17 15 16 eqtrdi ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
18 17 biantrud ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) )
19 neeq1 ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( 𝑦 ≠ ∅ ↔ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) )
20 19 anbi2d ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ↔ ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) ) )
21 18 20 bitr3d ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) ) )
22 14 21 bitrid ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) ) )
23 uneq2 ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( 𝑥 ∪ 𝑦 ) = ( 𝑥 ∪ ( ∪ 𝐽 ∖ 𝑥 ) ) )
24 undif2 ⊢ ( 𝑥 ∪ ( ∪ 𝐽 ∖ 𝑥 ) ) = ( 𝑥 ∪ ∪ 𝐽 )
25 23 24 eqtrdi ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( 𝑥 ∪ 𝑦 ) = ( 𝑥 ∪ ∪ 𝐽 ) )
26 25 neeq1d ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ↔ ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) )
27 22 26 imbi12d ⊢ ( 𝑦 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ↔ ( ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ) )
28 27 rspcv ⊢ ( ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 → ( ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) → ( ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ) )
29 13 28 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) → ( ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ) )
30 1 cldss ⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ ∪ 𝐽 )
31 30 adantl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ⊆ ∪ 𝐽 )
32 ssequn1 ⊢ ( 𝑥 ⊆ ∪ 𝐽 ↔ ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 )
33 31 32 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 )
34 ssdif0 ⊢ ( ∪ 𝐽 ⊆ 𝑥 ↔ ( ∪ 𝐽 ∖ 𝑥 ) = ∅ )
35 idd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ⊆ 𝑥 → ∪ 𝐽 ⊆ 𝑥 ) )
36 35 31 jctild ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ⊆ 𝑥 → ( 𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥 ) ) )
37 eqss ⊢ ( 𝑥 = ∪ 𝐽 ↔ ( 𝑥 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ⊆ 𝑥 ) )
38 36 37 imbitrrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ⊆ 𝑥 → 𝑥 = ∪ 𝐽 ) )
39 34 38 biimtrrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ∪ 𝐽 ∖ 𝑥 ) = ∅ → 𝑥 = ∪ 𝐽 ) )
40 33 39 embantd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) → 𝑥 = ∪ 𝐽 ) )
41 40 orim2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑥 = ∅ ∨ ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) ) → ( 𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽 ) ) )
42 impexp ⊢ ( ( ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ↔ ( 𝑥 ≠ ∅ → ( ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ) )
43 df-ne ⊢ ( 𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅ )
44 id ⊢ ( ( ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) → ( ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) )
45 44 necon4d ⊢ ( ( ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) → ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) )
46 id ⊢ ( ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) → ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) )
47 46 necon3d ⊢ ( ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) → ( ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) )
48 45 47 impbii ⊢ ( ( ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ↔ ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) )
49 43 48 imbi12i ⊢ ( ( 𝑥 ≠ ∅ → ( ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ) ↔ ( ¬ 𝑥 = ∅ → ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) ) )
50 pm4.64 ⊢ ( ( ¬ 𝑥 = ∅ → ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) ) ↔ ( 𝑥 = ∅ ∨ ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) ) )
51 49 50 bitri ⊢ ( ( 𝑥 ≠ ∅ → ( ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ) ↔ ( 𝑥 = ∅ ∨ ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) ) )
52 42 51 bitri ⊢ ( ( ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) ↔ ( 𝑥 = ∅ ∨ ( ( 𝑥 ∪ ∪ 𝐽 ) = ∪ 𝐽 → ( ∪ 𝐽 ∖ 𝑥 ) = ∅ ) ) )
53 vex ⊢ 𝑥 ∈ V
54 53 elpr ⊢ ( 𝑥 ∈ { ∅ , ∪ 𝐽 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = ∪ 𝐽 ) )
55 41 52 54 3imtr4g ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑥 ≠ ∅ ∧ ( ∪ 𝐽 ∖ 𝑥 ) ≠ ∅ ) → ( 𝑥 ∪ ∪ 𝐽 ) ≠ ∪ 𝐽 ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) )
56 29 55 syld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) )
57 56 ex ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → ( ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ) )
58 57 com23 ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ) )
59 58 imim2d ⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 → ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) → ( 𝑥 ∈ 𝐽 → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ) ) )
60 elin ⊢ ( 𝑥 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ↔ ( 𝑥 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
61 60 imbi1i ⊢ ( ( 𝑥 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ↔ ( ( 𝑥 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) )
62 impexp ⊢ ( ( ( 𝑥 ∈ 𝐽 ∧ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ↔ ( 𝑥 ∈ 𝐽 → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ) )
63 61 62 bitri ⊢ ( ( 𝑥 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ↔ ( 𝑥 ∈ 𝐽 → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ) )
64 59 63 imbitrrdi ⊢ ( 𝐽 ∈ Top → ( ( 𝑥 ∈ 𝐽 → ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) → ( 𝑥 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ) )
65 64 alimdv ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ( 𝑥 ∈ 𝐽 → ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) → ∀ 𝑥 ( 𝑥 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) ) )
66 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐽 → ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
67 df-ss ⊢ ( ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , ∪ 𝐽 } ↔ ∀ 𝑥 ( 𝑥 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) → 𝑥 ∈ { ∅ , ∪ 𝐽 } ) )
68 65 66 67 3imtr4g ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) → ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , ∪ 𝐽 } ) )
69 1 isconn2 ⊢ ( 𝐽 ∈ Conn ↔ ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , ∪ 𝐽 } ) )
70 69 baib ⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Conn ↔ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ⊆ { ∅ , ∪ 𝐽 } ) )
71 68 70 sylibrd ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) → 𝐽 ∈ Conn ) )
72 11 71 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) → 𝐽 ∈ Conn ) )
73 10 72 impbid2 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
74 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
75 74 neeq2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( 𝑥 ∪ 𝑦 ) ≠ 𝑋 ↔ ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) )
76 75 imbi2d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ 𝑋 ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
77 76 2ralbidv ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
78 73 77 bitr4d ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ 𝑋 ) ) )