Step | Hyp | Ref
| Expression |
1 | | eleq1 2097 |
. . 3
⊢ (v = y →
(v ∈
B ↔ y ∈ B)) |
2 | 1 | cbvexv 1792 |
. 2
⊢ (∃v v ∈ B ↔ ∃y y ∈ B) |
3 | | opelxp 4317 |
. . . . . . . . . 10
⊢
(〈u, v〉 ∈
(A × B) ↔ (u
∈ A ∧ v ∈ B)) |
4 | | fvres 5141 |
. . . . . . . . . . . 12
⊢
(〈u, v〉 ∈
(A × B) → ((1st ↾ (A × B))‘〈u, v〉) =
(1st ‘〈u, v〉)) |
5 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ u ∈
V |
6 | | vex 2554 |
. . . . . . . . . . . . 13
⊢ v ∈
V |
7 | 5, 6 | op1st 5715 |
. . . . . . . . . . . 12
⊢
(1st ‘〈u,
v〉) = u |
8 | 4, 7 | syl6req 2086 |
. . . . . . . . . . 11
⊢
(〈u, v〉 ∈
(A × B) → u =
((1st ↾ (A ×
B))‘〈u, v〉)) |
9 | | f1stres 5728 |
. . . . . . . . . . . . 13
⊢
(1st ↾ (A ×
B)):(A
× B)⟶A |
10 | | ffn 4989 |
. . . . . . . . . . . . 13
⊢
((1st ↾ (A ×
B)):(A
× B)⟶A → (1st ↾ (A × B)) Fn
(A × B)) |
11 | 9, 10 | ax-mp 7 |
. . . . . . . . . . . 12
⊢
(1st ↾ (A ×
B)) Fn (A × B) |
12 | | fnfvelrn 5242 |
. . . . . . . . . . . 12
⊢
(((1st ↾ (A ×
B)) Fn (A × B)
∧ 〈u,
v〉 ∈
(A × B)) → ((1st ↾ (A × B))‘〈u, v〉)
∈ ran (1st ↾ (A × B))) |
13 | 11, 12 | mpan 400 |
. . . . . . . . . . 11
⊢
(〈u, v〉 ∈
(A × B) → ((1st ↾ (A × B))‘〈u, v〉)
∈ ran (1st ↾ (A × B))) |
14 | 8, 13 | eqeltrd 2111 |
. . . . . . . . . 10
⊢
(〈u, v〉 ∈
(A × B) → u
∈ ran (1st ↾ (A × B))) |
15 | 3, 14 | sylbir 125 |
. . . . . . . . 9
⊢
((u ∈ A ∧ v ∈ B) →
u ∈ ran
(1st ↾ (A × B))) |
16 | 15 | expcom 109 |
. . . . . . . 8
⊢ (v ∈ B → (u
∈ A
→ u ∈ ran (1st ↾ (A × B)))) |
17 | 16 | exlimiv 1486 |
. . . . . . 7
⊢ (∃v v ∈ B → (u
∈ A
→ u ∈ ran (1st ↾ (A × B)))) |
18 | 17 | ssrdv 2945 |
. . . . . 6
⊢ (∃v v ∈ B → A
⊆ ran (1st ↾ (A
× B))) |
19 | | frn 4995 |
. . . . . . 7
⊢
((1st ↾ (A ×
B)):(A
× B)⟶A → ran (1st ↾ (A × B))
⊆ A) |
20 | 9, 19 | ax-mp 7 |
. . . . . 6
⊢ ran
(1st ↾ (A × B)) ⊆ A |
21 | 18, 20 | jctil 295 |
. . . . 5
⊢ (∃v v ∈ B → (ran (1st ↾ (A × B))
⊆ A ∧ A ⊆ ran
(1st ↾ (A × B)))) |
22 | | eqss 2954 |
. . . . 5
⊢ (ran
(1st ↾ (A × B)) = A ↔
(ran (1st ↾ (A ×
B)) ⊆ A ∧ A ⊆ ran (1st ↾ (A × B)))) |
23 | 21, 22 | sylibr 137 |
. . . 4
⊢ (∃v v ∈ B → ran (1st ↾ (A × B)) =
A) |
24 | 23, 9 | jctil 295 |
. . 3
⊢ (∃v v ∈ B → ((1st ↾ (A × B)):(A ×
B)⟶A ∧ ran
(1st ↾ (A × B)) = A)) |
25 | | dffo2 5053 |
. . 3
⊢
((1st ↾ (A ×
B)):(A
× B)–onto→A ↔
((1st ↾ (A ×
B)):(A
× B)⟶A ∧ ran
(1st ↾ (A × B)) = A)) |
26 | 24, 25 | sylibr 137 |
. 2
⊢ (∃v v ∈ B → (1st ↾ (A × B)):(A ×
B)–onto→A) |
27 | 2, 26 | sylbir 125 |
1
⊢ (∃y y ∈ B → (1st ↾ (A × B)):(A ×
B)–onto→A) |