This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssonprc

Description: Two ways of saying a class of ordinals is unbounded. (Contributed by Mario Carneiro, 8-Jun-2013)

Ref Expression
Assertion ssonprc 
|- ( A C_ On -> ( A e/ _V <-> U. A = On ) )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( A e/ _V <-> -. A e. _V )
2 ssorduni 
 |-  ( A C_ On -> Ord U. A )
3 ordeleqon 
 |-  ( Ord U. A <-> ( U. A e. On \/ U. A = On ) )
4 2 3 sylib 
 |-  ( A C_ On -> ( U. A e. On \/ U. A = On ) )
5 4 orcomd 
 |-  ( A C_ On -> ( U. A = On \/ U. A e. On ) )
6 5 ord 
 |-  ( A C_ On -> ( -. U. A = On -> U. A e. On ) )
7 uniexr 
 |-  ( U. A e. On -> A e. _V )
8 6 7 syl6 
 |-  ( A C_ On -> ( -. U. A = On -> A e. _V ) )
9 8 con1d 
 |-  ( A C_ On -> ( -. A e. _V -> U. A = On ) )
10 onprc 
 |-  -. On e. _V
11 uniexg 
 |-  ( A e. _V -> U. A e. _V )
12 eleq1 
 |-  ( U. A = On -> ( U. A e. _V <-> On e. _V ) )
13 11 12 imbitrid 
 |-  ( U. A = On -> ( A e. _V -> On e. _V ) )
14 10 13 mtoi 
 |-  ( U. A = On -> -. A e. _V )
15 9 14 impbid1 
 |-  ( A C_ On -> ( -. A e. _V <-> U. A = On ) )
16 1 15 bitrid 
 |-  ( A C_ On -> ( A e/ _V <-> U. A = On ) )