Metamath Proof Explorer

Theorem ontgval

Description: The topology generated from an ordinal number B is suc U. B . (Contributed by Chen-Pang He, 10-Oct-2015)

Ref Expression
Assertion ontgval ⊢ B ∈ On → topGen ⁡ B = suc ⁡ ⋃ B

Proof

Step Hyp Ref Expression
1 eltg4i ⊢ x ∈ topGen ⁡ B → x = ⋃ B ∩ 𝒫 x
2 inex1g ⊢ B ∈ On → B ∩ 𝒫 x ∈ V
3 onss ⊢ B ∈ On → B ⊆ On
4 ssinss1 ⊢ B ⊆ On → B ∩ 𝒫 x ⊆ On
5 3 4 syl ⊢ B ∈ On → B ∩ 𝒫 x ⊆ On
6 ssonuni ⊢ B ∩ 𝒫 x ∈ V → B ∩ 𝒫 x ⊆ On → ⋃ B ∩ 𝒫 x ∈ On
7 2 5 6 sylc ⊢ B ∈ On → ⋃ B ∩ 𝒫 x ∈ On
8 eleq1 ⊢ x = ⋃ B ∩ 𝒫 x → x ∈ On ↔ ⋃ B ∩ 𝒫 x ∈ On
9 8 biimprd ⊢ x = ⋃ B ∩ 𝒫 x → ⋃ B ∩ 𝒫 x ∈ On → x ∈ On
10 1 7 9 syl2imc ⊢ B ∈ On → x ∈ topGen ⁡ B → x ∈ On
11 onuni ⊢ B ∈ On → ⋃ B ∈ On
12 suceloni ⊢ ⋃ B ∈ On → suc ⁡ ⋃ B ∈ On
13 11 12 syl ⊢ B ∈ On → suc ⁡ ⋃ B ∈ On
14 10 13 jctird ⊢ B ∈ On → x ∈ topGen ⁡ B → x ∈ On ∧ suc ⁡ ⋃ B ∈ On
15 tg1 ⊢ x ∈ topGen ⁡ B → x ⊆ ⋃ B
16 15 a1i ⊢ B ∈ On → x ∈ topGen ⁡ B → x ⊆ ⋃ B
17 sucidg ⊢ ⋃ B ∈ On → ⋃ B ∈ suc ⁡ ⋃ B
18 11 17 syl ⊢ B ∈ On → ⋃ B ∈ suc ⁡ ⋃ B
19 16 18 jctird ⊢ B ∈ On → x ∈ topGen ⁡ B → x ⊆ ⋃ B ∧ ⋃ B ∈ suc ⁡ ⋃ B
20 ontr2 ⊢ x ∈ On ∧ suc ⁡ ⋃ B ∈ On → x ⊆ ⋃ B ∧ ⋃ B ∈ suc ⁡ ⋃ B → x ∈ suc ⁡ ⋃ B
21 14 19 20 syl6c ⊢ B ∈ On → x ∈ topGen ⁡ B → x ∈ suc ⁡ ⋃ B
22 elsuci ⊢ x ∈ suc ⁡ ⋃ B → x ∈ ⋃ B ∨ x = ⋃ B
23 eloni ⊢ B ∈ On → Ord ⁡ B
24 orduniss ⊢ Ord ⁡ B → ⋃ B ⊆ B
25 23 24 syl ⊢ B ∈ On → ⋃ B ⊆ B
26 bastg ⊢ B ∈ On → B ⊆ topGen ⁡ B
27 25 26 sstrd ⊢ B ∈ On → ⋃ B ⊆ topGen ⁡ B
28 27 sseld ⊢ B ∈ On → x ∈ ⋃ B → x ∈ topGen ⁡ B
29 ssid ⊢ B ⊆ B
30 eltg3i ⊢ B ∈ On ∧ B ⊆ B → ⋃ B ∈ topGen ⁡ B
31 29 30 mpan2 ⊢ B ∈ On → ⋃ B ∈ topGen ⁡ B
32 eleq1a ⊢ ⋃ B ∈ topGen ⁡ B → x = ⋃ B → x ∈ topGen ⁡ B
33 31 32 syl ⊢ B ∈ On → x = ⋃ B → x ∈ topGen ⁡ B
34 28 33 jaod ⊢ B ∈ On → x ∈ ⋃ B ∨ x = ⋃ B → x ∈ topGen ⁡ B
35 22 34 syl5 ⊢ B ∈ On → x ∈ suc ⁡ ⋃ B → x ∈ topGen ⁡ B
36 21 35 impbid ⊢ B ∈ On → x ∈ topGen ⁡ B ↔ x ∈ suc ⁡ ⋃ B
37 36 eqrdv ⊢ B ∈ On → topGen ⁡ B = suc ⁡ ⋃ B