Step |
Hyp |
Ref |
Expression |
1 |
|
elong |
⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ On ↔ Ord 𝐴 ) ) |
2 |
|
suceloni |
⊢ ( 𝐴 ∈ On → suc 𝐴 ∈ On ) |
3 |
|
eloni |
⊢ ( suc 𝐴 ∈ On → Ord suc 𝐴 ) |
4 |
2 3
|
syl |
⊢ ( 𝐴 ∈ On → Ord suc 𝐴 ) |
5 |
1 4
|
syl6bir |
⊢ ( 𝐴 ∈ V → ( Ord 𝐴 → Ord suc 𝐴 ) ) |
6 |
|
sucidg |
⊢ ( 𝐴 ∈ V → 𝐴 ∈ suc 𝐴 ) |
7 |
|
ordelord |
⊢ ( ( Ord suc 𝐴 ∧ 𝐴 ∈ suc 𝐴 ) → Ord 𝐴 ) |
8 |
7
|
ex |
⊢ ( Ord suc 𝐴 → ( 𝐴 ∈ suc 𝐴 → Ord 𝐴 ) ) |
9 |
6 8
|
syl5com |
⊢ ( 𝐴 ∈ V → ( Ord suc 𝐴 → Ord 𝐴 ) ) |
10 |
5 9
|
impbid |
⊢ ( 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) ) |
11 |
|
sucprc |
⊢ ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 ) |
12 |
11
|
eqcomd |
⊢ ( ¬ 𝐴 ∈ V → 𝐴 = suc 𝐴 ) |
13 |
|
ordeq |
⊢ ( 𝐴 = suc 𝐴 → ( Ord 𝐴 ↔ Ord suc 𝐴 ) ) |
14 |
12 13
|
syl |
⊢ ( ¬ 𝐴 ∈ V → ( Ord 𝐴 ↔ Ord suc 𝐴 ) ) |
15 |
10 14
|
pm2.61i |
⊢ ( Ord 𝐴 ↔ Ord suc 𝐴 ) |