Metamath Proof Explorer
Description: An ordinal number is a proper subset of its successor. (Contributed by Stefan O'Rear, 18-Nov-2014)
|
|
Ref |
Expression |
|
Assertion |
onpsssuc |
⊢ ( 𝐴 ∈ On → 𝐴 ⊊ suc 𝐴 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
sucidg |
⊢ ( 𝐴 ∈ On → 𝐴 ∈ suc 𝐴 ) |
2 |
|
eloni |
⊢ ( 𝐴 ∈ On → Ord 𝐴 ) |
3 |
|
ordsuc |
⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 ) |
4 |
2 3
|
sylib |
⊢ ( 𝐴 ∈ On → Ord suc 𝐴 ) |
5 |
|
ordelpss |
⊢ ( ( Ord 𝐴 ∧ Ord suc 𝐴 ) → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ⊊ suc 𝐴 ) ) |
6 |
2 4 5
|
syl2anc |
⊢ ( 𝐴 ∈ On → ( 𝐴 ∈ suc 𝐴 ↔ 𝐴 ⊊ suc 𝐴 ) ) |
7 |
1 6
|
mpbid |
⊢ ( 𝐴 ∈ On → 𝐴 ⊊ suc 𝐴 ) |