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 syl5ib
 |-  ( 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 syl5bb
 |-  ( A C_ On -> ( A e/ _V <-> U. A = On ) )