cnt1

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

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

Proof

Step	Hyp	Ref	Expression
1		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
2	1	3ad2ant3	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to J \in Top$
3		eqid	$⊢ ⋃ J = ⋃ J$
4		eqid	$⊢ ⋃ K = ⋃ K$
5	3 4	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
6	5	3ad2ant3	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to F : ⋃ J ⟶ ⋃ K$
7	6	ffnd	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to F Fn ⋃ J$
8		fnsnfv	$⊢ (F Fn ⋃ J \land x \in ⋃ J) \to \{F (x)\} = F [\{x\}]$
9	7 8	sylan	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to \{F (x)\} = F [\{x\}]$
10	9	imaeq2d	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to F^{-1} [\{F (x)\}] = F^{-1} [F [\{x\}]]$
11		simpl2	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to F : X \underset{1-1}{⟶} Y$
12	6	fdmd	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to dom F = ⋃ J$
13		f1dm	$⊢ F : X \underset{1-1}{⟶} Y \to dom F = X$
14	13	3ad2ant2	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to dom F = X$
15	12 14	eqtr3d	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to ⋃ J = X$
16	15	eleq2d	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to (x \in ⋃ J \leftrightarrow x \in X)$
17	16	biimpa	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to x \in X$
18	17	snssd	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to \{x\} \subseteq X$
19		f1imacnv	$⊢ (F : X \underset{1-1}{⟶} Y \land \{x\} \subseteq X) \to F^{-1} [F [\{x\}]] = \{x\}$
20	11 18 19	syl2anc	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to F^{-1} [F [\{x\}]] = \{x\}$
21	10 20	eqtrd	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to F^{-1} [\{F (x)\}] = \{x\}$
22		simpl3	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to F \in (J Cn K)$
23		simpl1	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to K \in Fre$
24	6	ffvelcdmda	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to F (x) \in ⋃ K$
25	4	t1sncld	$⊢ (K \in Fre \land F (x) \in ⋃ K) \to \{F (x)\} \in Clsd (K)$
26	23 24 25	syl2anc	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to \{F (x)\} \in Clsd (K)$
27		cnclima	$⊢ (F \in (J Cn K) \land \{F (x)\} \in Clsd (K)) \to F^{-1} [\{F (x)\}] \in Clsd (J)$
28	22 26 27	syl2anc	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to F^{-1} [\{F (x)\}] \in Clsd (J)$
29	21 28	eqeltrrd	$⊢ ((K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land x \in ⋃ J) \to \{x\} \in Clsd (J)$
30	29	ralrimiva	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to \forall x \in ⋃ J \{x\} \in Clsd (J)$
31	3	ist1	$⊢ J \in Fre \leftrightarrow (J \in Top \land \forall x \in ⋃ J \{x\} \in Clsd (J))$
32	2 30 31	sylanbrc	$⊢ (K \in Fre \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to J \in Fre$

Metamath Proof Explorer

Theorem cnt1

Proof