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 ⊢ A ∈ On ∖ 2 𝑜 ↔ A ∈ On ∧ 1 𝑜 ∈ A

Proof

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