Step | Hyp | Ref
| Expression |
1 | | f1fn 5259 |
. . . 4
⊢ (F:A–1-1→B
→ F Fn A) |
2 | | fvelimab 5370 |
. . . 4
⊢ ((F Fn A ∧ Y ⊆ A) →
((F ‘X) ∈ (F “ Y)
↔ ∃z ∈ Y (F
‘z) = (F ‘X))) |
3 | 1, 2 | sylan 457 |
. . 3
⊢ ((F:A–1-1→B
∧ Y ⊆ A) →
((F ‘X) ∈ (F “ Y)
↔ ∃z ∈ Y (F
‘z) = (F ‘X))) |
4 | 3 | 3adant2 974 |
. 2
⊢ ((F:A–1-1→B
∧ X ∈ A ∧ Y ⊆ A) →
((F ‘X) ∈ (F “ Y)
↔ ∃z ∈ Y (F
‘z) = (F ‘X))) |
5 | | ssel 3267 |
. . . . . . . 8
⊢ (Y ⊆ A → (z
∈ Y
→ z ∈ A)) |
6 | 5 | impac 604 |
. . . . . . 7
⊢ ((Y ⊆ A ∧ z ∈ Y) → (z
∈ A ∧ z ∈ Y)) |
7 | | f1fveq 5473 |
. . . . . . . . . . . 12
⊢ ((F:A–1-1→B
∧ (z ∈ A ∧ X ∈ A)) →
((F ‘z) = (F
‘X) ↔ z = X)) |
8 | 7 | ancom2s 777 |
. . . . . . . . . . 11
⊢ ((F:A–1-1→B
∧ (X ∈ A ∧ z ∈ A)) →
((F ‘z) = (F
‘X) ↔ z = X)) |
9 | 8 | biimpd 198 |
. . . . . . . . . 10
⊢ ((F:A–1-1→B
∧ (X ∈ A ∧ z ∈ A)) →
((F ‘z) = (F
‘X) → z = X)) |
10 | 9 | anassrs 629 |
. . . . . . . . 9
⊢ (((F:A–1-1→B
∧ X ∈ A) ∧ z ∈ A) →
((F ‘z) = (F
‘X) → z = X)) |
11 | | eleq1 2413 |
. . . . . . . . . 10
⊢ (z = X →
(z ∈
Y ↔ X ∈ Y)) |
12 | 11 | biimpcd 215 |
. . . . . . . . 9
⊢ (z ∈ Y → (z =
X → X ∈ Y)) |
13 | 10, 12 | sylan9 638 |
. . . . . . . 8
⊢ ((((F:A–1-1→B
∧ X ∈ A) ∧ z ∈ A) ∧ z ∈ Y) →
((F ‘z) = (F
‘X) → X ∈ Y)) |
14 | 13 | anasss 628 |
. . . . . . 7
⊢ (((F:A–1-1→B
∧ X ∈ A) ∧ (z ∈ A ∧ z ∈ Y)) →
((F ‘z) = (F
‘X) → X ∈ Y)) |
15 | 6, 14 | sylan2 460 |
. . . . . 6
⊢ (((F:A–1-1→B
∧ X ∈ A) ∧ (Y ⊆ A ∧ z ∈ Y)) →
((F ‘z) = (F
‘X) → X ∈ Y)) |
16 | 15 | anassrs 629 |
. . . . 5
⊢ ((((F:A–1-1→B
∧ X ∈ A) ∧ Y ⊆ A) ∧ z ∈ Y) →
((F ‘z) = (F
‘X) → X ∈ Y)) |
17 | 16 | rexlimdva 2738 |
. . . 4
⊢ (((F:A–1-1→B
∧ X ∈ A) ∧ Y ⊆ A) →
(∃z
∈ Y
(F ‘z) = (F
‘X) → X ∈ Y)) |
18 | 17 | 3impa 1146 |
. . 3
⊢ ((F:A–1-1→B
∧ X ∈ A ∧ Y ⊆ A) →
(∃z
∈ Y
(F ‘z) = (F
‘X) → X ∈ Y)) |
19 | | eqid 2353 |
. . . 4
⊢ (F ‘X) =
(F ‘X) |
20 | | fveq2 5328 |
. . . . . 6
⊢ (z = X →
(F ‘z) = (F
‘X)) |
21 | 20 | eqeq1d 2361 |
. . . . 5
⊢ (z = X →
((F ‘z) = (F
‘X) ↔ (F ‘X) =
(F ‘X))) |
22 | 21 | rspcev 2955 |
. . . 4
⊢ ((X ∈ Y ∧ (F ‘X) =
(F ‘X)) → ∃z ∈ Y (F ‘z) =
(F ‘X)) |
23 | 19, 22 | mpan2 652 |
. . 3
⊢ (X ∈ Y → ∃z ∈ Y (F ‘z) =
(F ‘X)) |
24 | 18, 23 | impbid1 194 |
. 2
⊢ ((F:A–1-1→B
∧ X ∈ A ∧ Y ⊆ A) →
(∃z
∈ Y
(F ‘z) = (F
‘X) ↔ X ∈ Y)) |
25 | 4, 24 | bitrd 244 |
1
⊢ ((F:A–1-1→B
∧ X ∈ A ∧ Y ⊆ A) →
((F ‘X) ∈ (F “ Y)
↔ X ∈ Y)) |