Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
⊢ ( 𝐴 ∈ dom card → 𝐴 ∈ V ) |
2 |
|
isnum2 |
⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 ) |
3 |
|
rabn0 |
⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ≠ ∅ ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 ) |
4 |
|
intex |
⊢ ( { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ≠ ∅ ↔ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ∈ V ) |
5 |
2 3 4
|
3bitr2i |
⊢ ( 𝐴 ∈ dom card ↔ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ∈ V ) |
6 |
5
|
biimpi |
⊢ ( 𝐴 ∈ dom card → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ∈ V ) |
7 |
|
breq2 |
⊢ ( 𝑦 = 𝐴 → ( 𝑥 ≈ 𝑦 ↔ 𝑥 ≈ 𝐴 ) ) |
8 |
7
|
rabbidv |
⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ On ∣ 𝑥 ≈ 𝑦 } = { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ) |
9 |
8
|
inteqd |
⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝑦 } = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ) |
10 |
|
df-card |
⊢ card = ( 𝑦 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝑦 } ) |
11 |
9 10
|
fvmptg |
⊢ ( ( 𝐴 ∈ V ∧ ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ∈ V ) → ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ) |
12 |
1 6 11
|
syl2anc |
⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝑥 ≈ 𝐴 } ) |