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 ( 𝐴 ⊆ 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 ) )