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