| Step | Hyp | Ref
| Expression |
| 1 | | n0 4353 |
. . . . . . 7
⊢ (𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
| 2 | | opelxp 5721 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
| 3 | | fvres 6925 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → ((1st ↾ (𝐴 × 𝐵))‘〈𝑥, 𝑦〉) = (1st ‘〈𝑥, 𝑦〉)) |
| 4 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
| 5 | | vex 3484 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
| 6 | 4, 5 | op1st 8022 |
. . . . . . . . . . . 12
⊢
(1st ‘〈𝑥, 𝑦〉) = 𝑥 |
| 7 | 3, 6 | eqtr2di 2794 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → 𝑥 = ((1st ↾ (𝐴 × 𝐵))‘〈𝑥, 𝑦〉)) |
| 8 | | f1stres 8038 |
. . . . . . . . . . . . 13
⊢
(1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 |
| 9 | | ffn 6736 |
. . . . . . . . . . . . 13
⊢
((1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 → (1st ↾ (𝐴 × 𝐵)) Fn (𝐴 × 𝐵)) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(1st ↾ (𝐴 × 𝐵)) Fn (𝐴 × 𝐵) |
| 11 | | fnfvelrn 7100 |
. . . . . . . . . . . 12
⊢
(((1st ↾ (𝐴 × 𝐵)) Fn (𝐴 × 𝐵) ∧ 〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵)) → ((1st ↾ (𝐴 × 𝐵))‘〈𝑥, 𝑦〉) ∈ ran (1st ↾
(𝐴 × 𝐵))) |
| 12 | 10, 11 | mpan 690 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → ((1st ↾ (𝐴 × 𝐵))‘〈𝑥, 𝑦〉) ∈ ran (1st ↾
(𝐴 × 𝐵))) |
| 13 | 7, 12 | eqeltrd 2841 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ (𝐴 × 𝐵) → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵))) |
| 14 | 2, 13 | sylbir 235 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵))) |
| 15 | 14 | expcom 413 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵)))) |
| 16 | 15 | exlimiv 1930 |
. . . . . . 7
⊢
(∃𝑦 𝑦 ∈ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵)))) |
| 17 | 1, 16 | sylbi 217 |
. . . . . 6
⊢ (𝐵 ≠ ∅ → (𝑥 ∈ 𝐴 → 𝑥 ∈ ran (1st ↾ (𝐴 × 𝐵)))) |
| 18 | 17 | ssrdv 3989 |
. . . . 5
⊢ (𝐵 ≠ ∅ → 𝐴 ⊆ ran (1st
↾ (𝐴 × 𝐵))) |
| 19 | | frn 6743 |
. . . . . 6
⊢
((1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 → ran (1st ↾ (𝐴 × 𝐵)) ⊆ 𝐴) |
| 20 | 8, 19 | ax-mp 5 |
. . . . 5
⊢ ran
(1st ↾ (𝐴
× 𝐵)) ⊆ 𝐴 |
| 21 | 18, 20 | jctil 519 |
. . . 4
⊢ (𝐵 ≠ ∅ → (ran
(1st ↾ (𝐴
× 𝐵)) ⊆ 𝐴 ∧ 𝐴 ⊆ ran (1st ↾ (𝐴 × 𝐵)))) |
| 22 | | eqss 3999 |
. . . 4
⊢ (ran
(1st ↾ (𝐴
× 𝐵)) = 𝐴 ↔ (ran (1st
↾ (𝐴 × 𝐵)) ⊆ 𝐴 ∧ 𝐴 ⊆ ran (1st ↾ (𝐴 × 𝐵)))) |
| 23 | 21, 22 | sylibr 234 |
. . 3
⊢ (𝐵 ≠ ∅ → ran
(1st ↾ (𝐴
× 𝐵)) = 𝐴) |
| 24 | 23, 8 | jctil 519 |
. 2
⊢ (𝐵 ≠ ∅ →
((1st ↾ (𝐴
× 𝐵)):(𝐴 × 𝐵)⟶𝐴 ∧ ran (1st ↾ (𝐴 × 𝐵)) = 𝐴)) |
| 25 | | dffo2 6824 |
. 2
⊢
((1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)–onto→𝐴 ↔ ((1st ↾ (𝐴 × 𝐵)):(𝐴 × 𝐵)⟶𝐴 ∧ ran (1st ↾ (𝐴 × 𝐵)) = 𝐴)) |
| 26 | 24, 25 | sylibr 234 |
1
⊢ (𝐵 ≠ ∅ →
(1st ↾ (𝐴
× 𝐵)):(𝐴 × 𝐵)–onto→𝐴) |