Step |
Hyp |
Ref |
Expression |
1 |
|
hashfun |
⊢ ( 𝐹 ∈ Fin → ( Fun 𝐹 ↔ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) ) |
2 |
1
|
biimpd |
⊢ ( 𝐹 ∈ Fin → ( Fun 𝐹 → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) ) |
3 |
2
|
adantld |
⊢ ( 𝐹 ∈ Fin → ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) ) |
4 |
|
hashinf |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ 𝐹 ) = +∞ ) |
5 |
4
|
3adant2 |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ 𝐹 ) = +∞ ) |
6 |
|
fundmfibi |
⊢ ( Fun 𝐹 → ( 𝐹 ∈ Fin ↔ dom 𝐹 ∈ Fin ) ) |
7 |
6
|
notbid |
⊢ ( Fun 𝐹 → ( ¬ 𝐹 ∈ Fin ↔ ¬ dom 𝐹 ∈ Fin ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ¬ 𝐹 ∈ Fin ↔ ¬ dom 𝐹 ∈ Fin ) ) |
9 |
|
dmexg |
⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V ) |
10 |
|
hashinf |
⊢ ( ( dom 𝐹 ∈ V ∧ ¬ dom 𝐹 ∈ Fin ) → ( ♯ ‘ dom 𝐹 ) = +∞ ) |
11 |
9 10
|
sylan |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ ¬ dom 𝐹 ∈ Fin ) → ( ♯ ‘ dom 𝐹 ) = +∞ ) |
12 |
11
|
ex |
⊢ ( 𝐹 ∈ 𝑉 → ( ¬ dom 𝐹 ∈ Fin → ( ♯ ‘ dom 𝐹 ) = +∞ ) ) |
13 |
12
|
adantr |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ¬ dom 𝐹 ∈ Fin → ( ♯ ‘ dom 𝐹 ) = +∞ ) ) |
14 |
8 13
|
sylbid |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ¬ 𝐹 ∈ Fin → ( ♯ ‘ dom 𝐹 ) = +∞ ) ) |
15 |
14
|
3impia |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ dom 𝐹 ) = +∞ ) |
16 |
5 15
|
eqtr4d |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ∧ ¬ 𝐹 ∈ Fin ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) |
17 |
16
|
3comr |
⊢ ( ( ¬ 𝐹 ∈ Fin ∧ 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) |
18 |
17
|
3expib |
⊢ ( ¬ 𝐹 ∈ Fin → ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) ) |
19 |
3 18
|
pm2.61i |
⊢ ( ( 𝐹 ∈ 𝑉 ∧ Fun 𝐹 ) → ( ♯ ‘ 𝐹 ) = ( ♯ ‘ dom 𝐹 ) ) |