Proof of Theorem elpreima
Step | Hyp | Ref
| Expression |
1 | | cnvimass 5923 |
. . . . 5
⊢ (◡𝐹 “ 𝐶) ⊆ dom 𝐹 |
2 | 1 | sseli 3873 |
. . . 4
⊢ (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ dom 𝐹) |
3 | | fndm 6440 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
4 | 3 | eleq2d 2818 |
. . . 4
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ dom 𝐹 ↔ 𝐵 ∈ 𝐴)) |
5 | 2, 4 | syl5ib 247 |
. . 3
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → 𝐵 ∈ 𝐴)) |
6 | | fnfun 6438 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
7 | | fvimacnvi 6831 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶) |
8 | 6, 7 | sylan 583 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ (◡𝐹 “ 𝐶)) → (𝐹‘𝐵) ∈ 𝐶) |
9 | 8 | ex 416 |
. . 3
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐹‘𝐵) ∈ 𝐶)) |
10 | 5, 9 | jcad 516 |
. 2
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) → (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) |
11 | | fvimacnv 6832 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝐵 ∈ dom 𝐹) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶))) |
12 | 11 | funfni 6443 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 ↔ 𝐵 ∈ (◡𝐹 “ 𝐶))) |
13 | 12 | biimpd 232 |
. . 3
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → ((𝐹‘𝐵) ∈ 𝐶 → 𝐵 ∈ (◡𝐹 “ 𝐶))) |
14 | 13 | expimpd 457 |
. 2
⊢ (𝐹 Fn 𝐴 → ((𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶) → 𝐵 ∈ (◡𝐹 “ 𝐶))) |
15 | 10, 14 | impbid 215 |
1
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ (◡𝐹 “ 𝐶) ↔ (𝐵 ∈ 𝐴 ∧ (𝐹‘𝐵) ∈ 𝐶))) |