Step | Hyp | Ref
| Expression |
1 | | xpsfrnel2 16611 |
. . . . . 6
⊢ (◡({𝑥} +𝑐 {𝑦}) ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
2 | 1 | biimpri 220 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ◡({𝑥} +𝑐 {𝑦}) ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)) |
3 | 2 | rgen2 3157 |
. . . 4
⊢
∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 ◡({𝑥} +𝑐 {𝑦}) ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) |
4 | | xpsff1o.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ ◡({𝑥} +𝑐 {𝑦})) |
5 | 4 | fmpt2 7517 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 ◡({𝑥} +𝑐 {𝑦}) ∈ X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ 𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)) |
6 | 3, 5 | mpbi 222 |
. . 3
⊢ 𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) |
7 | | 1st2nd2 7484 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 × 𝐵) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
8 | 7 | fveq2d 6450 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘𝑧) = (𝐹‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
9 | | df-ov 6925 |
. . . . . . . 8
⊢
((1st ‘𝑧)𝐹(2nd ‘𝑧)) = (𝐹‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
10 | | xp1st 7477 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (1st ‘𝑧) ∈ 𝐴) |
11 | | xp2nd 7478 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
12 | 4 | xpsfval 16613 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = ◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})) |
13 | 10, 11, 12 | syl2anc 579 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 × 𝐵) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = ◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})) |
14 | 9, 13 | syl5eqr 2828 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) = ◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})) |
15 | 8, 14 | eqtrd 2814 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘𝑧) = ◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})) |
16 | | 1st2nd2 7484 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝐴 × 𝐵) → 𝑤 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
17 | 16 | fveq2d 6450 |
. . . . . . 7
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘𝑤) = (𝐹‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) |
18 | | df-ov 6925 |
. . . . . . . 8
⊢
((1st ‘𝑤)𝐹(2nd ‘𝑤)) = (𝐹‘〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
19 | | xp1st 7477 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (1st ‘𝑤) ∈ 𝐴) |
20 | | xp2nd 7478 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (2nd ‘𝑤) ∈ 𝐵) |
21 | 4 | xpsfval 16613 |
. . . . . . . . 9
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (2nd ‘𝑤) ∈ 𝐵) → ((1st ‘𝑤)𝐹(2nd ‘𝑤)) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})) |
22 | 19, 20, 21 | syl2anc 579 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝐴 × 𝐵) → ((1st ‘𝑤)𝐹(2nd ‘𝑤)) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})) |
23 | 18, 22 | syl5eqr 2828 |
. . . . . . 7
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘〈(1st ‘𝑤), (2nd ‘𝑤)〉) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})) |
24 | 17, 23 | eqtrd 2814 |
. . . . . 6
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘𝑤) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})) |
25 | 15, 24 | eqeqan12d 2794 |
. . . . 5
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)}) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)}))) |
26 | | fveq1 6445 |
. . . . . . . 8
⊢ (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)}) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)}) → (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})‘∅)
= (◡({(1st ‘𝑤)} +𝑐
{(2nd ‘𝑤)})‘∅)) |
27 | | fvex 6459 |
. . . . . . . . 9
⊢
(1st ‘𝑧) ∈ V |
28 | | xpsc0 16606 |
. . . . . . . . 9
⊢
((1st ‘𝑧) ∈ V → (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})‘∅)
= (1st ‘𝑧)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . 8
⊢ (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})‘∅)
= (1st ‘𝑧) |
30 | | fvex 6459 |
. . . . . . . . 9
⊢
(1st ‘𝑤) ∈ V |
31 | | xpsc0 16606 |
. . . . . . . . 9
⊢
((1st ‘𝑤) ∈ V → (◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})‘∅)
= (1st ‘𝑤)) |
32 | 30, 31 | ax-mp 5 |
. . . . . . . 8
⊢ (◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})‘∅)
= (1st ‘𝑤) |
33 | 26, 29, 32 | 3eqtr3g 2837 |
. . . . . . 7
⊢ (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)}) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)}) →
(1st ‘𝑧) =
(1st ‘𝑤)) |
34 | | fveq1 6445 |
. . . . . . . 8
⊢ (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)}) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)}) → (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})‘1o) = (◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})‘1o)) |
35 | | fvex 6459 |
. . . . . . . . 9
⊢
(2nd ‘𝑧) ∈ V |
36 | | xpsc1 16607 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) ∈ V → (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})‘1o) = (2nd
‘𝑧)) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . 8
⊢ (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)})‘1o) = (2nd
‘𝑧) |
38 | | fvex 6459 |
. . . . . . . . 9
⊢
(2nd ‘𝑤) ∈ V |
39 | | xpsc1 16607 |
. . . . . . . . 9
⊢
((2nd ‘𝑤) ∈ V → (◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})‘1o) = (2nd
‘𝑤)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . 8
⊢ (◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)})‘1o) = (2nd
‘𝑤) |
41 | 34, 37, 40 | 3eqtr3g 2837 |
. . . . . . 7
⊢ (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)}) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)}) →
(2nd ‘𝑧) =
(2nd ‘𝑤)) |
42 | 33, 41 | opeq12d 4644 |
. . . . . 6
⊢ (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)}) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)}) →
〈(1st ‘𝑧), (2nd ‘𝑧)〉 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
43 | 7, 16 | eqeqan12d 2794 |
. . . . . 6
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → (𝑧 = 𝑤 ↔ 〈(1st ‘𝑧), (2nd ‘𝑧)〉 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉)) |
44 | 42, 43 | syl5ibr 238 |
. . . . 5
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → (◡({(1st ‘𝑧)} +𝑐 {(2nd
‘𝑧)}) = ◡({(1st ‘𝑤)} +𝑐 {(2nd
‘𝑤)}) → 𝑧 = 𝑤)) |
45 | 25, 44 | sylbid 232 |
. . . 4
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
46 | 45 | rgen2 3157 |
. . 3
⊢
∀𝑧 ∈
(𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤) |
47 | | dff13 6784 |
. . 3
⊢ (𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ ∀𝑧 ∈ (𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
48 | 6, 46, 47 | mpbir2an 701 |
. 2
⊢ 𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) |
49 | | xpsfrnel 16609 |
. . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝑧 Fn 2o ∧ (𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵)) |
50 | 49 | simp2bi 1137 |
. . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → (𝑧‘∅) ∈ 𝐴) |
51 | 49 | simp3bi 1138 |
. . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → (𝑧‘1o) ∈ 𝐵) |
52 | 4 | xpsfval 16613 |
. . . . . . 7
⊢ (((𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵) → ((𝑧‘∅)𝐹(𝑧‘1o)) = ◡({(𝑧‘∅)} +𝑐
{(𝑧‘1o)})) |
53 | 50, 51, 52 | syl2anc 579 |
. . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → ((𝑧‘∅)𝐹(𝑧‘1o)) = ◡({(𝑧‘∅)} +𝑐
{(𝑧‘1o)})) |
54 | | ixpfn 8200 |
. . . . . . 7
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → 𝑧 Fn 2o) |
55 | | xpsfeq 16610 |
. . . . . . 7
⊢ (𝑧 Fn 2o → ◡({(𝑧‘∅)} +𝑐
{(𝑧‘1o)})
= 𝑧) |
56 | 54, 55 | syl 17 |
. . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → ◡({(𝑧‘∅)} +𝑐
{(𝑧‘1o)})
= 𝑧) |
57 | 53, 56 | eqtr2d 2815 |
. . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → 𝑧 = ((𝑧‘∅)𝐹(𝑧‘1o))) |
58 | | rspceov 6968 |
. . . . 5
⊢ (((𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵 ∧ 𝑧 = ((𝑧‘∅)𝐹(𝑧‘1o))) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏)) |
59 | 50, 51, 57, 58 | syl3anc 1439 |
. . . 4
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏)) |
60 | 59 | rgen 3104 |
. . 3
⊢
∀𝑧 ∈
X 𝑘
∈ 2o if(𝑘 =
∅, 𝐴, 𝐵)∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏) |
61 | | foov 7085 |
. . 3
⊢ (𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ ∀𝑧 ∈ X 𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏))) |
62 | 6, 60, 61 | mpbir2an 701 |
. 2
⊢ 𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) |
63 | | df-f1o 6142 |
. 2
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ 𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵))) |
64 | 48, 62, 63 | mpbir2an 701 |
1
⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) |