Step | Hyp | Ref
| Expression |
1 | | n0 4307 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
2 | | opelxp 5670 |
. . . . . . . . . 10
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
3 | | fvres 6862 |
. . . . . . . . . . . 12
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) → ((1st ↾ (𝐴 × 𝐵))‘⟨𝑥, 𝑦⟩) = (1st ‘⟨𝑥, 𝑦⟩)) |
4 | | vex 3450 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
5 | | vex 3450 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
6 | 4, 5 | op1st 7930 |
. . . . . . . . . . . 12
⊢
(1st ‘⟨𝑥, 𝑦⟩) = 𝑥 |
7 | 3, 6 | eqtr2di 2794 |
. . . . . . . . . . 11
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) → 𝑥 = ((1st ↾ (𝐴 × 𝐵))‘⟨𝑥, 𝑦⟩)) |
8 | | f1stres 7946 |
. . . . . . . . . . . . 13
⊢
(1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 |
9 | | ffn 6669 |
. . . . . . . . . . . . 13
⊢
((1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 → (1st ↾ (𝐴 × 𝐵)) Fn (𝐴 × 𝐵)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1st ↾ (𝐴 × 𝐵)) Fn (𝐴 × 𝐵) |
11 | | fnfvelrn 7032 |
. . . . . . . . . . . 12
⊢
(((1st ↾ (𝐴 × 𝐵)) Fn (𝐴 × 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵)) → ((1st ↾ (𝐴 × 𝐵))‘⟨𝑥, 𝑦⟩) ∈ ran (1st ↾
(𝐴 × 𝐵))) |
12 | 10, 11 | mpan 689 |
. . . . . . . . . . 11
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) → ((1st ↾ (𝐴 × 𝐵))‘⟨𝑥, 𝑦⟩) ∈ ran (1st ↾
(𝐴 × 𝐵))) |
13 | 7, 12 | eqeltrd 2838 |
. . . . . . . . . 10
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐴 × 𝐵) → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵))) |
14 | 2, 13 | sylbir 234 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵))) |
15 | 14 | expcom 415 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵)))) |
16 | 15 | exlimiv 1934 |
. . . . . . 7
⊢
(∃𝑦 𝑦 ∈ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵)))) |
17 | 1, 16 | sylbi 216 |
. . . . . 6
⊢ (𝐵 ≠ ∅ → (𝑥 ∈ 𝐴 → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵)))) |
18 | 17 | ssrdv 3951 |
. . . . 5
⊢ (𝐵 ≠ ∅ → 𝐴 ⊆ ran (1st
↾ (𝐴 × 𝐵))) |
19 | | frn 6676 |
. . . . . 6
⊢
((1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 → ran (1st ↾ (𝐴 × 𝐵)) ⊆ 𝐴) |
20 | 8, 19 | ax-mp 5 |
. . . . 5
⊢ ran
(1st ↾ (𝐴
× 𝐵)) ⊆ 𝐴 |
21 | 18, 20 | jctil 521 |
. . . 4
⊢ (𝐵 ≠ ∅ → (ran
(1st ↾ (𝐴
× 𝐵)) ⊆ 𝐴 ∧ 𝐴 ⊆ ran (1st ↾ (𝐴 × 𝐵)))) |
22 | | eqss 3960 |
. . . 4
⊢ (ran
(1st ↾ (𝐴
× 𝐵)) = 𝐴 ↔ (ran (1st
↾ (𝐴 × 𝐵)) ⊆ 𝐴 ∧ 𝐴 ⊆ ran (1st ↾ (𝐴 × 𝐵)))) |
23 | 21, 22 | sylibr 233 |
. . 3
⊢ (𝐵 ≠ ∅ → ran
(1st ↾ (𝐴
× 𝐵)) = 𝐴) |
24 | 23, 8 | jctil 521 |
. 2
⊢ (𝐵 ≠ ∅ →
((1st ↾ (𝐴
× 𝐵)):(𝐴 × 𝐵)⟶𝐴 ∧ ran (1st ↾ (𝐴 × 𝐵)) = 𝐴)) |
25 | | dffo2 6761 |
. 2
⊢
((1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐴 ↔ ((1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 ∧ ran (1st ↾ (𝐴 × 𝐵)) = 𝐴)) |
26 | 24, 25 | sylibr 233 |
1
⊢ (𝐵 ≠ ∅ →
(1st ↾ (𝐴
× 𝐵)):(𝐴 × 𝐵)–onto→𝐴) |