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 ∈ 𝐴 ) )