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