Step |
Hyp |
Ref |
Expression |
1 |
|
psrbag.d |
⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } |
2 |
|
cnveq |
⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 ) |
3 |
2
|
imaeq1d |
⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝐹 “ ℕ ) ) |
4 |
3
|
eleq1d |
⊢ ( 𝑓 = 𝐹 → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) |
5 |
4 1
|
elrab2 |
⊢ ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) |
6 |
|
nn0ex |
⊢ ℕ0 ∈ V |
7 |
|
elmapg |
⊢ ( ( ℕ0 ∈ V ∧ 𝐼 ∈ 𝑉 ) → ( 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) ↔ 𝐹 : 𝐼 ⟶ ℕ0 ) ) |
8 |
6 7
|
mpan |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) ↔ 𝐹 : 𝐼 ⟶ ℕ0 ) ) |
9 |
8
|
anbi1d |
⊢ ( 𝐼 ∈ 𝑉 → ( ( 𝐹 ∈ ( ℕ0 ↑m 𝐼 ) ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) ) |
10 |
5 9
|
syl5bb |
⊢ ( 𝐼 ∈ 𝑉 → ( 𝐹 ∈ 𝐷 ↔ ( 𝐹 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝐹 “ ℕ ) ∈ Fin ) ) ) |