| Step | Hyp | Ref
| Expression |
| 1 | | f1fn 6805 |
. . . 4
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
| 2 | | fvelimab 6981 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋))) |
| 3 | 1, 2 | sylan 580 |
. . 3
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋))) |
| 4 | 3 | 3adant2 1132 |
. 2
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋))) |
| 5 | | ssel 3977 |
. . . . . . . 8
⊢ (𝑌 ⊆ 𝐴 → (𝑧 ∈ 𝑌 → 𝑧 ∈ 𝐴)) |
| 6 | 5 | impac 552 |
. . . . . . 7
⊢ ((𝑌 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑌) → (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑌)) |
| 7 | | f1fveq 7282 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑧 ∈ 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹‘𝑧) = (𝐹‘𝑋) ↔ 𝑧 = 𝑋)) |
| 8 | 7 | ancom2s 650 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) = (𝐹‘𝑋) ↔ 𝑧 = 𝑋)) |
| 9 | 8 | biimpd 229 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑧 = 𝑋)) |
| 10 | 9 | anassrs 467 |
. . . . . . . . 9
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑧 = 𝑋)) |
| 11 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑋 → (𝑧 ∈ 𝑌 ↔ 𝑋 ∈ 𝑌)) |
| 12 | 11 | biimpcd 249 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑌 → (𝑧 = 𝑋 → 𝑋 ∈ 𝑌)) |
| 13 | 10, 12 | sylan9 507 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ 𝑧 ∈ 𝑌) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌)) |
| 14 | 13 | anasss 466 |
. . . . . . 7
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ (𝑧 ∈ 𝐴 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌)) |
| 15 | 6, 14 | sylan2 593 |
. . . . . 6
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ (𝑌 ⊆ 𝐴 ∧ 𝑧 ∈ 𝑌)) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌)) |
| 16 | 15 | anassrs 467 |
. . . . 5
⊢ ((((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ⊆ 𝐴) ∧ 𝑧 ∈ 𝑌) → ((𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌)) |
| 17 | 16 | rexlimdva 3155 |
. . . 4
⊢ (((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) ∧ 𝑌 ⊆ 𝐴) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌)) |
| 18 | 17 | 3impa 1110 |
. . 3
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋) → 𝑋 ∈ 𝑌)) |
| 19 | | eqid 2737 |
. . . 4
⊢ (𝐹‘𝑋) = (𝐹‘𝑋) |
| 20 | | fveqeq2 6915 |
. . . . 5
⊢ (𝑧 = 𝑋 → ((𝐹‘𝑧) = (𝐹‘𝑋) ↔ (𝐹‘𝑋) = (𝐹‘𝑋))) |
| 21 | 20 | rspcev 3622 |
. . . 4
⊢ ((𝑋 ∈ 𝑌 ∧ (𝐹‘𝑋) = (𝐹‘𝑋)) → ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋)) |
| 22 | 19, 21 | mpan2 691 |
. . 3
⊢ (𝑋 ∈ 𝑌 → ∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋)) |
| 23 | 18, 22 | impbid1 225 |
. 2
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (∃𝑧 ∈ 𝑌 (𝐹‘𝑧) = (𝐹‘𝑋) ↔ 𝑋 ∈ 𝑌)) |
| 24 | 4, 23 | bitrd 279 |
1
⊢ ((𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝐹‘𝑋) ∈ (𝐹 “ 𝑌) ↔ 𝑋 ∈ 𝑌)) |