Metamath Proof Explorer

Theorem indishmph

Description: Equinumerous sets equipped with their indiscrete topologies are homeomorphic (which means in that particular case that a segment is homeomorphic to a circle contrary to what Wikipedia claims). (Contributed by FL, 17-Aug-2008) (Proof shortened by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion indishmph 
|- ( A ~~ B -> { (/) , A } ~= { (/) , B } )

Proof

Step Hyp Ref Expression
1 bren 
 |-  ( A ~~ B <-> E. f f : A -1-1-onto-> B )
2 f1of 
 |-  ( f : A -1-1-onto-> B -> f : A --> B )
3 f1odm 
 |-  ( f : A -1-1-onto-> B -> dom f = A )
4 vex 
 |-  f e. _V
5 4 dmex 
 |-  dom f e. _V
6 3 5 eqeltrrdi 
 |-  ( f : A -1-1-onto-> B -> A e. _V )
7 f1ofo 
 |-  ( f : A -1-1-onto-> B -> f : A -onto-> B )
8 focdmex 
 |-  ( A e. _V -> ( f : A -onto-> B -> B e. _V ) )
9 6 7 8 sylc 
 |-  ( f : A -1-1-onto-> B -> B e. _V )
10 9 6 elmapd 
 |-  ( f : A -1-1-onto-> B -> ( f e. ( B ^m A ) <-> f : A --> B ) )
11 2 10 mpbird 
 |-  ( f : A -1-1-onto-> B -> f e. ( B ^m A ) )
12 indistopon 
 |-  ( A e. _V -> { (/) , A } e. ( TopOn ` A ) )
13 6 12 syl 
 |-  ( f : A -1-1-onto-> B -> { (/) , A } e. ( TopOn ` A ) )
14 cnindis 
 |-  ( ( { (/) , A } e. ( TopOn ` A ) /\ B e. _V ) -> ( { (/) , A } Cn { (/) , B } ) = ( B ^m A ) )
15 13 9 14 syl2anc 
 |-  ( f : A -1-1-onto-> B -> ( { (/) , A } Cn { (/) , B } ) = ( B ^m A ) )
16 11 15 eleqtrrd 
 |-  ( f : A -1-1-onto-> B -> f e. ( { (/) , A } Cn { (/) , B } ) )
17 f1ocnv 
 |-  ( f : A -1-1-onto-> B -> `' f : B -1-1-onto-> A )
18 f1of 
 |-  ( `' f : B -1-1-onto-> A -> `' f : B --> A )
19 17 18 syl 
 |-  ( f : A -1-1-onto-> B -> `' f : B --> A )
20 6 9 elmapd 
 |-  ( f : A -1-1-onto-> B -> ( `' f e. ( A ^m B ) <-> `' f : B --> A ) )
21 19 20 mpbird 
 |-  ( f : A -1-1-onto-> B -> `' f e. ( A ^m B ) )
22 indistopon 
 |-  ( B e. _V -> { (/) , B } e. ( TopOn ` B ) )
23 9 22 syl 
 |-  ( f : A -1-1-onto-> B -> { (/) , B } e. ( TopOn ` B ) )
24 cnindis 
 |-  ( ( { (/) , B } e. ( TopOn ` B ) /\ A e. _V ) -> ( { (/) , B } Cn { (/) , A } ) = ( A ^m B ) )
25 23 6 24 syl2anc 
 |-  ( f : A -1-1-onto-> B -> ( { (/) , B } Cn { (/) , A } ) = ( A ^m B ) )
26 21 25 eleqtrrd 
 |-  ( f : A -1-1-onto-> B -> `' f e. ( { (/) , B } Cn { (/) , A } ) )
27 ishmeo 
 |-  ( f e. ( { (/) , A } Homeo { (/) , B } ) <-> ( f e. ( { (/) , A } Cn { (/) , B } ) /\ `' f e. ( { (/) , B } Cn { (/) , A } ) ) )
28 16 26 27 sylanbrc 
 |-  ( f : A -1-1-onto-> B -> f e. ( { (/) , A } Homeo { (/) , B } ) )
29 hmphi 
 |-  ( f e. ( { (/) , A } Homeo { (/) , B } ) -> { (/) , A } ~= { (/) , B } )
30 28 29 syl 
 |-  ( f : A -1-1-onto-> B -> { (/) , A } ~= { (/) , B } )
31 30 exlimiv 
 |-  ( E. f f : A -1-1-onto-> B -> { (/) , A } ~= { (/) , B } )
32 1 31 sylbi 
 |-  ( A ~~ B -> { (/) , A } ~= { (/) , B } )