Step | Hyp | Ref
| Expression |
1 | | snmg 3477 |
. . 3
⊢ (A ∈ 𝑉 → ∃x x ∈ {A}) |
2 | | fo2ndresm 5731 |
. . 3
⊢ (∃x x ∈ {A} → (2nd ↾ ({A} × B)):({A} ×
B)–onto→B) |
3 | 1, 2 | syl 14 |
. 2
⊢ (A ∈ 𝑉 → (2nd ↾
({A} × B)):({A} ×
B)–onto→B) |
4 | | moeq 2710 |
. . . . . 6
⊢ ∃*x x = 〈A,
y〉 |
5 | 4 | moani 1967 |
. . . . 5
⊢ ∃*x(y ∈ B ∧ x = 〈A,
y〉) |
6 | | vex 2554 |
. . . . . . . 8
⊢ y ∈
V |
7 | 6 | brres 4561 |
. . . . . . 7
⊢ (x(2nd ↾ ({A} × B))y ↔
(x2nd y ∧ x ∈ ({A} × B))) |
8 | | fo2nd 5727 |
. . . . . . . . . . 11
⊢
2nd :V–onto→V |
9 | | fofn 5051 |
. . . . . . . . . . 11
⊢
(2nd :V–onto→V → 2nd Fn V) |
10 | 8, 9 | ax-mp 7 |
. . . . . . . . . 10
⊢
2nd Fn V |
11 | | vex 2554 |
. . . . . . . . . 10
⊢ x ∈
V |
12 | | fnbrfvb 5157 |
. . . . . . . . . 10
⊢
((2nd Fn V ∧ x ∈ V) →
((2nd ‘x) = y ↔ x2nd y)) |
13 | 10, 11, 12 | mp2an 402 |
. . . . . . . . 9
⊢
((2nd ‘x) =
y ↔ x2nd y) |
14 | 13 | anbi1i 431 |
. . . . . . . 8
⊢
(((2nd ‘x) =
y ∧
x ∈
({A} × B)) ↔ (x2nd y ∧ x ∈ ({A} × B))) |
15 | | elxp7 5739 |
. . . . . . . . . . 11
⊢ (x ∈ ({A} × B)
↔ (x ∈ (V × V) ∧
((1st ‘x) ∈ {A} ∧ (2nd ‘x) ∈ B))) |
16 | | eleq1 2097 |
. . . . . . . . . . . . . . 15
⊢
((2nd ‘x) =
y → ((2nd ‘x) ∈ B ↔ y ∈ B)) |
17 | 16 | biimpa 280 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘x) =
y ∧
(2nd ‘x) ∈ B) →
y ∈
B) |
18 | 17 | adantrl 447 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘x) =
y ∧
((1st ‘x) ∈ {A} ∧ (2nd ‘x) ∈ B)) → y
∈ B) |
19 | 18 | adantrl 447 |
. . . . . . . . . . . 12
⊢
(((2nd ‘x) =
y ∧
(x ∈ (V
× V) ∧ ((1st ‘x) ∈ {A} ∧
(2nd ‘x) ∈ B))) →
y ∈
B) |
20 | | elsni 3391 |
. . . . . . . . . . . . . 14
⊢
((1st ‘x) ∈ {A} →
(1st ‘x) = A) |
21 | | eqopi 5740 |
. . . . . . . . . . . . . . . 16
⊢
((x ∈ (V × V) ∧
((1st ‘x) = A ∧ (2nd
‘x) = y)) → x =
〈A, y〉) |
22 | 21 | ancom2s 500 |
. . . . . . . . . . . . . . 15
⊢
((x ∈ (V × V) ∧
((2nd ‘x) = y ∧ (1st
‘x) = A)) → x =
〈A, y〉) |
23 | 22 | an12s 499 |
. . . . . . . . . . . . . 14
⊢
(((2nd ‘x) =
y ∧
(x ∈ (V
× V) ∧ (1st ‘x) = A)) →
x = 〈A, y〉) |
24 | 20, 23 | sylanr2 385 |
. . . . . . . . . . . . 13
⊢
(((2nd ‘x) =
y ∧
(x ∈ (V
× V) ∧ (1st ‘x) ∈ {A})) → x =
〈A, y〉) |
25 | 24 | adantrrr 456 |
. . . . . . . . . . . 12
⊢
(((2nd ‘x) =
y ∧
(x ∈ (V
× V) ∧ ((1st ‘x) ∈ {A} ∧
(2nd ‘x) ∈ B))) →
x = 〈A, y〉) |
26 | 19, 25 | jca 290 |
. . . . . . . . . . 11
⊢
(((2nd ‘x) =
y ∧
(x ∈ (V
× V) ∧ ((1st ‘x) ∈ {A} ∧
(2nd ‘x) ∈ B))) →
(y ∈
B ∧
x = 〈A, y〉)) |
27 | 15, 26 | sylan2b 271 |
. . . . . . . . . 10
⊢
(((2nd ‘x) =
y ∧
x ∈
({A} × B)) → (y
∈ B ∧ x =
〈A, y〉)) |
28 | 27 | adantl 262 |
. . . . . . . . 9
⊢
((A ∈ 𝑉 ∧
((2nd ‘x) = y ∧ x ∈ ({A} × B)))
→ (y ∈ B ∧ x =
〈A, y〉)) |
29 | | fveq2 5121 |
. . . . . . . . . . . 12
⊢ (x = 〈A,
y〉 → (2nd
‘x) = (2nd
‘〈A, y〉)) |
30 | | op2ndg 5720 |
. . . . . . . . . . . . 13
⊢
((A ∈ 𝑉 ∧ y ∈ V) →
(2nd ‘〈A, y〉) = y) |
31 | 6, 30 | mpan2 401 |
. . . . . . . . . . . 12
⊢ (A ∈ 𝑉 → (2nd
‘〈A, y〉) = y) |
32 | 29, 31 | sylan9eqr 2091 |
. . . . . . . . . . 11
⊢
((A ∈ 𝑉 ∧ x = 〈A,
y〉) → (2nd
‘x) = y) |
33 | 32 | adantrl 447 |
. . . . . . . . . 10
⊢
((A ∈ 𝑉 ∧
(y ∈
B ∧
x = 〈A, y〉))
→ (2nd ‘x) = y) |
34 | | simprr 484 |
. . . . . . . . . . 11
⊢
((A ∈ 𝑉 ∧
(y ∈
B ∧
x = 〈A, y〉))
→ x = 〈A, y〉) |
35 | | snidg 3392 |
. . . . . . . . . . . . 13
⊢ (A ∈ 𝑉 → A ∈ {A}) |
36 | 35 | adantr 261 |
. . . . . . . . . . . 12
⊢
((A ∈ 𝑉 ∧
(y ∈
B ∧
x = 〈A, y〉))
→ A ∈ {A}) |
37 | | simprl 483 |
. . . . . . . . . . . 12
⊢
((A ∈ 𝑉 ∧
(y ∈
B ∧
x = 〈A, y〉))
→ y ∈ B) |
38 | | opelxpi 4319 |
. . . . . . . . . . . 12
⊢
((A ∈ {A} ∧ y ∈ B) →
〈A, y〉 ∈
({A} × B)) |
39 | 36, 37, 38 | syl2anc 391 |
. . . . . . . . . . 11
⊢
((A ∈ 𝑉 ∧
(y ∈
B ∧
x = 〈A, y〉))
→ 〈A, y〉 ∈
({A} × B)) |
40 | 34, 39 | eqeltrd 2111 |
. . . . . . . . . 10
⊢
((A ∈ 𝑉 ∧
(y ∈
B ∧
x = 〈A, y〉))
→ x ∈ ({A} ×
B)) |
41 | 33, 40 | jca 290 |
. . . . . . . . 9
⊢
((A ∈ 𝑉 ∧
(y ∈
B ∧
x = 〈A, y〉))
→ ((2nd ‘x) =
y ∧
x ∈
({A} × B))) |
42 | 28, 41 | impbida 528 |
. . . . . . . 8
⊢ (A ∈ 𝑉 → (((2nd
‘x) = y ∧ x ∈ ({A} × B))
↔ (y ∈ B ∧ x =
〈A, y〉))) |
43 | 14, 42 | syl5bbr 183 |
. . . . . . 7
⊢ (A ∈ 𝑉 → ((x2nd y ∧ x ∈ ({A} × B))
↔ (y ∈ B ∧ x =
〈A, y〉))) |
44 | 7, 43 | syl5bb 181 |
. . . . . 6
⊢ (A ∈ 𝑉 → (x(2nd ↾ ({A} × B))y ↔
(y ∈
B ∧
x = 〈A, y〉))) |
45 | 44 | mobidv 1933 |
. . . . 5
⊢ (A ∈ 𝑉 → (∃*x x(2nd ↾ ({A} × B))y ↔
∃*x(y ∈ B ∧ x =
〈A, y〉))) |
46 | 5, 45 | mpbiri 157 |
. . . 4
⊢ (A ∈ 𝑉 → ∃*x x(2nd ↾ ({A} × B))y) |
47 | 46 | alrimiv 1751 |
. . 3
⊢ (A ∈ 𝑉 → ∀y∃*x x(2nd ↾ ({A} × B))y) |
48 | | funcnv2 4902 |
. . 3
⊢ (Fun
◡(2nd ↾ ({A} × B))
↔ ∀y∃*x x(2nd ↾ ({A} × B))y) |
49 | 47, 48 | sylibr 137 |
. 2
⊢ (A ∈ 𝑉 → Fun ◡(2nd ↾ ({A} × B))) |
50 | | dff1o3 5075 |
. 2
⊢
((2nd ↾ ({A}
× B)):({A} × B)–1-1-onto→B ↔
((2nd ↾ ({A} ×
B)):({A} × B)–onto→B ∧ Fun ◡(2nd ↾ ({A} × B)))) |
51 | 3, 49, 50 | sylanbrc 394 |
1
⊢ (A ∈ 𝑉 → (2nd ↾
({A} × B)):({A} ×
B)–1-1-onto→B) |