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	5	birani	$⊢ (j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \to j \in TopOn (⋃ j)$
24		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))))$
25	23 24	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))))$
26	11 22 25	mpbir2and	$⊢ (j \in Top \land x \in 𝑘Gen (𝑘Gen (j))) \to x \in 𝑘Gen (j)$
27	26	ex	$⊢ j \in Top \to (x \in 𝑘Gen (𝑘Gen (j)) \to x \in 𝑘Gen (j))$
28	27	ssrdv	$⊢ j \in Top \to 𝑘Gen (𝑘Gen (j)) \subseteq 𝑘Gen (j)$
29		fveq2	$⊢ 𝑘Gen (j) = J \to 𝑘Gen (𝑘Gen (j)) = 𝑘Gen (J)$
30		id	$⊢ 𝑘Gen (j) = J \to 𝑘Gen (j) = J$
31	29 30	sseq12d	$⊢ 𝑘Gen (j) = J \to (𝑘Gen (𝑘Gen (j)) \subseteq 𝑘Gen (j) \leftrightarrow 𝑘Gen (J) \subseteq J)$
32	28 31	syl5ibcom	$⊢ j \in Top \to (𝑘Gen (j) = J \to 𝑘Gen (J) \subseteq J)$
33	32	rexlimiv	$⊢ \exists j \in Top 𝑘Gen (j) = J \to 𝑘Gen (J) \subseteq J$
34	4 33	sylbi	$⊢ J \in ran 𝑘Gen \to 𝑘Gen (J) \subseteq J$
35		kgentop	$⊢ J \in ran 𝑘Gen \to J \in Top$
36		kgenss	$⊢ J \in Top \to J \subseteq 𝑘Gen (J)$
37	35 36	syl	$⊢ J \in ran 𝑘Gen \to J \subseteq 𝑘Gen (J)$
38	34 37	eqssd	$⊢ J \in ran 𝑘Gen \to 𝑘Gen (J) = J$

Metamath Proof Explorer

Theorem kgenidm

Proof