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 e. On -> ( topGen ` B ) = suc U. B )

Proof

Step Hyp Ref Expression
1 eltg4i 
 |-  ( x e. ( topGen ` B ) -> x = U. ( B i^i ~P x ) )
2 inex1g 
 |-  ( B e. On -> ( B i^i ~P x ) e. _V )
3 onss 
 |-  ( B e. On -> B C_ On )
4 ssinss1 
 |-  ( B C_ On -> ( B i^i ~P x ) C_ On )
5 3 4 syl 
 |-  ( B e. On -> ( B i^i ~P x ) C_ On )
6 ssonuni 
 |-  ( ( B i^i ~P x ) e. _V -> ( ( B i^i ~P x ) C_ On -> U. ( B i^i ~P x ) e. On ) )
7 2 5 6 sylc 
 |-  ( B e. On -> U. ( B i^i ~P x ) e. On )
8 eleq1 
 |-  ( x = U. ( B i^i ~P x ) -> ( x e. On <-> U. ( B i^i ~P x ) e. On ) )
9 8 biimprd 
 |-  ( x = U. ( B i^i ~P x ) -> ( U. ( B i^i ~P x ) e. On -> x e. On ) )
10 1 7 9 syl2imc 
 |-  ( B e. On -> ( x e. ( topGen ` B ) -> x e. On ) )
11 onuni 
 |-  ( B e. On -> U. B e. On )
12 onsuc 
 |-  ( U. B e. On -> suc U. B e. On )
13 11 12 syl 
 |-  ( B e. On -> suc U. B e. On )
14 10 13 jctird 
 |-  ( B e. On -> ( x e. ( topGen ` B ) -> ( x e. On /\ suc U. B e. On ) ) )
15 tg1 
 |-  ( x e. ( topGen ` B ) -> x C_ U. B )
16 15 a1i 
 |-  ( B e. On -> ( x e. ( topGen ` B ) -> x C_ U. B ) )
17 sucidg 
 |-  ( U. B e. On -> U. B e. suc U. B )
18 11 17 syl 
 |-  ( B e. On -> U. B e. suc U. B )
19 16 18 jctird 
 |-  ( B e. On -> ( x e. ( topGen ` B ) -> ( x C_ U. B /\ U. B e. suc U. B ) ) )
20 ontr2 
 |-  ( ( x e. On /\ suc U. B e. On ) -> ( ( x C_ U. B /\ U. B e. suc U. B ) -> x e. suc U. B ) )
21 14 19 20 syl6c 
 |-  ( B e. On -> ( x e. ( topGen ` B ) -> x e. suc U. B ) )
22 elsuci 
 |-  ( x e. suc U. B -> ( x e. U. B \/ x = U. B ) )
23 eloni 
 |-  ( B e. On -> Ord B )
24 orduniss 
 |-  ( Ord B -> U. B C_ B )
25 23 24 syl 
 |-  ( B e. On -> U. B C_ B )
26 bastg 
 |-  ( B e. On -> B C_ ( topGen ` B ) )
27 25 26 sstrd 
 |-  ( B e. On -> U. B C_ ( topGen ` B ) )
28 27 sseld 
 |-  ( B e. On -> ( x e. U. B -> x e. ( topGen ` B ) ) )
29 ssid 
 |-  B C_ B
30 eltg3i 
 |-  ( ( B e. On /\ B C_ B ) -> U. B e. ( topGen ` B ) )
31 29 30 mpan2 
 |-  ( B e. On -> U. B e. ( topGen ` B ) )
32 eleq1a 
 |-  ( U. B e. ( topGen ` B ) -> ( x = U. B -> x e. ( topGen ` B ) ) )
33 31 32 syl 
 |-  ( B e. On -> ( x = U. B -> x e. ( topGen ` B ) ) )
34 28 33 jaod 
 |-  ( B e. On -> ( ( x e. U. B \/ x = U. B ) -> x e. ( topGen ` B ) ) )
35 22 34 syl5 
 |-  ( B e. On -> ( x e. suc U. B -> x e. ( topGen ` B ) ) )
36 21 35 impbid 
 |-  ( B e. On -> ( x e. ( topGen ` B ) <-> x e. suc U. B ) )
37 36 eqrdv 
 |-  ( B e. On -> ( topGen ` B ) = suc U. B )