# Metamath Proof Explorer

## Theorem pconnconn

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

Ref Expression
Assertion pconnconn ${⊢}{J}\in \mathrm{PConn}\to {J}\in \mathrm{Conn}$

### Proof

Step Hyp Ref Expression
1 df-3an ${⊢}\left({x}\ne \varnothing \wedge {y}\ne \varnothing \wedge {x}\cap {y}=\varnothing \right)↔\left(\left({x}\ne \varnothing \wedge {y}\ne \varnothing \right)\wedge {x}\cap {y}=\varnothing \right)$
2 n0 ${⊢}{x}\ne \varnothing ↔\exists {a}\phantom{\rule{.4em}{0ex}}{a}\in {x}$
3 n0 ${⊢}{y}\ne \varnothing ↔\exists {b}\phantom{\rule{.4em}{0ex}}{b}\in {y}$
4 2 3 anbi12i ${⊢}\left({x}\ne \varnothing \wedge {y}\ne \varnothing \right)↔\left(\exists {a}\phantom{\rule{.4em}{0ex}}{a}\in {x}\wedge \exists {b}\phantom{\rule{.4em}{0ex}}{b}\in {y}\right)$
5 exdistrv ${⊢}\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({a}\in {x}\wedge {b}\in {y}\right)↔\left(\exists {a}\phantom{\rule{.4em}{0ex}}{a}\in {x}\wedge \exists {b}\phantom{\rule{.4em}{0ex}}{b}\in {y}\right)$
6 4 5 bitr4i ${⊢}\left({x}\ne \varnothing \wedge {y}\ne \varnothing \right)↔\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({a}\in {x}\wedge {b}\in {y}\right)$
7 simpll ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to {J}\in \mathrm{PConn}$
8 simprll ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to {a}\in {x}$
9 simplrl ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to {x}\in {J}$
10 elunii ${⊢}\left({a}\in {x}\wedge {x}\in {J}\right)\to {a}\in \bigcup {J}$
11 8 9 10 syl2anc ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to {a}\in \bigcup {J}$
12 simprlr ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to {b}\in {y}$
13 simplrr ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to {y}\in {J}$
14 elunii ${⊢}\left({b}\in {y}\wedge {y}\in {J}\right)\to {b}\in \bigcup {J}$
15 12 13 14 syl2anc ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to {b}\in \bigcup {J}$
16 eqid ${⊢}\bigcup {J}=\bigcup {J}$
17 16 pconncn ${⊢}\left({J}\in \mathrm{PConn}\wedge {a}\in \bigcup {J}\wedge {b}\in \bigcup {J}\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)$
18 7 11 15 17 syl3anc ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to \exists {f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\phantom{\rule{.4em}{0ex}}\left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)$
19 simplrr ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {x}\cap {y}=\varnothing$
20 simplrr ${⊢}\left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\to {f}\left(1\right)={b}$
21 20 adantl ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {f}\left(1\right)={b}$
22 iiuni ${⊢}\left[0,1\right]=\bigcup \mathrm{II}$
23 iiconn ${⊢}\mathrm{II}\in \mathrm{Conn}$
24 23 a1i ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to \mathrm{II}\in \mathrm{Conn}$
25 simprll ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)$
26 9 adantr ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {x}\in {J}$
27 uncom ${⊢}{y}\cup {x}={x}\cup {y}$
28 simprr ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {x}\cup {y}=\bigcup {J}$
29 27 28 syl5eq ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {y}\cup {x}=\bigcup {J}$
30 13 adantr ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {y}\in {J}$
31 elssuni ${⊢}{y}\in {J}\to {y}\subseteq \bigcup {J}$
32 30 31 syl ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {y}\subseteq \bigcup {J}$
33 incom ${⊢}{y}\cap {x}={x}\cap {y}$
34 33 19 syl5eq ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {y}\cap {x}=\varnothing$
35 uneqdifeq ${⊢}\left({y}\subseteq \bigcup {J}\wedge {y}\cap {x}=\varnothing \right)\to \left({y}\cup {x}=\bigcup {J}↔\bigcup {J}\setminus {y}={x}\right)$
36 32 34 35 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to \left({y}\cup {x}=\bigcup {J}↔\bigcup {J}\setminus {y}={x}\right)$
37 29 36 mpbid ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to \bigcup {J}\setminus {y}={x}$
38 pconntop ${⊢}{J}\in \mathrm{PConn}\to {J}\in \mathrm{Top}$
39 38 ad3antrrr ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {J}\in \mathrm{Top}$
40 16 opncld ${⊢}\left({J}\in \mathrm{Top}\wedge {y}\in {J}\right)\to \bigcup {J}\setminus {y}\in \mathrm{Clsd}\left({J}\right)$
41 39 30 40 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to \bigcup {J}\setminus {y}\in \mathrm{Clsd}\left({J}\right)$
42 37 41 eqeltrrd ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {x}\in \mathrm{Clsd}\left({J}\right)$
43 0elunit ${⊢}0\in \left[0,1\right]$
44 43 a1i ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to 0\in \left[0,1\right]$
45 simplrl ${⊢}\left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\to {f}\left(0\right)={a}$
46 45 adantl ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {f}\left(0\right)={a}$
47 8 adantr ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {a}\in {x}$
48 46 47 eqeltrd ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {f}\left(0\right)\in {x}$
49 22 24 25 26 42 44 48 conncn ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {f}:\left[0,1\right]⟶{x}$
50 1elunit ${⊢}1\in \left[0,1\right]$
51 ffvelrn ${⊢}\left({f}:\left[0,1\right]⟶{x}\wedge 1\in \left[0,1\right]\right)\to {f}\left(1\right)\in {x}$
52 49 50 51 sylancl ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {f}\left(1\right)\in {x}$
53 21 52 eqeltrrd ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {b}\in {x}$
54 12 adantr ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {b}\in {y}$
55 inelcm ${⊢}\left({b}\in {x}\wedge {b}\in {y}\right)\to {x}\cap {y}\ne \varnothing$
56 53 54 55 syl2anc ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to {x}\cap {y}\ne \varnothing$
57 19 56 pm2.21ddne ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left(\left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\wedge {x}\cup {y}=\bigcup {J}\right)\right)\to ¬{x}\cup {y}=\bigcup {J}$
58 57 expr ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\right)\to \left({x}\cup {y}=\bigcup {J}\to ¬{x}\cup {y}=\bigcup {J}\right)$
59 58 pm2.01d ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\right)\to ¬{x}\cup {y}=\bigcup {J}$
60 59 neqned ${⊢}\left(\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\wedge \left({f}\in \left(\mathrm{II}\mathrm{Cn}{J}\right)\wedge \left({f}\left(0\right)={a}\wedge {f}\left(1\right)={b}\right)\right)\right)\to {x}\cup {y}\ne \bigcup {J}$
61 18 60 rexlimddv ${⊢}\left(\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\wedge \left(\left({a}\in {x}\wedge {b}\in {y}\right)\wedge {x}\cap {y}=\varnothing \right)\right)\to {x}\cup {y}\ne \bigcup {J}$
62 61 exp32 ${⊢}\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left(\left({a}\in {x}\wedge {b}\in {y}\right)\to \left({x}\cap {y}=\varnothing \to {x}\cup {y}\ne \bigcup {J}\right)\right)$
63 62 exlimdvv ${⊢}\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left(\exists {a}\phantom{\rule{.4em}{0ex}}\exists {b}\phantom{\rule{.4em}{0ex}}\left({a}\in {x}\wedge {b}\in {y}\right)\to \left({x}\cap {y}=\varnothing \to {x}\cup {y}\ne \bigcup {J}\right)\right)$
64 6 63 syl5bi ${⊢}\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left(\left({x}\ne \varnothing \wedge {y}\ne \varnothing \right)\to \left({x}\cap {y}=\varnothing \to {x}\cup {y}\ne \bigcup {J}\right)\right)$
65 64 impd ${⊢}\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left(\left(\left({x}\ne \varnothing \wedge {y}\ne \varnothing \right)\wedge {x}\cap {y}=\varnothing \right)\to {x}\cup {y}\ne \bigcup {J}\right)$
66 1 65 syl5bi ${⊢}\left({J}\in \mathrm{PConn}\wedge \left({x}\in {J}\wedge {y}\in {J}\right)\right)\to \left(\left({x}\ne \varnothing \wedge {y}\ne \varnothing \wedge {x}\cap {y}=\varnothing \right)\to {x}\cup {y}\ne \bigcup {J}\right)$
67 66 ralrimivva ${⊢}{J}\in \mathrm{PConn}\to \forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\left(\left({x}\ne \varnothing \wedge {y}\ne \varnothing \wedge {x}\cap {y}=\varnothing \right)\to {x}\cup {y}\ne \bigcup {J}\right)$
68 16 toptopon ${⊢}{J}\in \mathrm{Top}↔{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
69 38 68 sylib ${⊢}{J}\in \mathrm{PConn}\to {J}\in \mathrm{TopOn}\left(\bigcup {J}\right)$
70 dfconn2 ${⊢}{J}\in \mathrm{TopOn}\left(\bigcup {J}\right)\to \left({J}\in \mathrm{Conn}↔\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\left(\left({x}\ne \varnothing \wedge {y}\ne \varnothing \wedge {x}\cap {y}=\varnothing \right)\to {x}\cup {y}\ne \bigcup {J}\right)\right)$
71 69 70 syl ${⊢}{J}\in \mathrm{PConn}\to \left({J}\in \mathrm{Conn}↔\forall {x}\in {J}\phantom{\rule{.4em}{0ex}}\forall {y}\in {J}\phantom{\rule{.4em}{0ex}}\left(\left({x}\ne \varnothing \wedge {y}\ne \varnothing \wedge {x}\cap {y}=\varnothing \right)\to {x}\cup {y}\ne \bigcup {J}\right)\right)$
72 67 71 mpbird ${⊢}{J}\in \mathrm{PConn}\to {J}\in \mathrm{Conn}$