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 { ∅ , 𝐴 } ∈ PConn

Proof

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