cnt0

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

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

Proof

Step	Hyp	Ref	Expression
1		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
2	1	3ad2ant3	$⊢ (K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to J \in Top$
3		simpl3	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to F \in (J Cn K)$
4		cnima	$⊢ (F \in (J Cn K) \land w \in K) \to F^{-1} [w] \in J$
5	3 4	sylan	$⊢ (((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \land w \in K) \to F^{-1} [w] \in J$
6		eleq2	$⊢ z = F^{-1} [w] \to (x \in z \leftrightarrow x \in F^{-1} [w])$
7		eleq2	$⊢ z = F^{-1} [w] \to (y \in z \leftrightarrow y \in F^{-1} [w])$
8	6 7	bibi12d	$⊢ z = F^{-1} [w] \to ((x \in z \leftrightarrow y \in z) \leftrightarrow (x \in F^{-1} [w] \leftrightarrow y \in F^{-1} [w]))$
9	8	rspcv	$⊢ F^{-1} [w] \in J \to (\forall z \in J (x \in z \leftrightarrow y \in z) \to (x \in F^{-1} [w] \leftrightarrow y \in F^{-1} [w]))$
10	5 9	syl	$⊢ (((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \land w \in K) \to (\forall z \in J (x \in z \leftrightarrow y \in z) \to (x \in F^{-1} [w] \leftrightarrow y \in F^{-1} [w]))$
11		simprl	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to x \in ⋃ J$
12		eqid	$⊢ ⋃ J = ⋃ J$
13		eqid	$⊢ ⋃ K = ⋃ K$
14	12 13	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
15	3 14	syl	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to F : ⋃ J ⟶ ⋃ K$
16	15	ffnd	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to F Fn ⋃ J$
17		elpreima	$⊢ F Fn ⋃ J \to (x \in F^{-1} [w] \leftrightarrow (x \in ⋃ J \land F (x) \in w))$
18	16 17	syl	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (x \in F^{-1} [w] \leftrightarrow (x \in ⋃ J \land F (x) \in w))$
19	11 18	mpbirand	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (x \in F^{-1} [w] \leftrightarrow F (x) \in w)$
20		simprr	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to y \in ⋃ J$
21		elpreima	$⊢ F Fn ⋃ J \to (y \in F^{-1} [w] \leftrightarrow (y \in ⋃ J \land F (y) \in w))$
22	16 21	syl	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (y \in F^{-1} [w] \leftrightarrow (y \in ⋃ J \land F (y) \in w))$
23	20 22	mpbirand	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (y \in F^{-1} [w] \leftrightarrow F (y) \in w)$
24	19 23	bibi12d	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to ((x \in F^{-1} [w] \leftrightarrow y \in F^{-1} [w]) \leftrightarrow (F (x) \in w \leftrightarrow F (y) \in w))$
25	24	adantr	$⊢ (((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \land w \in K) \to ((x \in F^{-1} [w] \leftrightarrow y \in F^{-1} [w]) \leftrightarrow (F (x) \in w \leftrightarrow F (y) \in w))$
26	10 25	sylibd	$⊢ (((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \land w \in K) \to (\forall z \in J (x \in z \leftrightarrow y \in z) \to (F (x) \in w \leftrightarrow F (y) \in w))$
27	26	ralrimdva	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (\forall z \in J (x \in z \leftrightarrow y \in z) \to \forall w \in K (F (x) \in w \leftrightarrow F (y) \in w))$
28		simpl1	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to K \in Kol2$
29	15 11	ffvelcdmd	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to F (x) \in ⋃ K$
30	15 20	ffvelcdmd	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to F (y) \in ⋃ K$
31	13	t0sep	$⊢ (K \in Kol2 \land (F (x) \in ⋃ K \land F (y) \in ⋃ K)) \to (\forall w \in K (F (x) \in w \leftrightarrow F (y) \in w) \to F (x) = F (y))$
32	28 29 30 31	syl12anc	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (\forall w \in K (F (x) \in w \leftrightarrow F (y) \in w) \to F (x) = F (y))$
33	27 32	syld	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (\forall z \in J (x \in z \leftrightarrow y \in z) \to F (x) = F (y))$
34		simpl2	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to F : X \underset{1-1}{⟶} Y$
35	15	fdmd	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to dom F = ⋃ J$
36		f1dm	$⊢ F : X \underset{1-1}{⟶} Y \to dom F = X$
37	34 36	syl	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to dom F = X$
38	35 37	eqtr3d	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to ⋃ J = X$
39	11 38	eleqtrd	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to x \in X$
40	20 38	eleqtrd	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to y \in X$
41		f1fveq	$⊢ (F : X \underset{1-1}{⟶} Y \land (x \in X \land y \in X)) \to (F (x) = F (y) \leftrightarrow x = y)$
42	34 39 40 41	syl12anc	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (F (x) = F (y) \leftrightarrow x = y)$
43	33 42	sylibd	$⊢ ((K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \land (x \in ⋃ J \land y \in ⋃ J)) \to (\forall z \in J (x \in z \leftrightarrow y \in z) \to x = y)$
44	43	ralrimivva	$⊢ (K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to \forall x \in ⋃ J \forall y \in ⋃ J (\forall z \in J (x \in z \leftrightarrow y \in z) \to x = y)$
45	12	ist0	$⊢ J \in Kol2 \leftrightarrow (J \in Top \land \forall x \in ⋃ J \forall y \in ⋃ J (\forall z \in J (x \in z \leftrightarrow y \in z) \to x = y))$
46	2 44 45	sylanbrc	$⊢ (K \in Kol2 \land F : X \underset{1-1}{⟶} Y \land F \in (J Cn K)) \to J \in Kol2$

Metamath Proof Explorer

Theorem cnt0

Proof