kgenidm

Description: The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Assertion	kgenidm	$⊢ J \in ran 𝑘Gen \to 𝑘Gen (J) = J$

Proof

Step	Hyp	Ref	Expression
1		kgenf	$⊢ 𝑘Gen : Top ⟶ Top$
2		ffn	$⊢ 𝑘Gen : Top ⟶ Top \to 𝑘Gen Fn Top$
3		fvelrnb	$⊢ 𝑘Gen Fn Top \to (J \in ran 𝑘Gen \leftrightarrow \exists j \in Top 𝑘Gen (j) = J)$
4	1 2 3	mp2b	$⊢ J \in ran 𝑘Gen \leftrightarrow \exists j \in Top 𝑘Gen (j) = J$
5		toptopon2	$⊢ j \in Top \leftrightarrow j \in TopOn (⋃ j)$
6		kgentopon	$⊢ j \in TopOn (⋃ j) \to 𝑘Gen (j) \in TopOn (⋃ j)$
7	5 6	sylbi	$⊢ j \in Top \to 𝑘Gen (j) \in TopOn (⋃ j)$
8		kgentopon	$⊢ 𝑘Gen (j) \in TopOn (⋃ j) \to 𝑘Gen (𝑘Gen (j)) \in TopOn (⋃ j)$
9	7 8	syl	$⊢ j \in Top \to 𝑘Gen (𝑘Gen (j)) \in TopOn (⋃ j)$
10		toponss	$⊢ (𝑘Gen (𝑘Gen (j)) \in TopOn (⋃ j) \land x \in 𝑘Gen (𝑘Gen (j))) \to x \subseteq ⋃ j$
11	9 10	sylan	$⊢ (j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \to x \subseteq ⋃ j$
12		simplr	$⊢ ((j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \land (k \in 𝒫 ⋃ j \land j ↾_{𝑡} k \in Comp)) \to x \in 𝑘Gen (𝑘Gen (j))$
13		kgencmp2	$⊢ j \in Top \to (j ↾_{𝑡} k \in Comp \leftrightarrow 𝑘Gen (j) ↾_{𝑡} k \in Comp)$
14	13	biimpa	$⊢ (j \in Top \land j ↾_{𝑡} k \in Comp) \to 𝑘Gen (j) ↾_{𝑡} k \in Comp$
15	14	ad2ant2rl	$⊢ ((j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \land (k \in 𝒫 ⋃ j \land j ↾_{𝑡} k \in Comp)) \to 𝑘Gen (j) ↾_{𝑡} k \in Comp$
16		kgeni	$⊢ (x \in 𝑘Gen (𝑘Gen (j)) \land 𝑘Gen (j) ↾_{𝑡} k \in Comp) \to x \cap k \in (𝑘Gen (j) ↾_{𝑡} k)$
17	12 15 16	syl2anc	$⊢ ((j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \land (k \in 𝒫 ⋃ j \land j ↾_{𝑡} k \in Comp)) \to x \cap k \in (𝑘Gen (j) ↾_{𝑡} k)$
18		kgencmp	$⊢ (j \in Top \land j ↾_{𝑡} k \in Comp) \to j ↾_{𝑡} k = 𝑘Gen (j) ↾_{𝑡} k$
19	18	ad2ant2rl	$⊢ ((j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \land (k \in 𝒫 ⋃ j \land j ↾_{𝑡} k \in Comp)) \to j ↾_{𝑡} k = 𝑘Gen (j) ↾_{𝑡} k$
20	17 19	eleqtrrd	$⊢ ((j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \land (k \in 𝒫 ⋃ j \land j ↾_{𝑡} k \in Comp)) \to x \cap k \in (j ↾_{𝑡} k)$
21	20	expr	$⊢ ((j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \land k \in 𝒫 ⋃ j) \to (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))$
22	21	ralrimiva	$⊢ (j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \to \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))$
23		simpl	$⊢ (j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \to j \in Top$
24	23 5	sylib	$⊢ (j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \to j \in TopOn (⋃ j)$
25		elkgen	$⊢ j \in TopOn (⋃ j) \to (x \in 𝑘Gen (j) \leftrightarrow (x \subseteq ⋃ j \land \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))))$
26	24 25	syl	$⊢ (j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \to (x \in 𝑘Gen (j) \leftrightarrow (x \subseteq ⋃ j \land \forall k \in 𝒫 ⋃ j (j ↾_{𝑡} k \in Comp \to x \cap k \in (j ↾_{𝑡} k))))$
27	11 22 26	mpbir2and	$⊢ (j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \to x \in 𝑘Gen (j)$
28	27	ex	$⊢ j \in Top \to (x \in 𝑘Gen (𝑘Gen (j)) \to x \in 𝑘Gen (j))$
29	28	ssrdv	$⊢ j \in Top \to 𝑘Gen (𝑘Gen (j)) \subseteq 𝑘Gen (j)$
30		fveq2	$⊢ 𝑘Gen (j) = J \to 𝑘Gen (𝑘Gen (j)) = 𝑘Gen (J)$
31		id	$⊢ 𝑘Gen (j) = J \to 𝑘Gen (j) = J$
32	30 31	sseq12d	$⊢ 𝑘Gen (j) = J \to (𝑘Gen (𝑘Gen (j)) \subseteq 𝑘Gen (j) \leftrightarrow 𝑘Gen (J) \subseteq J)$
33	29 32	syl5ibcom	$⊢ j \in Top \to (𝑘Gen (j) = J \to 𝑘Gen (J) \subseteq J)$
34	33	rexlimiv	$⊢ \exists j \in Top 𝑘Gen (j) = J \to 𝑘Gen (J) \subseteq J$
35	4 34	sylbi	$⊢ J \in ran 𝑘Gen \to 𝑘Gen (J) \subseteq J$
36		kgentop	$⊢ J \in ran 𝑘Gen \to J \in Top$
37		kgenss	$⊢ J \in Top \to J \subseteq 𝑘Gen (J)$
38	36 37	syl	$⊢ J \in ran 𝑘Gen \to J \subseteq 𝑘Gen (J)$
39	35 38	eqssd	$⊢ J \in ran 𝑘Gen \to 𝑘Gen (J) = J$

Metamath Proof Explorer

Theorem kgenidm

Proof