Step |
Hyp |
Ref |
Expression |
1 |
|
isfi |
⊢ ( 𝐴 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) |
2 |
1
|
biimpi |
⊢ ( 𝐴 ∈ Fin → ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 ) |
3 |
|
finnum |
⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card ) |
4 |
|
cardid2 |
⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 ) |
5 |
3 4
|
syl |
⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ≈ 𝐴 ) |
6 |
|
entr |
⊢ ( ( ( card ‘ 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≈ 𝑥 ) → ( card ‘ 𝐴 ) ≈ 𝑥 ) |
7 |
5 6
|
sylan |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝑥 ) → ( card ‘ 𝐴 ) ≈ 𝑥 ) |
8 |
|
cardon |
⊢ ( card ‘ 𝐴 ) ∈ On |
9 |
|
onomeneq |
⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ 𝑥 ∈ ω ) → ( ( card ‘ 𝐴 ) ≈ 𝑥 ↔ ( card ‘ 𝐴 ) = 𝑥 ) ) |
10 |
8 9
|
mpan |
⊢ ( 𝑥 ∈ ω → ( ( card ‘ 𝐴 ) ≈ 𝑥 ↔ ( card ‘ 𝐴 ) = 𝑥 ) ) |
11 |
7 10
|
syl5ib |
⊢ ( 𝑥 ∈ ω → ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝑥 ) → ( card ‘ 𝐴 ) = 𝑥 ) ) |
12 |
|
eleq1a |
⊢ ( 𝑥 ∈ ω → ( ( card ‘ 𝐴 ) = 𝑥 → ( card ‘ 𝐴 ) ∈ ω ) ) |
13 |
11 12
|
syld |
⊢ ( 𝑥 ∈ ω → ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝑥 ) → ( card ‘ 𝐴 ) ∈ ω ) ) |
14 |
13
|
expcomd |
⊢ ( 𝑥 ∈ ω → ( 𝐴 ≈ 𝑥 → ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω ) ) ) |
15 |
14
|
rexlimiv |
⊢ ( ∃ 𝑥 ∈ ω 𝐴 ≈ 𝑥 → ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω ) ) |
16 |
2 15
|
mpcom |
⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω ) |