Step | Hyp | Ref
| Expression |
1 | | fo2nd 7080 |
. . . 4
⊢
2nd :V–onto→V |
2 | | fof 6028 |
. . . 4
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
3 | | ffn 5958 |
. . . 4
⊢
(2nd :V⟶V → 2nd Fn V) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢
2nd Fn V |
5 | | ssv 3588 |
. . 3
⊢ 𝑇 ⊆ V |
6 | | fnssres 5918 |
. . 3
⊢
((2nd Fn V ∧ 𝑇 ⊆ V) → (2nd ↾
𝑇) Fn 𝑇) |
7 | 4, 5, 6 | mp2an 704 |
. 2
⊢
(2nd ↾ 𝑇) Fn 𝑇 |
8 | | df-ima 5051 |
. . 3
⊢
(2nd “ 𝑇) = ran (2nd ↾ 𝑇) |
9 | | iunfo.1 |
. . . . . . . . . . 11
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
10 | 9 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑇 ↔ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
11 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
12 | 10, 11 | bitri 263 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑇 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
13 | | xp2nd 7090 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
14 | | eleq1 2676 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) = 𝑦 → ((2nd ‘𝑧) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
15 | 13, 14 | syl5ib 233 |
. . . . . . . . . 10
⊢
((2nd ‘𝑧) = 𝑦 → (𝑧 ∈ ({𝑥} × 𝐵) → 𝑦 ∈ 𝐵)) |
16 | 15 | reximdv 2999 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) = 𝑦 → (∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
17 | 12, 16 | syl5bi 231 |
. . . . . . . 8
⊢
((2nd ‘𝑧) = 𝑦 → (𝑧 ∈ 𝑇 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
18 | 17 | impcom 445 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑇 ∧ (2nd ‘𝑧) = 𝑦) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
19 | 18 | rexlimiva 3010 |
. . . . . 6
⊢
(∃𝑧 ∈
𝑇 (2nd
‘𝑧) = 𝑦 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
20 | | nfiu1 4486 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
21 | 9, 20 | nfcxfr 2749 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑇 |
22 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑥(2nd ‘𝑧) = 𝑦 |
23 | 21, 22 | nfrex 2990 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦 |
24 | | ssiun2 4499 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → ({𝑥} × 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
25 | 24 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} × 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
26 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
27 | | vsnid 4156 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ {𝑥} |
28 | | opelxp 5070 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵) ↔ (𝑥 ∈ {𝑥} ∧ 𝑦 ∈ 𝐵)) |
29 | 27, 28 | mpbiran 955 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵) ↔ 𝑦 ∈ 𝐵) |
30 | 26, 29 | sylibr 223 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵)) |
31 | 25, 30 | sseldd 3569 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
32 | 31, 9 | syl6eleqr 2699 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝑇) |
33 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
34 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
35 | 33, 34 | op2nd 7068 |
. . . . . . . . 9
⊢
(2nd ‘〈𝑥, 𝑦〉) = 𝑦 |
36 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = (2nd
‘〈𝑥, 𝑦〉)) |
37 | 36 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2nd ‘𝑧) = 𝑦 ↔ (2nd ‘〈𝑥, 𝑦〉) = 𝑦)) |
38 | 37 | rspcev 3282 |
. . . . . . . . 9
⊢
((〈𝑥, 𝑦〉 ∈ 𝑇 ∧ (2nd ‘〈𝑥, 𝑦〉) = 𝑦) → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
39 | 32, 35, 38 | sylancl 693 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
40 | 39 | ex 449 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦)) |
41 | 23, 40 | rexlimi 3006 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ 𝐵 → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
42 | 19, 41 | impbii 198 |
. . . . 5
⊢
(∃𝑧 ∈
𝑇 (2nd
‘𝑧) = 𝑦 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
43 | | fvelimab 6163 |
. . . . . 6
⊢
((2nd Fn V ∧ 𝑇 ⊆ V) → (𝑦 ∈ (2nd “ 𝑇) ↔ ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦)) |
44 | 4, 5, 43 | mp2an 704 |
. . . . 5
⊢ (𝑦 ∈ (2nd “
𝑇) ↔ ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
45 | | eliun 4460 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
46 | 42, 44, 45 | 3bitr4i 291 |
. . . 4
⊢ (𝑦 ∈ (2nd “
𝑇) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) |
47 | 46 | eqriv 2607 |
. . 3
⊢
(2nd “ 𝑇) = ∪
𝑥 ∈ 𝐴 𝐵 |
48 | 8, 47 | eqtr3i 2634 |
. 2
⊢ ran
(2nd ↾ 𝑇)
= ∪ 𝑥 ∈ 𝐴 𝐵 |
49 | | df-fo 5810 |
. 2
⊢
((2nd ↾ 𝑇):𝑇–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ ((2nd ↾ 𝑇) Fn 𝑇 ∧ ran (2nd ↾ 𝑇) = ∪ 𝑥 ∈ 𝐴 𝐵)) |
50 | 7, 48, 49 | mpbir2an 957 |
1
⊢
(2nd ↾ 𝑇):𝑇–onto→∪ 𝑥 ∈ 𝐴 𝐵 |