Metamath Proof Explorer

Theorem pconnconn

Description: A path-connected space is connected. (Contributed by Mario Carneiro, 11-Feb-2015)

Ref Expression
Assertion pconnconn ( 𝐽 ∈ PConn → 𝐽 ∈ Conn )

Proof

Step Hyp Ref Expression
1 df-3an ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
2 n0 ⊢ ( 𝑥 ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ 𝑥 )
3 n0 ⊢ ( 𝑦 ≠ ∅ ↔ ∃ 𝑏 𝑏 ∈ 𝑦 )
4 2 3 anbi12i ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ↔ ( ∃ 𝑎 𝑎 ∈ 𝑥 ∧ ∃ 𝑏 𝑏 ∈ 𝑦 ) )
5 exdistrv ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ↔ ( ∃ 𝑎 𝑎 ∈ 𝑥 ∧ ∃ 𝑏 𝑏 ∈ 𝑦 ) )
6 4 5 bitr4i ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) )
7 simpll ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝐽 ∈ PConn )
8 simprll ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑎 ∈ 𝑥 )
9 simplrl ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑥 ∈ 𝐽 )
10 elunii ⊢ ( ( 𝑎 ∈ 𝑥 ∧ 𝑥 ∈ 𝐽 ) → 𝑎 ∈ ∪ 𝐽 )
11 8 9 10 syl2anc ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑎 ∈ ∪ 𝐽 )
12 simprlr ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑏 ∈ 𝑦 )
13 simplrr ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑦 ∈ 𝐽 )
14 elunii ⊢ ( ( 𝑏 ∈ 𝑦 ∧ 𝑦 ∈ 𝐽 ) → 𝑏 ∈ ∪ 𝐽 )
15 12 13 14 syl2anc ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑏 ∈ ∪ 𝐽 )
16 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
17 16 pconncn ⊢ ( ( 𝐽 ∈ PConn ∧ 𝑎 ∈ ∪ 𝐽 ∧ 𝑏 ∈ ∪ 𝐽 ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) )
18 7 11 15 17 syl3anc ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ∃ 𝑓 ∈ ( II Cn 𝐽 ) ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) )
19 simplrr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) = ∅ )
20 simplrr ⊢ ( ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) → ( 𝑓 ‘ 1 ) = 𝑏 )
21 20 adantl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑓 ‘ 1 ) = 𝑏 )
22 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
23 iiconn ⊢ II ∈ Conn
24 23 a1i ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → II ∈ Conn )
25 simprll ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑓 ∈ ( II Cn 𝐽 ) )
26 9 adantr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑥 ∈ 𝐽 )
27 uncom ⊢ ( 𝑦 ∪ 𝑥 ) = ( 𝑥 ∪ 𝑦 )
28 simprr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 )
29 27 28 syl5eq ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑦 ∪ 𝑥 ) = ∪ 𝐽 )
30 13 adantr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑦 ∈ 𝐽 )
31 elssuni ⊢ ( 𝑦 ∈ 𝐽 → 𝑦 ⊆ ∪ 𝐽 )
32 30 31 syl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑦 ⊆ ∪ 𝐽 )
33 incom ⊢ ( 𝑦 ∩ 𝑥 ) = ( 𝑥 ∩ 𝑦 )
34 33 19 syl5eq ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑦 ∩ 𝑥 ) = ∅ )
35 uneqdifeq ⊢ ( ( 𝑦 ⊆ ∪ 𝐽 ∧ ( 𝑦 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∪ 𝑥 ) = ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ 𝑦 ) = 𝑥 ) )
36 32 34 35 syl2anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( ( 𝑦 ∪ 𝑥 ) = ∪ 𝐽 ↔ ( ∪ 𝐽 ∖ 𝑦 ) = 𝑥 ) )
37 29 36 mpbid ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( ∪ 𝐽 ∖ 𝑦 ) = 𝑥 )
38 pconntop ⊢ ( 𝐽 ∈ PConn → 𝐽 ∈ Top )
39 38 ad3antrrr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝐽 ∈ Top )
40 16 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
41 39 30 40 syl2anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) )
42 37 41 eqeltrrd ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑥 ∈ ( Clsd ‘ 𝐽 ) )
43 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
44 43 a1i ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 0 ∈ ( 0 [,] 1 ) )
45 simplrl ⊢ ( ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) → ( 𝑓 ‘ 0 ) = 𝑎 )
46 45 adantl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑓 ‘ 0 ) = 𝑎 )
47 8 adantr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑎 ∈ 𝑥 )
48 46 47 eqeltrd ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑓 ‘ 0 ) ∈ 𝑥 )
49 22 24 25 26 42 44 48 conncn ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ 𝑥 )
50 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
51 ffvelrn ⊢ ( ( 𝑓 : ( 0 [,] 1 ) ⟶ 𝑥 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑓 ‘ 1 ) ∈ 𝑥 )
52 49 50 51 sylancl ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑓 ‘ 1 ) ∈ 𝑥 )
53 21 52 eqeltrrd ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑏 ∈ 𝑥 )
54 12 adantr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → 𝑏 ∈ 𝑦 )
55 inelcm ⊢ ( ( 𝑏 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) → ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
56 53 54 55 syl2anc ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ( 𝑥 ∩ 𝑦 ) ≠ ∅ )
57 19 56 pm2.21ddne ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ∧ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) ) → ¬ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 )
58 57 expr ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ) → ( ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 → ¬ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 ) )
59 58 pm2.01d ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ) → ¬ ( 𝑥 ∪ 𝑦 ) = ∪ 𝐽 )
60 59 neqned ⊢ ( ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ∧ ( 𝑓 ∈ ( II Cn 𝐽 ) ∧ ( ( 𝑓 ‘ 0 ) = 𝑎 ∧ ( 𝑓 ‘ 1 ) = 𝑏 ) ) ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 )
61 18 60 rexlimddv ⊢ ( ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) ∧ ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 )
62 61 exp32 ⊢ ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
63 62 exlimdvv ⊢ ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ∈ 𝑥 ∧ 𝑏 ∈ 𝑦 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
64 6 63 syl5bi ⊢ ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
65 64 impd ⊢ ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) )
66 1 65 syl5bi ⊢ ( ( 𝐽 ∈ PConn ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) )
67 66 ralrimivva ⊢ ( 𝐽 ∈ PConn → ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) )
68 16 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
69 38 68 sylib ⊢ ( 𝐽 ∈ PConn → 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) )
70 dfconn2 ⊢ ( 𝐽 ∈ ( TopOn ‘ ∪ 𝐽 ) → ( 𝐽 ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
71 69 70 syl ⊢ ( 𝐽 ∈ PConn → ( 𝐽 ∈ Conn ↔ ∀ 𝑥 ∈ 𝐽 ∀ 𝑦 ∈ 𝐽 ( ( 𝑥 ≠ ∅ ∧ 𝑦 ≠ ∅ ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∪ 𝑦 ) ≠ ∪ 𝐽 ) ) )
72 67 71 mpbird ⊢ ( 𝐽 ∈ PConn → 𝐽 ∈ Conn )