Step | Hyp | Ref
| Expression |
1 | | snmg 3677 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∃𝑥 𝑥 ∈ {𝐴}) |
2 | | fo2ndresm 6110 |
. . 3
⊢
(∃𝑥 𝑥 ∈ {𝐴} → (2nd ↾ ({𝐴} × 𝐵)):({𝐴} × 𝐵)–onto→𝐵) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝐴 ∈ 𝑉 → (2nd ↾ ({𝐴} × 𝐵)):({𝐴} × 𝐵)–onto→𝐵) |
4 | | moeq 2887 |
. . . . . 6
⊢
∃*𝑥 𝑥 = 〈𝐴, 𝑦〉 |
5 | 4 | moani 2076 |
. . . . 5
⊢
∃*𝑥(𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉) |
6 | | vex 2715 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
7 | 6 | brres 4872 |
. . . . . . 7
⊢ (𝑥(2nd ↾ ({𝐴} × 𝐵))𝑦 ↔ (𝑥2nd 𝑦 ∧ 𝑥 ∈ ({𝐴} × 𝐵))) |
8 | | fo2nd 6106 |
. . . . . . . . . . 11
⊢
2nd :V–onto→V |
9 | | fofn 5394 |
. . . . . . . . . . 11
⊢
(2nd :V–onto→V → 2nd Fn V) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . 10
⊢
2nd Fn V |
11 | | vex 2715 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
12 | | fnbrfvb 5509 |
. . . . . . . . . 10
⊢
((2nd Fn V ∧ 𝑥 ∈ V) → ((2nd
‘𝑥) = 𝑦 ↔ 𝑥2nd 𝑦)) |
13 | 10, 11, 12 | mp2an 423 |
. . . . . . . . 9
⊢
((2nd ‘𝑥) = 𝑦 ↔ 𝑥2nd 𝑦) |
14 | 13 | anbi1i 454 |
. . . . . . . 8
⊢
(((2nd ‘𝑥) = 𝑦 ∧ 𝑥 ∈ ({𝐴} × 𝐵)) ↔ (𝑥2nd 𝑦 ∧ 𝑥 ∈ ({𝐴} × 𝐵))) |
15 | | elxp7 6118 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ({𝐴} × 𝐵) ↔ (𝑥 ∈ (V × V) ∧ ((1st
‘𝑥) ∈ {𝐴} ∧ (2nd
‘𝑥) ∈ 𝐵))) |
16 | | eleq1 2220 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘𝑥) = 𝑦 → ((2nd ‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
17 | 16 | biimpa 294 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘𝑥) = 𝑦 ∧ (2nd ‘𝑥) ∈ 𝐵) → 𝑦 ∈ 𝐵) |
18 | 17 | adantrl 470 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝑥) = 𝑦 ∧ ((1st ‘𝑥) ∈ {𝐴} ∧ (2nd ‘𝑥) ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
19 | 18 | adantrl 470 |
. . . . . . . . . . . 12
⊢
(((2nd ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ ((1st
‘𝑥) ∈ {𝐴} ∧ (2nd
‘𝑥) ∈ 𝐵))) → 𝑦 ∈ 𝐵) |
20 | | elsni 3578 |
. . . . . . . . . . . . . 14
⊢
((1st ‘𝑥) ∈ {𝐴} → (1st ‘𝑥) = 𝐴) |
21 | | eqopi 6120 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (V × V) ∧
((1st ‘𝑥)
= 𝐴 ∧ (2nd
‘𝑥) = 𝑦)) → 𝑥 = 〈𝐴, 𝑦〉) |
22 | 21 | ancom2s 556 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (V × V) ∧
((2nd ‘𝑥)
= 𝑦 ∧ (1st
‘𝑥) = 𝐴)) → 𝑥 = 〈𝐴, 𝑦〉) |
23 | 22 | an12s 555 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ (1st
‘𝑥) = 𝐴)) → 𝑥 = 〈𝐴, 𝑦〉) |
24 | 20, 23 | sylanr2 403 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ (1st
‘𝑥) ∈ {𝐴})) → 𝑥 = 〈𝐴, 𝑦〉) |
25 | 24 | adantrrr 479 |
. . . . . . . . . . . 12
⊢
(((2nd ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ ((1st
‘𝑥) ∈ {𝐴} ∧ (2nd
‘𝑥) ∈ 𝐵))) → 𝑥 = 〈𝐴, 𝑦〉) |
26 | 19, 25 | jca 304 |
. . . . . . . . . . 11
⊢
(((2nd ‘𝑥) = 𝑦 ∧ (𝑥 ∈ (V × V) ∧ ((1st
‘𝑥) ∈ {𝐴} ∧ (2nd
‘𝑥) ∈ 𝐵))) → (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) |
27 | 15, 26 | sylan2b 285 |
. . . . . . . . . 10
⊢
(((2nd ‘𝑥) = 𝑦 ∧ 𝑥 ∈ ({𝐴} × 𝐵)) → (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) |
28 | 27 | adantl 275 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ ((2nd ‘𝑥) = 𝑦 ∧ 𝑥 ∈ ({𝐴} × 𝐵))) → (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) |
29 | | fveq2 5468 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈𝐴, 𝑦〉 → (2nd ‘𝑥) = (2nd
‘〈𝐴, 𝑦〉)) |
30 | | op2ndg 6099 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑦 ∈ V) → (2nd
‘〈𝐴, 𝑦〉) = 𝑦) |
31 | 6, 30 | mpan2 422 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (2nd ‘〈𝐴, 𝑦〉) = 𝑦) |
32 | 29, 31 | sylan9eqr 2212 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑥 = 〈𝐴, 𝑦〉) → (2nd ‘𝑥) = 𝑦) |
33 | 32 | adantrl 470 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) → (2nd ‘𝑥) = 𝑦) |
34 | | simprr 522 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) → 𝑥 = 〈𝐴, 𝑦〉) |
35 | | snidg 3589 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴}) |
36 | 35 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) → 𝐴 ∈ {𝐴}) |
37 | | simprl 521 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) → 𝑦 ∈ 𝐵) |
38 | | opelxpi 4618 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ {𝐴} ∧ 𝑦 ∈ 𝐵) → 〈𝐴, 𝑦〉 ∈ ({𝐴} × 𝐵)) |
39 | 36, 37, 38 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) → 〈𝐴, 𝑦〉 ∈ ({𝐴} × 𝐵)) |
40 | 34, 39 | eqeltrd 2234 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) → 𝑥 ∈ ({𝐴} × 𝐵)) |
41 | 33, 40 | jca 304 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉)) → ((2nd ‘𝑥) = 𝑦 ∧ 𝑥 ∈ ({𝐴} × 𝐵))) |
42 | 28, 41 | impbida 586 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (((2nd ‘𝑥) = 𝑦 ∧ 𝑥 ∈ ({𝐴} × 𝐵)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉))) |
43 | 14, 42 | bitr3id 193 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → ((𝑥2nd 𝑦 ∧ 𝑥 ∈ ({𝐴} × 𝐵)) ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉))) |
44 | 7, 43 | syl5bb 191 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑥(2nd ↾ ({𝐴} × 𝐵))𝑦 ↔ (𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉))) |
45 | 44 | mobidv 2042 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∃*𝑥 𝑥(2nd ↾ ({𝐴} × 𝐵))𝑦 ↔ ∃*𝑥(𝑦 ∈ 𝐵 ∧ 𝑥 = 〈𝐴, 𝑦〉))) |
46 | 5, 45 | mpbiri 167 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∃*𝑥 𝑥(2nd ↾ ({𝐴} × 𝐵))𝑦) |
47 | 46 | alrimiv 1854 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∀𝑦∃*𝑥 𝑥(2nd ↾ ({𝐴} × 𝐵))𝑦) |
48 | | funcnv2 5230 |
. . 3
⊢ (Fun
◡(2nd ↾ ({𝐴} × 𝐵)) ↔ ∀𝑦∃*𝑥 𝑥(2nd ↾ ({𝐴} × 𝐵))𝑦) |
49 | 47, 48 | sylibr 133 |
. 2
⊢ (𝐴 ∈ 𝑉 → Fun ◡(2nd ↾ ({𝐴} × 𝐵))) |
50 | | dff1o3 5420 |
. 2
⊢
((2nd ↾ ({𝐴} × 𝐵)):({𝐴} × 𝐵)–1-1-onto→𝐵 ↔ ((2nd ↾
({𝐴} × 𝐵)):({𝐴} × 𝐵)–onto→𝐵 ∧ Fun ◡(2nd ↾ ({𝐴} × 𝐵)))) |
51 | 3, 49, 50 | sylanbrc 414 |
1
⊢ (𝐴 ∈ 𝑉 → (2nd ↾ ({𝐴} × 𝐵)):({𝐴} × 𝐵)–1-1-onto→𝐵) |