kgeni

Description: Property of the open sets in the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Assertion	kgeni	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to A \cap K \in (J ↾_{𝑡} K)$

Proof

Step	Hyp	Ref	Expression
1		inass	$⊢ (A \cap K) \cap ⋃ J = A \cap (K \cap ⋃ J)$
2		in32	$⊢ (A \cap K) \cap ⋃ J = (A \cap ⋃ J) \cap K$
3	1 2	eqtr3i	$⊢ A \cap (K \cap ⋃ J) = (A \cap ⋃ J) \cap K$
4		df-kgen	$⊢ 𝑘Gen = (j \in Top ⟼ \{x \in 𝒫 ⋃ j \| \forall y \in 𝒫 ⋃ j (j ↾_{𝑡} y \in Comp \to x \cap y \in (j ↾_{𝑡} y))\})$
5	4	mptrcl	$⊢ A \in 𝑘Gen (J) \to J \in Top$
6	5	adantr	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to J \in Top$
7		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
8	6 7	sylib	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to J \in TopOn (⋃ J)$
9		simpl	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to A \in 𝑘Gen (J)$
10		elkgen	$⊢ J \in TopOn (⋃ J) \to (A \in 𝑘Gen (J) \leftrightarrow (A \subseteq ⋃ J \land \forall y \in 𝒫 ⋃ J (J ↾_{𝑡} y \in Comp \to A \cap y \in (J ↾_{𝑡} y))))$
11	10	biimpa	$⊢ (J \in TopOn (⋃ J) \land A \in 𝑘Gen (J)) \to (A \subseteq ⋃ J \land \forall y \in 𝒫 ⋃ J (J ↾_{𝑡} y \in Comp \to A \cap y \in (J ↾_{𝑡} y)))$
12	8 9 11	syl2anc	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to (A \subseteq ⋃ J \land \forall y \in 𝒫 ⋃ J (J ↾_{𝑡} y \in Comp \to A \cap y \in (J ↾_{𝑡} y)))$
13	12	simpld	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to A \subseteq ⋃ J$
14		df-ss	$⊢ A \subseteq ⋃ J \leftrightarrow A \cap ⋃ J = A$
15	13 14	sylib	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to A \cap ⋃ J = A$
16	15	ineq1d	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to (A \cap ⋃ J) \cap K = A \cap K$
17	3 16	syl5eq	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to A \cap (K \cap ⋃ J) = A \cap K$
18		cmptop	$⊢ J ↾_{𝑡} K \in Comp \to J ↾_{𝑡} K \in Top$
19	18	adantl	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \in Top$
20		restrcl	$⊢ J ↾_{𝑡} K \in Top \to (J \in V \land K \in V)$
21	20	simprd	$⊢ J ↾_{𝑡} K \in Top \to K \in V$
22	19 21	syl	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to K \in V$
23		eqid	$⊢ ⋃ J = ⋃ J$
24	23	restin	$⊢ (J \in Top \land K \in V) \to J ↾_{𝑡} K = J ↾_{𝑡} (K \cap ⋃ J)$
25	6 22 24	syl2anc	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K = J ↾_{𝑡} (K \cap ⋃ J)$
26		simpr	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} K \in Comp$
27	25 26	eqeltrrd	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to J ↾_{𝑡} (K \cap ⋃ J) \in Comp$
28		oveq2	$⊢ y = K \cap ⋃ J \to J ↾_{𝑡} y = J ↾_{𝑡} (K \cap ⋃ J)$
29	28	eleq1d	$⊢ y = K \cap ⋃ J \to (J ↾_{𝑡} y \in Comp \leftrightarrow J ↾_{𝑡} (K \cap ⋃ J) \in Comp)$
30		ineq2	$⊢ y = K \cap ⋃ J \to A \cap y = A \cap (K \cap ⋃ J)$
31	30 28	eleq12d	$⊢ y = K \cap ⋃ J \to (A \cap y \in (J ↾_{𝑡} y) \leftrightarrow A \cap (K \cap ⋃ J) \in (J ↾_{𝑡} (K \cap ⋃ J)))$
32	29 31	imbi12d	$⊢ y = K \cap ⋃ J \to ((J ↾_{𝑡} y \in Comp \to A \cap y \in (J ↾_{𝑡} y)) \leftrightarrow (J ↾_{𝑡} (K \cap ⋃ J) \in Comp \to A \cap (K \cap ⋃ J) \in (J ↾_{𝑡} (K \cap ⋃ J))))$
33	12	simprd	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to \forall y \in 𝒫 ⋃ J (J ↾_{𝑡} y \in Comp \to A \cap y \in (J ↾_{𝑡} y))$
34		inss2	$⊢ K \cap ⋃ J \subseteq ⋃ J$
35		inex1g	$⊢ K \in V \to K \cap ⋃ J \in V$
36		elpwg	$⊢ K \cap ⋃ J \in V \to (K \cap ⋃ J \in 𝒫 ⋃ J \leftrightarrow K \cap ⋃ J \subseteq ⋃ J)$
37	22 35 36	3syl	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to (K \cap ⋃ J \in 𝒫 ⋃ J \leftrightarrow K \cap ⋃ J \subseteq ⋃ J)$
38	34 37	mpbiri	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to K \cap ⋃ J \in 𝒫 ⋃ J$
39	32 33 38	rspcdva	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to (J ↾_{𝑡} (K \cap ⋃ J) \in Comp \to A \cap (K \cap ⋃ J) \in (J ↾_{𝑡} (K \cap ⋃ J)))$
40	27 39	mpd	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to A \cap (K \cap ⋃ J) \in (J ↾_{𝑡} (K \cap ⋃ J))$
41	17 40	eqeltrrd	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to A \cap K \in (J ↾_{𝑡} (K \cap ⋃ J))$
42	41 25	eleqtrrd	$⊢ (A \in 𝑘Gen (J) \land J ↾_{𝑡} K \in Comp) \to A \cap K \in (J ↾_{𝑡} K)$

Metamath Proof Explorer

Theorem kgeni

Proof