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 \approx B \to \{\emptyset, A\} ≃ \{\emptyset, B\}$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B$
2		f1of	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A ⟶ B$
3		f1odm	$⊢ f : A \underset{1-1 onto}{⟶} B \to dom f = A$
4		vex	$⊢ f \in V$
5	4	dmex	$⊢ dom f \in V$
6	3 5	eqeltrrdi	$⊢ f : A \underset{1-1 onto}{⟶} B \to A \in V$
7		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
8		focdmex	$⊢ A \in V \to (f : A \underset{onto}{⟶} B \to B \in V)$
9	6 7 8	sylc	$⊢ f : A \underset{1-1 onto}{⟶} B \to B \in V$
10	9 6	elmapd	$⊢ f : A \underset{1-1 onto}{⟶} B \to (f \in (B^{A}) \leftrightarrow f : A ⟶ B)$
11	2 10	mpbird	$⊢ f : A \underset{1-1 onto}{⟶} B \to f \in (B^{A})$
12		indistopon	$⊢ A \in V \to \{\emptyset, A\} \in TopOn (A)$
13	6 12	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to \{\emptyset, A\} \in TopOn (A)$
14		cnindis	$⊢ (\{\emptyset, A\} \in TopOn (A) \land B \in V) \to \{\emptyset, A\} Cn \{\emptyset, B\} = B^{A}$
15	13 9 14	syl2anc	$⊢ f : A \underset{1-1 onto}{⟶} B \to \{\emptyset, A\} Cn \{\emptyset, B\} = B^{A}$
16	11 15	eleqtrrd	$⊢ f : A \underset{1-1 onto}{⟶} B \to f \in (\{\emptyset, A\} Cn \{\emptyset, B\})$
17		f1ocnv	$⊢ f : A \underset{1-1 onto}{⟶} B \to f^{-1} : B \underset{1-1 onto}{⟶} A$
18		f1of	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to f^{-1} : B ⟶ A$
19	17 18	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to f^{-1} : B ⟶ A$
20	6 9	elmapd	$⊢ f : A \underset{1-1 onto}{⟶} B \to (f^{-1} \in (A^{B}) \leftrightarrow f^{-1} : B ⟶ A)$
21	19 20	mpbird	$⊢ f : A \underset{1-1 onto}{⟶} B \to f^{-1} \in (A^{B})$
22		indistopon	$⊢ B \in V \to \{\emptyset, B\} \in TopOn (B)$
23	9 22	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to \{\emptyset, B\} \in TopOn (B)$
24		cnindis	$⊢ (\{\emptyset, B\} \in TopOn (B) \land A \in V) \to \{\emptyset, B\} Cn \{\emptyset, A\} = A^{B}$
25	23 6 24	syl2anc	$⊢ f : A \underset{1-1 onto}{⟶} B \to \{\emptyset, B\} Cn \{\emptyset, A\} = A^{B}$
26	21 25	eleqtrrd	$⊢ f : A \underset{1-1 onto}{⟶} B \to f^{-1} \in (\{\emptyset, B\} Cn \{\emptyset, A\})$
27		ishmeo	$⊢ f \in (\{\emptyset, A\} Homeo \{\emptyset, B\}) \leftrightarrow (f \in (\{\emptyset, A\} Cn \{\emptyset, B\}) \land f^{-1} \in (\{\emptyset, B\} Cn \{\emptyset, A\}))$
28	16 26 27	sylanbrc	$⊢ f : A \underset{1-1 onto}{⟶} B \to f \in (\{\emptyset, A\} Homeo \{\emptyset, B\})$
29		hmphi	$⊢ f \in (\{\emptyset, A\} Homeo \{\emptyset, B\}) \to \{\emptyset, A\} ≃ \{\emptyset, B\}$
30	28 29	syl	$⊢ f : A \underset{1-1 onto}{⟶} B \to \{\emptyset, A\} ≃ \{\emptyset, B\}$
31	30	exlimiv	$⊢ \exists f f : A \underset{1-1 onto}{⟶} B \to \{\emptyset, A\} ≃ \{\emptyset, B\}$
32	1 31	sylbi	$⊢ A \approx B \to \{\emptyset, A\} ≃ \{\emptyset, B\}$

Metamath Proof Explorer

Theorem indishmph

Proof