topssnei

Description: A finer topology has more neighborhoods. (Contributed by Mario Carneiro, 9-Apr-2015)

	Ref	Expression
Hypotheses	tpnei.1	$⊢ X = ⋃ J$
	topssnei.2	$⊢ Y = ⋃ K$
Assertion	topssnei	$⊢ ((J \in Top \land K \in Top \land X = Y) \land J \subseteq K) \to nei (J) (S) \subseteq nei (K) (S)$

Proof

Step	Hyp	Ref	Expression
1		tpnei.1	$⊢ X = ⋃ J$
2		topssnei.2	$⊢ Y = ⋃ K$
3		simpl2	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to K \in Top$
4		simprl	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to J \subseteq K$
5		simpl1	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to J \in Top$
6		simprr	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to x \in nei (J) (S)$
7	1	neii1	$⊢ (J \in Top \land x \in nei (J) (S)) \to x \subseteq X$
8	5 6 7	syl2anc	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to x \subseteq X$
9	1	ntropn	$⊢ (J \in Top \land x \subseteq X) \to int (J) (x) \in J$
10	5 8 9	syl2anc	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to int (J) (x) \in J$
11	4 10	sseldd	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to int (J) (x) \in K$
12	1	neiss2	$⊢ (J \in Top \land x \in nei (J) (S)) \to S \subseteq X$
13	5 6 12	syl2anc	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to S \subseteq X$
14	1	neiint	$⊢ (J \in Top \land S \subseteq X \land x \subseteq X) \to (x \in nei (J) (S) \leftrightarrow S \subseteq int (J) (x))$
15	5 13 8 14	syl3anc	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to (x \in nei (J) (S) \leftrightarrow S \subseteq int (J) (x))$
16	6 15	mpbid	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to S \subseteq int (J) (x)$
17		opnneiss	$⊢ (K \in Top \land int (J) (x) \in K \land S \subseteq int (J) (x)) \to int (J) (x) \in nei (K) (S)$
18	3 11 16 17	syl3anc	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to int (J) (x) \in nei (K) (S)$
19	1	ntrss2	$⊢ (J \in Top \land x \subseteq X) \to int (J) (x) \subseteq x$
20	5 8 19	syl2anc	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to int (J) (x) \subseteq x$
21		simpl3	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to X = Y$
22	8 21	sseqtrd	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to x \subseteq Y$
23	2	ssnei2	$⊢ ((K \in Top \land int (J) (x) \in nei (K) (S)) \land (int (J) (x) \subseteq x \land x \subseteq Y)) \to x \in nei (K) (S)$
24	3 18 20 22 23	syl22anc	$⊢ ((J \in Top \land K \in Top \land X = Y) \land (J \subseteq K \land x \in nei (J) (S))) \to x \in nei (K) (S)$
25	24	expr	$⊢ ((J \in Top \land K \in Top \land X = Y) \land J \subseteq K) \to (x \in nei (J) (S) \to x \in nei (K) (S))$
26	25	ssrdv	$⊢ ((J \in Top \land K \in Top \land X = Y) \land J \subseteq K) \to nei (J) (S) \subseteq nei (K) (S)$

Metamath Proof Explorer

Theorem topssnei

Proof