cnhaus

Description: The preimage of a Hausdorff topology under an injective map is Hausdorff. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Assertion	cnhaus	$⊢ (K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to J \in Haus$

Proof

Step	Hyp	Ref	Expression
1		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
2	1	3ad2ant3	$⊢ (K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to J \in Top$
3		simpl1	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to K \in Haus$
4		simpl3	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to F \in (J Cn K)$
5		eqid	$⊢ ⋃ J = ⋃ J$
6		eqid	$⊢ ⋃ K = ⋃ K$
7	5 6	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
8	4 7	syl	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to F : ⋃ J ⟶ ⋃ K$
9		simprll	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to x \in ⋃ J$
10	8 9	ffvelcdmd	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to F (x) \in ⋃ K$
11		simprlr	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to y \in ⋃ J$
12	8 11	ffvelcdmd	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to F (y) \in ⋃ K$
13		simprr	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to x \neq y$
14		simpl2	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to F : X \underset{1-1}{⟶} Y$
15	8	fdmd	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to dom F = ⋃ J$
16		f1dm	$⊢ F : X \underset{1-1}{⟶} Y \to dom F = X$
17	14 16	syl	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to dom F = X$
18	15 17	eqtr3d	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to ⋃ J = X$
19	9 18	eleqtrd	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to x \in X$
20	11 18	eleqtrd	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to y \in X$
21		f1fveq	$⊢ (F : X \underset{1-1}{⟶} Y \land (x \in X \land y \in X)) \to (F (x) = F (y) \leftrightarrow x = y)$
22	14 19 20 21	syl12anc	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to (F (x) = F (y) \leftrightarrow x = y)$
23	22	necon3bid	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to (F (x) \neq F (y) \leftrightarrow x \neq y)$
24	13 23	mpbird	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to F (x) \neq F (y)$
25	6	hausnei	$⊢ (K \in Haus \land (F (x) \in ⋃ K \land F (y) \in ⋃ K \land F (x) \neq F (y))) \to \exists u \in K \exists v \in K (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset)$
26	3 10 12 24 25	syl13anc	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to \exists u \in K \exists v \in K (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset)$
27		simpll3	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F \in (J Cn K)$
28		simprll	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to u \in K$
29		cnima	$⊢ (F \in (J Cn K) \land u \in K) \to F^{-1} [u] \in J$
30	27 28 29	syl2anc	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F^{-1} [u] \in J$
31		simprlr	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to v \in K$
32		cnima	$⊢ (F \in (J Cn K) \land v \in K) \to F^{-1} [v] \in J$
33	27 31 32	syl2anc	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F^{-1} [v] \in J$
34	9	adantr	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to x \in ⋃ J$
35		simprr1	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F (x) \in u$
36	8	adantr	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F : ⋃ J ⟶ ⋃ K$
37	36	ffnd	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F Fn ⋃ J$
38		elpreima	$⊢ F Fn ⋃ J \to (x \in F^{-1} [u] \leftrightarrow (x \in ⋃ J \land F (x) \in u))$
39	37 38	syl	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to (x \in F^{-1} [u] \leftrightarrow (x \in ⋃ J \land F (x) \in u))$
40	34 35 39	mpbir2and	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to x \in F^{-1} [u]$
41	11	adantr	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to y \in ⋃ J$
42		simprr2	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F (y) \in v$
43		elpreima	$⊢ F Fn ⋃ J \to (y \in F^{-1} [v] \leftrightarrow (y \in ⋃ J \land F (y) \in v))$
44	37 43	syl	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to (y \in F^{-1} [v] \leftrightarrow (y \in ⋃ J \land F (y) \in v))$
45	41 42 44	mpbir2and	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to y \in F^{-1} [v]$
46		ffun	$⊢ F : ⋃ J ⟶ ⋃ K \to Fun F$
47		inpreima	$⊢ Fun F \to F^{-1} [u \cap v] = F^{-1} [u] \cap F^{-1} [v]$
48	36 46 47	3syl	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F^{-1} [u \cap v] = F^{-1} [u] \cap F^{-1} [v]$
49		simprr3	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to u \cap v = \emptyset$
50	49	imaeq2d	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F^{-1} [u \cap v] = F^{-1} [\emptyset]$
51		ima0	$⊢ F^{-1} [\emptyset] = \emptyset$
52	50 51	eqtrdi	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F^{-1} [u \cap v] = \emptyset$
53	48 52	eqtr3d	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to F^{-1} [u] \cap F^{-1} [v] = \emptyset$
54		eleq2	$⊢ m = F^{-1} [u] \to (x \in m \leftrightarrow x \in F^{-1} [u])$
55		ineq1	$⊢ m = F^{-1} [u] \to m \cap n = F^{-1} [u] \cap n$
56	55	eqeq1d	$⊢ m = F^{-1} [u] \to (m \cap n = \emptyset \leftrightarrow F^{-1} [u] \cap n = \emptyset)$
57	54 56	3anbi13d	$⊢ m = F^{-1} [u] \to ((x \in m \land y \in n \land m \cap n = \emptyset) \leftrightarrow (x \in F^{-1} [u] \land y \in n \land F^{-1} [u] \cap n = \emptyset))$
58		eleq2	$⊢ n = F^{-1} [v] \to (y \in n \leftrightarrow y \in F^{-1} [v])$
59		ineq2	$⊢ n = F^{-1} [v] \to F^{-1} [u] \cap n = F^{-1} [u] \cap F^{-1} [v]$
60	59	eqeq1d	$⊢ n = F^{-1} [v] \to (F^{-1} [u] \cap n = \emptyset \leftrightarrow F^{-1} [u] \cap F^{-1} [v] = \emptyset)$
61	58 60	3anbi23d	$⊢ n = F^{-1} [v] \to ((x \in F^{-1} [u] \land y \in n \land F^{-1} [u] \cap n = \emptyset) \leftrightarrow (x \in F^{-1} [u] \land y \in F^{-1} [v] \land F^{-1} [u] \cap F^{-1} [v] = \emptyset))$
62	57 61	rspc2ev	$⊢ (F^{-1} [u] \in J \land F^{-1} [v] \in J \land (x \in F^{-1} [u] \land y \in F^{-1} [v] \land F^{-1} [u] \cap F^{-1} [v] = \emptyset)) \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)$
63	30 33 40 45 53 62	syl113anc	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land ((u \in K \land v \in K) \land (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset))) \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)$
64	63	expr	$⊢ (((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \land (u \in K \land v \in K)) \to ((F (x) \in u \land F (y) \in v \land u \cap v = \emptyset) \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
65	64	rexlimdvva	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to (\exists u \in K \exists v \in K (F (x) \in u \land F (y) \in v \land u \cap v = \emptyset) \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
66	26 65	mpd	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land ((x \in ⋃ J \land y \in ⋃ J) \land x \neq y)) \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)$
67	66	expr	$⊢ ((K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (x \neq y \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
68	67	ralrimivva	$⊢ (K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to \forall x \in ⋃ J \forall y \in ⋃ J (x \neq y \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset))$
69	5	ishaus	$⊢ J \in Haus \leftrightarrow (J \in Top \land \forall x \in ⋃ J \forall y \in ⋃ J (x \neq y \to \exists m \in J \exists n \in J (x \in m \land y \in n \land m \cap n = \emptyset)))$
70	2 68 69	sylanbrc	$⊢ (K \in Haus \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to J \in Haus$

Metamath Proof Explorer

Theorem cnhaus

Proof