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 ( 𝐵 ∈ On → ( topGen ‘ 𝐵 ) = suc ∪ 𝐵 )

Proof

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