Metamath Proof Explorer

Theorem indispconn

Description: The indiscrete topology (or trivial topology) on any set is path-connected. (Contributed by Mario Carneiro, 7-Jul-2015) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion indispconn ⊢ ∅ A ∈ PConn

Proof

Step Hyp Ref Expression
1 indistop ⊢ ∅ A ∈ Top
2 simpl ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → x ∈ ⋃ ∅ A
3 0ex ⊢ ∅ ∈ V
4 n0i ⊢ x ∈ ⋃ ∅ A → ¬ ⋃ ∅ A = ∅
5 prprc2 ⊢ ¬ A ∈ V → ∅ A = ∅
6 5 unieqd ⊢ ¬ A ∈ V → ⋃ ∅ A = ⋃ ∅
7 3 unisn ⊢ ⋃ ∅ = ∅
8 6 7 eqtrdi ⊢ ¬ A ∈ V → ⋃ ∅ A = ∅
9 4 8 nsyl2 ⊢ x ∈ ⋃ ∅ A → A ∈ V
10 9 adantr ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → A ∈ V
11 uniprg ⊢ ∅ ∈ V ∧ A ∈ V → ⋃ ∅ A = ∅ ∪ A
12 3 10 11 sylancr ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → ⋃ ∅ A = ∅ ∪ A
13 uncom ⊢ ∅ ∪ A = A ∪ ∅
14 un0 ⊢ A ∪ ∅ = A
15 13 14 eqtri ⊢ ∅ ∪ A = A
16 12 15 eqtrdi ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → ⋃ ∅ A = A
17 2 16 eleqtrd ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → x ∈ A
18 simpr ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → y ∈ ⋃ ∅ A
19 18 16 eleqtrd ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → y ∈ A
20 17 19 ifcld ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → if z = 0 x y ∈ A
21 20 adantr ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A ∧ z ∈ 0 1 → if z = 0 x y ∈ A
22 21 fmpttd ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → z ∈ 0 1 ⟼ if z = 0 x y : 0 1 ⟶ A
23 ovex ⊢ 0 1 ∈ V
24 elmapg ⊢ A ∈ V ∧ 0 1 ∈ V → z ∈ 0 1 ⟼ if z = 0 x y ∈ A 0 1 ↔ z ∈ 0 1 ⟼ if z = 0 x y : 0 1 ⟶ A
25 10 23 24 sylancl ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → z ∈ 0 1 ⟼ if z = 0 x y ∈ A 0 1 ↔ z ∈ 0 1 ⟼ if z = 0 x y : 0 1 ⟶ A
26 22 25 mpbird ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → z ∈ 0 1 ⟼ if z = 0 x y ∈ A 0 1
27 iitopon ⊢ II ∈ TopOn ⁡ 0 1
28 cnindis ⊢ II ∈ TopOn ⁡ 0 1 ∧ A ∈ V → II Cn ∅ A = A 0 1
29 27 10 28 sylancr ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → II Cn ∅ A = A 0 1
30 26 29 eleqtrrd ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → z ∈ 0 1 ⟼ if z = 0 x y ∈ II Cn ∅ A
31 0elunit ⊢ 0 ∈ 0 1
32 iftrue ⊢ z = 0 → if z = 0 x y = x
33 eqid ⊢ z ∈ 0 1 ⟼ if z = 0 x y = z ∈ 0 1 ⟼ if z = 0 x y
34 vex ⊢ x ∈ V
35 32 33 34 fvmpt ⊢ 0 ∈ 0 1 → z ∈ 0 1 ⟼ if z = 0 x y ⁡ 0 = x
36 31 35 mp1i ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → z ∈ 0 1 ⟼ if z = 0 x y ⁡ 0 = x
37 1elunit ⊢ 1 ∈ 0 1
38 ax-1ne0 ⊢ 1 ≠ 0
39 neeq1 ⊢ z = 1 → z ≠ 0 ↔ 1 ≠ 0
40 38 39 mpbiri ⊢ z = 1 → z ≠ 0
41 ifnefalse ⊢ z ≠ 0 → if z = 0 x y = y
42 40 41 syl ⊢ z = 1 → if z = 0 x y = y
43 vex ⊢ y ∈ V
44 42 33 43 fvmpt ⊢ 1 ∈ 0 1 → z ∈ 0 1 ⟼ if z = 0 x y ⁡ 1 = y
45 37 44 mp1i ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → z ∈ 0 1 ⟼ if z = 0 x y ⁡ 1 = y
46 fveq1 ⊢ f = z ∈ 0 1 ⟼ if z = 0 x y → f ⁡ 0 = z ∈ 0 1 ⟼ if z = 0 x y ⁡ 0
47 46 eqeq1d ⊢ f = z ∈ 0 1 ⟼ if z = 0 x y → f ⁡ 0 = x ↔ z ∈ 0 1 ⟼ if z = 0 x y ⁡ 0 = x
48 fveq1 ⊢ f = z ∈ 0 1 ⟼ if z = 0 x y → f ⁡ 1 = z ∈ 0 1 ⟼ if z = 0 x y ⁡ 1
49 48 eqeq1d ⊢ f = z ∈ 0 1 ⟼ if z = 0 x y → f ⁡ 1 = y ↔ z ∈ 0 1 ⟼ if z = 0 x y ⁡ 1 = y
50 47 49 anbi12d ⊢ f = z ∈ 0 1 ⟼ if z = 0 x y → f ⁡ 0 = x ∧ f ⁡ 1 = y ↔ z ∈ 0 1 ⟼ if z = 0 x y ⁡ 0 = x ∧ z ∈ 0 1 ⟼ if z = 0 x y ⁡ 1 = y
51 50 rspcev ⊢ z ∈ 0 1 ⟼ if z = 0 x y ∈ II Cn ∅ A ∧ z ∈ 0 1 ⟼ if z = 0 x y ⁡ 0 = x ∧ z ∈ 0 1 ⟼ if z = 0 x y ⁡ 1 = y → ∃ f ∈ II Cn ∅ A f ⁡ 0 = x ∧ f ⁡ 1 = y
52 30 36 45 51 syl12anc ⊢ x ∈ ⋃ ∅ A ∧ y ∈ ⋃ ∅ A → ∃ f ∈ II Cn ∅ A f ⁡ 0 = x ∧ f ⁡ 1 = y
53 52 rgen2 ⊢ ∀ x ∈ ⋃ ∅ A ∀ y ∈ ⋃ ∅ A ∃ f ∈ II Cn ∅ A f ⁡ 0 = x ∧ f ⁡ 1 = y
54 eqid ⊢ ⋃ ∅ A = ⋃ ∅ A
55 54 ispconn ⊢ ∅ A ∈ PConn ↔ ∅ A ∈ Top ∧ ∀ x ∈ ⋃ ∅ A ∀ y ∈ ⋃ ∅ A ∃ f ∈ II Cn ∅ A f ⁡ 0 = x ∧ f ⁡ 1 = y
56 1 53 55 mpbir2an ⊢ ∅ A ∈ PConn