Step | Hyp | Ref
| Expression |
1 | | fo2nd 7735 |
. . . 4
⊢
2nd :V–onto→V |
2 | | fof 6592 |
. . . 4
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
3 | | ffn 6504 |
. . . 4
⊢
(2nd :V⟶V → 2nd Fn V) |
4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢
2nd Fn V |
5 | | ssv 3901 |
. . 3
⊢ 𝑇 ⊆ V |
6 | | fnssres 6459 |
. . 3
⊢
((2nd Fn V ∧ 𝑇 ⊆ V) → (2nd ↾
𝑇) Fn 𝑇) |
7 | 4, 5, 6 | mp2an 692 |
. 2
⊢
(2nd ↾ 𝑇) Fn 𝑇 |
8 | | df-ima 5538 |
. . 3
⊢
(2nd “ 𝑇) = ran (2nd ↾ 𝑇) |
9 | | iunfo.1 |
. . . . . . . . . . 11
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
10 | 9 | eleq2i 2824 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑇 ↔ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
11 | | eliun 4885 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
12 | 10, 11 | bitri 278 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑇 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
13 | | xp2nd 7747 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
14 | | eleq1 2820 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) = 𝑦 → ((2nd ‘𝑧) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
15 | 13, 14 | syl5ib 247 |
. . . . . . . . . 10
⊢
((2nd ‘𝑧) = 𝑦 → (𝑧 ∈ ({𝑥} × 𝐵) → 𝑦 ∈ 𝐵)) |
16 | 15 | reximdv 3183 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) = 𝑦 → (∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
17 | 12, 16 | syl5bi 245 |
. . . . . . . 8
⊢
((2nd ‘𝑧) = 𝑦 → (𝑧 ∈ 𝑇 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
18 | 17 | impcom 411 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑇 ∧ (2nd ‘𝑧) = 𝑦) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
19 | 18 | rexlimiva 3191 |
. . . . . 6
⊢
(∃𝑧 ∈
𝑇 (2nd
‘𝑧) = 𝑦 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
20 | | nfiu1 4915 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
21 | 9, 20 | nfcxfr 2897 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑇 |
22 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑥(2nd ‘𝑧) = 𝑦 |
23 | 21, 22 | nfrex 3219 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦 |
24 | | ssiun2 4933 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → ({𝑥} × 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
25 | 24 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} × 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
26 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
27 | | vsnid 4553 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ {𝑥} |
28 | | opelxp 5561 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵) ↔ (𝑥 ∈ {𝑥} ∧ 𝑦 ∈ 𝐵)) |
29 | 27, 28 | mpbiran 709 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵) ↔ 𝑦 ∈ 𝐵) |
30 | 26, 29 | sylibr 237 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵)) |
31 | 25, 30 | sseldd 3878 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
32 | 31, 9 | eleqtrrdi 2844 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝑇) |
33 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
34 | | vex 3402 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
35 | 33, 34 | op2nd 7723 |
. . . . . . . . 9
⊢
(2nd ‘〈𝑥, 𝑦〉) = 𝑦 |
36 | | fveqeq2 6683 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2nd ‘𝑧) = 𝑦 ↔ (2nd ‘〈𝑥, 𝑦〉) = 𝑦)) |
37 | 36 | rspcev 3526 |
. . . . . . . . 9
⊢
((〈𝑥, 𝑦〉 ∈ 𝑇 ∧ (2nd ‘〈𝑥, 𝑦〉) = 𝑦) → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
38 | 32, 35, 37 | sylancl 589 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
39 | 38 | ex 416 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦)) |
40 | 23, 39 | rexlimi 3225 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ 𝐵 → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
41 | 19, 40 | impbii 212 |
. . . . 5
⊢
(∃𝑧 ∈
𝑇 (2nd
‘𝑧) = 𝑦 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
42 | | fvelimab 6741 |
. . . . . 6
⊢
((2nd Fn V ∧ 𝑇 ⊆ V) → (𝑦 ∈ (2nd “ 𝑇) ↔ ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦)) |
43 | 4, 5, 42 | mp2an 692 |
. . . . 5
⊢ (𝑦 ∈ (2nd “
𝑇) ↔ ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
44 | | eliun 4885 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
45 | 41, 43, 44 | 3bitr4i 306 |
. . . 4
⊢ (𝑦 ∈ (2nd “
𝑇) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) |
46 | 45 | eqriv 2735 |
. . 3
⊢
(2nd “ 𝑇) = ∪
𝑥 ∈ 𝐴 𝐵 |
47 | 8, 46 | eqtr3i 2763 |
. 2
⊢ ran
(2nd ↾ 𝑇)
= ∪ 𝑥 ∈ 𝐴 𝐵 |
48 | | df-fo 6345 |
. 2
⊢
((2nd ↾ 𝑇):𝑇–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ ((2nd ↾ 𝑇) Fn 𝑇 ∧ ran (2nd ↾ 𝑇) = ∪ 𝑥 ∈ 𝐴 𝐵)) |
49 | 7, 47, 48 | mpbir2an 711 |
1
⊢
(2nd ↾ 𝑇):𝑇–onto→∪ 𝑥 ∈ 𝐴 𝐵 |