| Step | Hyp | Ref
| Expression |
| 1 | | fo2nd 8035 |
. . . 4
⊢
2nd :V–onto→V |
| 2 | | fof 6820 |
. . . 4
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
| 3 | | ffn 6736 |
. . . 4
⊢
(2nd :V⟶V → 2nd Fn V) |
| 4 | 1, 2, 3 | mp2b 10 |
. . 3
⊢
2nd Fn V |
| 5 | | ssv 4008 |
. . 3
⊢ 𝑇 ⊆ V |
| 6 | | fnssres 6691 |
. . 3
⊢
((2nd Fn V ∧ 𝑇 ⊆ V) → (2nd ↾
𝑇) Fn 𝑇) |
| 7 | 4, 5, 6 | mp2an 692 |
. 2
⊢
(2nd ↾ 𝑇) Fn 𝑇 |
| 8 | | df-ima 5698 |
. . 3
⊢
(2nd “ 𝑇) = ran (2nd ↾ 𝑇) |
| 9 | | iunfo.1 |
. . . . . . . . . . 11
⊢ 𝑇 = ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
| 10 | 9 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑇 ↔ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
| 11 | | eliun 4995 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
| 12 | 10, 11 | bitri 275 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝑇 ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
| 13 | | xp2nd 8047 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
| 14 | | eleq1 2829 |
. . . . . . . . . . 11
⊢
((2nd ‘𝑧) = 𝑦 → ((2nd ‘𝑧) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
| 15 | 13, 14 | imbitrid 244 |
. . . . . . . . . 10
⊢
((2nd ‘𝑧) = 𝑦 → (𝑧 ∈ ({𝑥} × 𝐵) → 𝑦 ∈ 𝐵)) |
| 16 | 15 | reximdv 3170 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) = 𝑦 → (∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
| 17 | 12, 16 | biimtrid 242 |
. . . . . . . 8
⊢
((2nd ‘𝑧) = 𝑦 → (𝑧 ∈ 𝑇 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
| 18 | 17 | impcom 407 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑇 ∧ (2nd ‘𝑧) = 𝑦) → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
| 19 | 18 | rexlimiva 3147 |
. . . . . 6
⊢
(∃𝑧 ∈
𝑇 (2nd
‘𝑧) = 𝑦 → ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
| 20 | | nfiu1 5027 |
. . . . . . . . 9
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
| 21 | 9, 20 | nfcxfr 2903 |
. . . . . . . 8
⊢
Ⅎ𝑥𝑇 |
| 22 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑥(2nd ‘𝑧) = 𝑦 |
| 23 | 21, 22 | nfrexw 3313 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦 |
| 24 | | ssiun2 5047 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 → ({𝑥} × 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ({𝑥} × 𝐵) ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
| 26 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
| 27 | | vsnid 4663 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ {𝑥} |
| 28 | | opelxp 5721 |
. . . . . . . . . . . . 13
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵) ↔ (𝑥 ∈ {𝑥} ∧ 𝑦 ∈ 𝐵)) |
| 29 | 27, 28 | mpbiran 709 |
. . . . . . . . . . . 12
⊢
(〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵) ↔ 𝑦 ∈ 𝐵) |
| 30 | 26, 29 | sylibr 234 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ ({𝑥} × 𝐵)) |
| 31 | 25, 30 | sseldd 3984 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
| 32 | 31, 9 | eleqtrrdi 2852 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑥, 𝑦〉 ∈ 𝑇) |
| 33 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 34 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
| 35 | 33, 34 | op2nd 8023 |
. . . . . . . . 9
⊢
(2nd ‘〈𝑥, 𝑦〉) = 𝑦 |
| 36 | | fveqeq2 6915 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((2nd ‘𝑧) = 𝑦 ↔ (2nd ‘〈𝑥, 𝑦〉) = 𝑦)) |
| 37 | 36 | rspcev 3622 |
. . . . . . . . 9
⊢
((〈𝑥, 𝑦〉 ∈ 𝑇 ∧ (2nd ‘〈𝑥, 𝑦〉) = 𝑦) → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
| 38 | 32, 35, 37 | sylancl 586 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
| 39 | 38 | ex 412 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦)) |
| 40 | 23, 39 | rexlimi 3259 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐴 𝑦 ∈ 𝐵 → ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
| 41 | 19, 40 | impbii 209 |
. . . . 5
⊢
(∃𝑧 ∈
𝑇 (2nd
‘𝑧) = 𝑦 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
| 42 | | fvelimab 6981 |
. . . . . 6
⊢
((2nd Fn V ∧ 𝑇 ⊆ V) → (𝑦 ∈ (2nd “ 𝑇) ↔ ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦)) |
| 43 | 4, 5, 42 | mp2an 692 |
. . . . 5
⊢ (𝑦 ∈ (2nd “
𝑇) ↔ ∃𝑧 ∈ 𝑇 (2nd ‘𝑧) = 𝑦) |
| 44 | | eliun 4995 |
. . . . 5
⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
| 45 | 41, 43, 44 | 3bitr4i 303 |
. . . 4
⊢ (𝑦 ∈ (2nd “
𝑇) ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) |
| 46 | 45 | eqriv 2734 |
. . 3
⊢
(2nd “ 𝑇) = ∪
𝑥 ∈ 𝐴 𝐵 |
| 47 | 8, 46 | eqtr3i 2767 |
. 2
⊢ ran
(2nd ↾ 𝑇)
= ∪ 𝑥 ∈ 𝐴 𝐵 |
| 48 | | df-fo 6567 |
. 2
⊢
((2nd ↾ 𝑇):𝑇–onto→∪ 𝑥 ∈ 𝐴 𝐵 ↔ ((2nd ↾ 𝑇) Fn 𝑇 ∧ ran (2nd ↾ 𝑇) = ∪ 𝑥 ∈ 𝐴 𝐵)) |
| 49 | 7, 47, 48 | mpbir2an 711 |
1
⊢
(2nd ↾ 𝑇):𝑇–onto→∪ 𝑥 ∈ 𝐴 𝐵 |