cnntri

Description: Property of the preimage of an interior. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	cncls2i.1	$⊢ Y = ⋃ K$
	Assertion	cnntri	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to F^{-1} [int (K) (S)] \subseteq int (J) (F^{-1} [S])$

Step	Hyp	Ref	Expression
1		cncls2i.1	$⊢ Y = ⋃ K$
2		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
3	2	adantr	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to J \in Top$
4		cnvimass	$⊢ F^{-1} [S] \subseteq dom F$
5		eqid	$⊢ ⋃ J = ⋃ J$
6	5 1	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ Y$
7	6	fdmd	$⊢ F \in (J Cn K) \to dom F = ⋃ J$
8	7	adantr	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to dom F = ⋃ J$
9	4 8	sseqtrid	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to F^{-1} [S] \subseteq ⋃ J$
10		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
11	1	ntropn	$⊢ (K \in Top \land S \subseteq Y) \to int (K) (S) \in K$
12	10 11	sylan	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to int (K) (S) \in K$
13		cnima	$⊢ (F \in (J Cn K) \land int (K) (S) \in K) \to F^{-1} [int (K) (S)] \in J$
14	12 13	syldan	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to F^{-1} [int (K) (S)] \in J$
15	1	ntrss2	$⊢ (K \in Top \land S \subseteq Y) \to int (K) (S) \subseteq S$
16	10 15	sylan	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to int (K) (S) \subseteq S$
17		imass2	$⊢ int (K) (S) \subseteq S \to F^{-1} [int (K) (S)] \subseteq F^{-1} [S]$
18	16 17	syl	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to F^{-1} [int (K) (S)] \subseteq F^{-1} [S]$
19	5	ssntr	$⊢ ((J \in Top \land F^{-1} [S] \subseteq ⋃ J) \land (F^{-1} [int (K) (S)] \in J \land F^{-1} [int (K) (S)] \subseteq F^{-1} [S])) \to F^{-1} [int (K) (S)] \subseteq int (J) (F^{-1} [S])$
20	3 9 14 18 19	syl22anc	$⊢ (F \in (J Cn K) \land S \subseteq Y) \to F^{-1} [int (K) (S)] \subseteq int (J) (F^{-1} [S])$

Metamath Proof Explorer