kgen2ss

Description: The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015)

		Ref	Expression
	Assertion	kgen2ss	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to 𝑘Gen (J) \subseteq 𝑘Gen (K)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to J \in TopOn (X)$
2		elpwi	$⊢ k \in 𝒫 X \to k \subseteq X$
3		resttopon	$⊢ (J \in TopOn (X) \land k \subseteq X) \to J ↾_{𝑡} k \in TopOn (k)$
4	1 2 3	syl2an	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to J ↾_{𝑡} k \in TopOn (k)$
5		simp2	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to K \in TopOn (X)$
6		resttopon	$⊢ (K \in TopOn (X) \land k \subseteq X) \to K ↾_{𝑡} k \in TopOn (k)$
7	5 2 6	syl2an	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to K ↾_{𝑡} k \in TopOn (k)$
8		toponuni	$⊢ K ↾_{𝑡} k \in TopOn (k) \to k = ⋃ (K ↾_{𝑡} k)$
9	7 8	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to k = ⋃ (K ↾_{𝑡} k)$
10	9	fveq2d	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to TopOn (k) = TopOn (⋃ (K ↾_{𝑡} k))$
11	4 10	eleqtrd	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to J ↾_{𝑡} k \in TopOn (⋃ (K ↾_{𝑡} k))$
12		simpl2	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to K \in TopOn (X)$
13		topontop	$⊢ K \in TopOn (X) \to K \in Top$
14	12 13	syl	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to K \in Top$
15		simpl3	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to J \subseteq K$
16		ssrest	$⊢ (K \in Top \land J \subseteq K) \to J ↾_{𝑡} k \subseteq K ↾_{𝑡} k$
17	14 15 16	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to J ↾_{𝑡} k \subseteq K ↾_{𝑡} k$
18		eqid	$⊢ ⋃ (K ↾_{𝑡} k) = ⋃ (K ↾_{𝑡} k)$
19	18	sscmp	$⊢ (J ↾_{𝑡} k \in TopOn (⋃ (K ↾_{𝑡} k)) \land K ↾_{𝑡} k \in Comp \land J ↾_{𝑡} k \subseteq K ↾_{𝑡} k) \to J ↾_{𝑡} k \in Comp$
20	19	3com23	$⊢ (J ↾_{𝑡} k \in TopOn (⋃ (K ↾_{𝑡} k)) \land J ↾_{𝑡} k \subseteq K ↾_{𝑡} k \land K ↾_{𝑡} k \in Comp) \to J ↾_{𝑡} k \in Comp$
21	20	3expia	$⊢ (J ↾_{𝑡} k \in TopOn (⋃ (K ↾_{𝑡} k)) \land J ↾_{𝑡} k \subseteq K ↾_{𝑡} k) \to (K ↾_{𝑡} k \in Comp \to J ↾_{𝑡} k \in Comp)$
22	11 17 21	syl2anc	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to (K ↾_{𝑡} k \in Comp \to J ↾_{𝑡} k \in Comp)$
23	17	sseld	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to (x \cap k \in (J ↾_{𝑡} k) \to x \cap k \in (K ↾_{𝑡} k))$
24	22 23	imim12d	$⊢ ((J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \land k \in 𝒫 X) \to ((J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to (K ↾_{𝑡} k \in Comp \to x \cap k \in (K ↾_{𝑡} k)))$
25	24	ralimdva	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to \forall k \in 𝒫 X (K ↾_{𝑡} k \in Comp \to x \cap k \in (K ↾_{𝑡} k)))$
26	25	anim2d	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to ((x \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))) \to (x \subseteq X \land \forall k \in 𝒫 X (K ↾_{𝑡} k \in Comp \to x \cap k \in (K ↾_{𝑡} k))))$
27		elkgen	$⊢ J \in TopOn (X) \to (x \in 𝑘Gen (J) \leftrightarrow (x \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))))$
28	27	3ad2ant1	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to (x \in 𝑘Gen (J) \leftrightarrow (x \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))))$
29		elkgen	$⊢ K \in TopOn (X) \to (x \in 𝑘Gen (K) \leftrightarrow (x \subseteq X \land \forall k \in 𝒫 X (K ↾_{𝑡} k \in Comp \to x \cap k \in (K ↾_{𝑡} k))))$
30	29	3ad2ant2	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to (x \in 𝑘Gen (K) \leftrightarrow (x \subseteq X \land \forall k \in 𝒫 X (K ↾_{𝑡} k \in Comp \to x \cap k \in (K ↾_{𝑡} k))))$
31	26 28 30	3imtr4d	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to (x \in 𝑘Gen (J) \to x \in 𝑘Gen (K))$
32	31	ssrdv	$⊢ (J \in TopOn (X) \land K \in TopOn (X) \land J \subseteq K) \to 𝑘Gen (J) \subseteq 𝑘Gen (K)$

Metamath Proof Explorer

Theorem kgen2ss

Proof