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