Step |
Hyp |
Ref |
Expression |
1 |
|
hashf |
⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) |
2 |
|
ffn |
⊢ ( ♯ : V ⟶ ( ℕ0 ∪ { +∞ } ) → ♯ Fn V ) |
3 |
|
elpreima |
⊢ ( ♯ Fn V → ( 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ( 𝐴 ∈ V ∧ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) ) ) |
4 |
1 2 3
|
mp2b |
⊢ ( 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ( 𝐴 ∈ V ∧ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) ) |
5 |
|
elex |
⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V ) |
6 |
5
|
biantrurd |
⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ↔ ( 𝐴 ∈ V ∧ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) ) ) |
7 |
4 6
|
bitr4id |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) ) |
8 |
7
|
notbid |
⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ ¬ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ) ) |
9 |
|
hashxnn0 |
⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℕ0* ) |
10 |
|
xnn01gt |
⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0* → ( ¬ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ↔ 1 < ( ♯ ‘ 𝐴 ) ) ) |
11 |
9 10
|
syl |
⊢ ( 𝐴 ∈ 𝑉 → ( ¬ ( ♯ ‘ 𝐴 ) ∈ { 0 , 1 } ↔ 1 < ( ♯ ‘ 𝐴 ) ) ) |
12 |
8 11
|
bitrd |
⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ ( ◡ ♯ “ { 0 , 1 } ) ↔ 1 < ( ♯ ‘ 𝐴 ) ) ) |