Theorem ssonprc

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

	Ref	Expression
Assertion	ssonprc	⊢ ( 𝐴 ⊆ On → ( 𝐴 ∉ V ↔ ∪ 𝐴 = On ) )

Proof

Step	Hyp	Ref	Expression
1		df-nel	⊢ ( 𝐴 ∉ V ↔ ¬ 𝐴 ∈ V )
2		ssorduni	⊢ ( 𝐴 ⊆ On → Ord ∪ 𝐴 )
3		ordeleqon	⊢ ( Ord ∪ 𝐴 ↔ ( ∪ 𝐴 ∈ On ∨ ∪ 𝐴 = On ) )
4	2 3	sylib	⊢ ( 𝐴 ⊆ On → ( ∪ 𝐴 ∈ On ∨ ∪ 𝐴 = On ) )
5	4	orcomd	⊢ ( 𝐴 ⊆ On → ( ∪ 𝐴 = On ∨ ∪ 𝐴 ∈ On ) )
6	5	ord	⊢ ( 𝐴 ⊆ On → ( ¬ ∪ 𝐴 = On → ∪ 𝐴 ∈ On ) )
7		uniexr	⊢ ( ∪ 𝐴 ∈ On → 𝐴 ∈ V )
8	6 7	syl6	⊢ ( 𝐴 ⊆ On → ( ¬ ∪ 𝐴 = On → 𝐴 ∈ V ) )
9	8	con1d	⊢ ( 𝐴 ⊆ On → ( ¬ 𝐴 ∈ V → ∪ 𝐴 = On ) )
10		onprc	⊢ ¬ On ∈ V
11		uniexg	⊢ ( 𝐴 ∈ V → ∪ 𝐴 ∈ V )
12		eleq1	⊢ ( ∪ 𝐴 = On → ( ∪ 𝐴 ∈ V ↔ On ∈ V ) )
13	11 12	imbitrid	⊢ ( ∪ 𝐴 = On → ( 𝐴 ∈ V → On ∈ V ) )
14	10 13	mtoi	⊢ ( ∪ 𝐴 = On → ¬ 𝐴 ∈ V )
15	9 14	impbid1	⊢ ( 𝐴 ⊆ On → ( ¬ 𝐴 ∈ V ↔ ∪ 𝐴 = On ) )
16	1 15	bitrid	⊢ ( 𝐴 ⊆ On → ( 𝐴 ∉ V ↔ ∪ 𝐴 = On ) )