Metamath Proof Explorer

Theorem tgidm

Description: The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006) (Revised by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion tgidm ( 𝐵 ∈ 𝑉 → ( topGen ‘ ( topGen ‘ 𝐵 ) ) = ( topGen ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( topGen ‘ 𝐵 ) ∈ V
2 eltg3 ⊢ ( ( topGen ‘ 𝐵 ) ∈ V → ( 𝑥 ∈ ( topGen ‘ ( topGen ‘ 𝐵 ) ) ↔ ∃ 𝑦 ( 𝑦 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑥 = ∪ 𝑦 ) ) )
3 1 2 ax-mp ⊢ ( 𝑥 ∈ ( topGen ‘ ( topGen ‘ 𝐵 ) ) ↔ ∃ 𝑦 ( 𝑦 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑥 = ∪ 𝑦 ) )
4 uniiun ⊢ ∪ 𝑦 = ∪ 𝑧 ∈ 𝑦 𝑧
5 simpr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) → 𝑦 ⊆ ( topGen ‘ 𝐵 ) )
6 5 sselda ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ∈ ( topGen ‘ 𝐵 ) )
7 eltg4i ⊢ ( 𝑧 ∈ ( topGen ‘ 𝐵 ) → 𝑧 = ∪ ( 𝐵 ∩ 𝒫 𝑧 ) )
8 6 7 syl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) ∧ 𝑧 ∈ 𝑦 ) → 𝑧 = ∪ ( 𝐵 ∩ 𝒫 𝑧 ) )
9 8 iuneq2dv ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝑧 ∈ 𝑦 𝑧 = ∪ 𝑧 ∈ 𝑦 ∪ ( 𝐵 ∩ 𝒫 𝑧 ) )
10 4 9 eqtrid ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝑦 = ∪ 𝑧 ∈ 𝑦 ∪ ( 𝐵 ∩ 𝒫 𝑧 ) )
11 iuncom4 ⊢ ∪ 𝑧 ∈ 𝑦 ∪ ( 𝐵 ∩ 𝒫 𝑧 ) = ∪ ∪ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 )
12 10 11 eqtrdi ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝑦 = ∪ ∪ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) )
13 inss1 ⊢ ( 𝐵 ∩ 𝒫 𝑧 ) ⊆ 𝐵
14 13 rgenw ⊢ ∀ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) ⊆ 𝐵
15 iunss ⊢ ( ∪ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) ⊆ 𝐵 ↔ ∀ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) ⊆ 𝐵 )
16 14 15 mpbir ⊢ ∪ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) ⊆ 𝐵
17 16 a1i ⊢ ( 𝑦 ⊆ ( topGen ‘ 𝐵 ) → ∪ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) ⊆ 𝐵 )
18 eltg3i ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ∪ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) ⊆ 𝐵 ) → ∪ ∪ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) ∈ ( topGen ‘ 𝐵 ) )
19 17 18 sylan2 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ ∪ 𝑧 ∈ 𝑦 ( 𝐵 ∩ 𝒫 𝑧 ) ∈ ( topGen ‘ 𝐵 ) )
20 12 19 eqeltrd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) → ∪ 𝑦 ∈ ( topGen ‘ 𝐵 ) )
21 eleq1 ⊢ ( 𝑥 = ∪ 𝑦 → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∪ 𝑦 ∈ ( topGen ‘ 𝐵 ) ) )
22 20 21 syl5ibrcom ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑦 ⊆ ( topGen ‘ 𝐵 ) ) → ( 𝑥 = ∪ 𝑦 → 𝑥 ∈ ( topGen ‘ 𝐵 ) ) )
23 22 expimpd ⊢ ( 𝐵 ∈ 𝑉 → ( ( 𝑦 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 ∈ ( topGen ‘ 𝐵 ) ) )
24 23 exlimdv ⊢ ( 𝐵 ∈ 𝑉 → ( ∃ 𝑦 ( 𝑦 ⊆ ( topGen ‘ 𝐵 ) ∧ 𝑥 = ∪ 𝑦 ) → 𝑥 ∈ ( topGen ‘ 𝐵 ) ) )
25 3 24 biimtrid ⊢ ( 𝐵 ∈ 𝑉 → ( 𝑥 ∈ ( topGen ‘ ( topGen ‘ 𝐵 ) ) → 𝑥 ∈ ( topGen ‘ 𝐵 ) ) )
26 25 ssrdv ⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ ( topGen ‘ 𝐵 ) ) ⊆ ( topGen ‘ 𝐵 ) )
27 bastg ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
28 tgss ⊢ ( ( ( topGen ‘ 𝐵 ) ∈ V ∧ 𝐵 ⊆ ( topGen ‘ 𝐵 ) ) → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ ( topGen ‘ 𝐵 ) ) )
29 1 27 28 sylancr ⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) ⊆ ( topGen ‘ ( topGen ‘ 𝐵 ) ) )
30 26 29 eqssd ⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ ( topGen ‘ 𝐵 ) ) = ( topGen ‘ 𝐵 ) )