Step |
Hyp |
Ref |
Expression |
1 |
|
ordsuci |
⊢ ( Ord 𝐴 → Ord suc 𝐴 ) |
2 |
|
sucidg |
⊢ ( 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 ) |
3 |
|
ordelord |
⊢ ( ( Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴 ) → Ord 𝐴 ) |
4 |
3
|
ex |
⊢ ( Ord suc 𝐴 → ( 𝐴 ∈ suc 𝐴 → Ord 𝐴 ) ) |
5 |
2 4
|
syl5com |
⊢ ( 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) ) |
6 |
|
sucprc |
⊢ ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 ) |
7 |
6
|
eqcomd |
⊢ ( ¬ 𝐴 ∈ V → 𝐴 = suc 𝐴 ) |
8 |
|
ordeq |
⊢ ( 𝐴 = suc 𝐴 → ( Ord 𝐴 ↔ Ord suc 𝐴 ) ) |
9 |
7 8
|
syl |
⊢ ( ¬ 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) ) |
10 |
9
|
biimprd |
⊢ ( ¬ 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) ) |
11 |
5 10
|
pm2.61i |
⊢ ( Ord suc 𝐴 → Ord 𝐴 ) |
12 |
1 11
|
impbii |
⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 ) |