Step |
Hyp |
Ref |
Expression |
1 |
|
nnon |
⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On ) |
2 |
|
onenon |
⊢ ( 𝐴 ∈ On → 𝐴 ∈ dom card ) |
3 |
|
harval2 |
⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
4 |
1 2 3
|
3syl |
⊢ ( 𝐴 ∈ ω → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } ) |
5 |
|
sucdom |
⊢ ( 𝐴 ∈ ω → ( 𝐴 ≺ 𝑥 ↔ suc 𝐴 ≼ 𝑥 ) ) |
6 |
5
|
adantr |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( 𝐴 ≺ 𝑥 ↔ suc 𝐴 ≼ 𝑥 ) ) |
7 |
|
peano2 |
⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω ) |
8 |
|
nndomog |
⊢ ( ( suc 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( suc 𝐴 ≼ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) ) |
9 |
7 8
|
sylan |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( suc 𝐴 ≼ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) ) |
10 |
6 9
|
bitrd |
⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( 𝐴 ≺ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) ) |
11 |
10
|
rabbidva |
⊢ ( 𝐴 ∈ ω → { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } ) |
12 |
11
|
inteqd |
⊢ ( 𝐴 ∈ ω → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } ) |
13 |
|
nnon |
⊢ ( suc 𝐴 ∈ ω → suc 𝐴 ∈ On ) |
14 |
|
intmin |
⊢ ( suc 𝐴 ∈ On → ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } = suc 𝐴 ) |
15 |
7 13 14
|
3syl |
⊢ ( 𝐴 ∈ ω → ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } = suc 𝐴 ) |
16 |
4 12 15
|
3eqtrd |
⊢ ( 𝐴 ∈ ω → ( har ‘ 𝐴 ) = suc 𝐴 ) |