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

Metamath Proof Explorer

Theorem ondif2

Description: Two ways to say that A is an ordinal greater than one. (Contributed by Mario Carneiro, 21-May-2015)

Ref Expression
Assertion ondif2 ( 𝐴 ∈ ( On ∖ 2o ) ↔ ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eldif ⊢ ( 𝐴 ∈ ( On ∖ 2o ) ↔ ( 𝐴 ∈ On ∧ ¬ 𝐴 ∈ 2o ) )
2 1on ⊢ 1o ∈ On
3 ontri1 ⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ On ) → ( 𝐴 ⊆ 1o ↔ ¬ 1o ∈ 𝐴 ) )
4 onsssuc ⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ On ) → ( 𝐴 ⊆ 1o ↔ 𝐴 ∈ suc 1o ) )
5 df-2o ⊢ 2o = suc 1o
6 5 eleq2i ⊢ ( 𝐴 ∈ 2o ↔ 𝐴 ∈ suc 1o )
7 4 6 bitr4di ⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ On ) → ( 𝐴 ⊆ 1o ↔ 𝐴 ∈ 2o ) )
8 3 7 bitr3d ⊢ ( ( 𝐴 ∈ On ∧ 1o ∈ On ) → ( ¬ 1o ∈ 𝐴 ↔ 𝐴 ∈ 2o ) )
9 2 8 mpan2 ⊢ ( 𝐴 ∈ On → ( ¬ 1o ∈ 𝐴 ↔ 𝐴 ∈ 2o ) )
10 9 con1bid ⊢ ( 𝐴 ∈ On → ( ¬ 𝐴 ∈ 2o ↔ 1o ∈ 𝐴 ) )
11 10 pm5.32i ⊢ ( ( 𝐴 ∈ On ∧ ¬ 𝐴 ∈ 2o ) ↔ ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )
12 1 11 bitri ⊢ ( 𝐴 ∈ ( On ∖ 2o ) ↔ ( 𝐴 ∈ On ∧ 1o ∈ 𝐴 ) )