Step | Hyp | Ref
| Expression |
1 | | fo2nd 7189 |
. . . 4
⊢
2nd :V–onto→V |
2 | | fof 6115 |
. . . 4
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
3 | | ffn 6045 |
. . . 4
⊢
(2nd :V⟶V → 2nd Fn V) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢
2nd Fn V |
5 | | ssv 3625 |
. . 3
⊢ 𝑇 ⊆ V |
6 | | fnssres 6004 |
. . 3
⊢
((2nd Fn V ∧ 𝑇 ⊆ V) → (2nd ↾
𝑇) Fn 𝑇) |
7 | 4, 5, 6 | mp2an 708 |
. 2
⊢
(2nd ↾ 𝑇) Fn 𝑇 |
8 | | df-ima 5127 |
. . 3
⊢
(2nd “ 𝑇) = ran (2nd ↾ 𝑇) |
9 | | iunfo.1 |
. . . . . . . . . . 11
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
10 | 9 | eleq2i 2693 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑇 ↔ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
11 | | eliun 4524 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
12 | 10, 11 | bitri 264 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑇 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
13 | | xp2nd 7199 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
14 | | eleq1 2689 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) = 𝑦 → ((2nd ‘𝑧) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
15 | 13, 14 | syl5ib 234 |
. . . . . . . . . 10
⊢
((2nd ‘𝑧) = 𝑦 → (𝑧 ∈ ({𝑥} × 𝐵) → 𝑦 ∈ 𝐵)) |
16 | 15 | reximdv 3016 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) = 𝑦 → (∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
17 | 12, 16 | syl5bi 232 |
. . . . . . . 8
⊢
((2nd ‘𝑧) = 𝑦 → (𝑧 ∈ 𝑇 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
18 | 17 | impcom 446 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑇 ∧ (2nd ‘𝑧) = 𝑦) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
19 | 18 | rexlimiva 3028 |
. . . . . 6
⊢
(∃𝑧 ∈
𝑇 (2nd
‘𝑧) = 𝑦 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
20 | | nfiu1 4550 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
21 | 9, 20 | nfcxfr 2762 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑇 |
22 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑥(2nd ‘𝑧) = 𝑦 |
23 | 21, 22 | nfrex 3007 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦 |
24 | | ssiun2 4563 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → ({𝑥} × 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
25 | 24 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} × 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
26 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
27 | | vsnid 4209 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ {𝑥} |
28 | | opelxp 5146 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵) ↔ (𝑥 ∈ {𝑥} ∧ 𝑦 ∈ 𝐵)) |
29 | 27, 28 | mpbiran 953 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵) ↔ 𝑦 ∈ 𝐵) |
30 | 26, 29 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵)) |
31 | 25, 30 | sseldd 3604 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
32 | 31, 9 | syl6eleqr 2712 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝑇) |
33 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
34 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
35 | 33, 34 | op2nd 7177 |
. . . . . . . . 9
⊢
(2nd ‘〈𝑥, 𝑦〉) = 𝑦 |
36 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = (2nd
‘〈𝑥, 𝑦〉)) |
37 | 36 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2nd ‘𝑧) = 𝑦 ↔ (2nd ‘〈𝑥, 𝑦〉) = 𝑦)) |
38 | 37 | rspcev 3309 |
. . . . . . . . 9
⊢
((〈𝑥, 𝑦〉 ∈ 𝑇 ∧ (2nd ‘〈𝑥, 𝑦〉) = 𝑦) → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
39 | 32, 35, 38 | sylancl 694 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
40 | 39 | ex 450 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦)) |
41 | 23, 40 | rexlimi 3024 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ 𝐵 → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
42 | 19, 41 | impbii 199 |
. . . . 5
⊢
(∃𝑧 ∈
𝑇 (2nd
‘𝑧) = 𝑦 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
43 | | fvelimab 6253 |
. . . . . 6
⊢
((2nd Fn V ∧ 𝑇 ⊆ V) → (𝑦 ∈ (2nd “ 𝑇) ↔ ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦)) |
44 | 4, 5, 43 | mp2an 708 |
. . . . 5
⊢ (𝑦 ∈ (2nd “
𝑇) ↔ ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
45 | | eliun 4524 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
46 | 42, 44, 45 | 3bitr4i 292 |
. . . 4
⊢ (𝑦 ∈ (2nd “
𝑇) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) |
47 | 46 | eqriv 2619 |
. . 3
⊢
(2nd “ 𝑇) = ∪
𝑥 ∈ 𝐴 𝐵 |
48 | 8, 47 | eqtr3i 2646 |
. 2
⊢ ran
(2nd ↾ 𝑇)
= ∪ 𝑥 ∈ 𝐴 𝐵 |
49 | | df-fo 5894 |
. 2
⊢
((2nd ↾ 𝑇):𝑇–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ ((2nd ↾ 𝑇) Fn 𝑇 ∧ ran (2nd ↾ 𝑇) = ∪ 𝑥 ∈ 𝐴 𝐵)) |
50 | 7, 48, 49 | mpbir2an 955 |
1
⊢
(2nd ↾ 𝑇):𝑇–onto→∪ 𝑥 ∈ 𝐴 𝐵 |