Step | Hyp | Ref
| Expression |
1 | | xpsfrnel2 12764 |
. . . . . 6
⊢
({⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
2 | 1 | biimpri 133 |
. . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵)) |
3 | 2 | rgen2 2563 |
. . . 4
⊢
∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) |
4 | | xpsff1o.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩}) |
5 | 4 | fmpo 6201 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐵 {⟨∅, 𝑥⟩, ⟨1o, 𝑦⟩} ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ 𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)) |
6 | 3, 5 | mpbi 145 |
. . 3
⊢ 𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) |
7 | | 1st2nd2 6175 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 × 𝐵) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩) |
8 | 7 | fveq2d 5519 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘𝑧) = (𝐹‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)) |
9 | | df-ov 5877 |
. . . . . . . 8
⊢
((1st ‘𝑧)𝐹(2nd ‘𝑧)) = (𝐹‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩) |
10 | | xp1st 6165 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (1st ‘𝑧) ∈ 𝐴) |
11 | | xp2nd 6166 |
. . . . . . . . 9
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
12 | 4 | xpsfval 12766 |
. . . . . . . . 9
⊢
(((1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = {⟨∅, (1st
‘𝑧)⟩,
⟨1o, (2nd ‘𝑧)⟩}) |
13 | 10, 11, 12 | syl2anc 411 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐴 × 𝐵) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = {⟨∅, (1st
‘𝑧)⟩,
⟨1o, (2nd ‘𝑧)⟩}) |
14 | 9, 13 | eqtr3id 2224 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩) = {⟨∅,
(1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩}) |
15 | 8, 14 | eqtrd 2210 |
. . . . . 6
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (𝐹‘𝑧) = {⟨∅, (1st
‘𝑧)⟩,
⟨1o, (2nd ‘𝑧)⟩}) |
16 | | 1st2nd2 6175 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝐴 × 𝐵) → 𝑤 = ⟨(1st ‘𝑤), (2nd ‘𝑤)⟩) |
17 | 16 | fveq2d 5519 |
. . . . . . 7
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘𝑤) = (𝐹‘⟨(1st ‘𝑤), (2nd ‘𝑤)⟩)) |
18 | | df-ov 5877 |
. . . . . . . 8
⊢
((1st ‘𝑤)𝐹(2nd ‘𝑤)) = (𝐹‘⟨(1st ‘𝑤), (2nd ‘𝑤)⟩) |
19 | | xp1st 6165 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (1st ‘𝑤) ∈ 𝐴) |
20 | | xp2nd 6166 |
. . . . . . . . 9
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (2nd ‘𝑤) ∈ 𝐵) |
21 | 4 | xpsfval 12766 |
. . . . . . . . 9
⊢
(((1st ‘𝑤) ∈ 𝐴 ∧ (2nd ‘𝑤) ∈ 𝐵) → ((1st ‘𝑤)𝐹(2nd ‘𝑤)) = {⟨∅, (1st
‘𝑤)⟩,
⟨1o, (2nd ‘𝑤)⟩}) |
22 | 19, 20, 21 | syl2anc 411 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝐴 × 𝐵) → ((1st ‘𝑤)𝐹(2nd ‘𝑤)) = {⟨∅, (1st
‘𝑤)⟩,
⟨1o, (2nd ‘𝑤)⟩}) |
23 | 18, 22 | eqtr3id 2224 |
. . . . . . 7
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘⟨(1st ‘𝑤), (2nd ‘𝑤)⟩) = {⟨∅,
(1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩}) |
24 | 17, 23 | eqtrd 2210 |
. . . . . 6
⊢ (𝑤 ∈ (𝐴 × 𝐵) → (𝐹‘𝑤) = {⟨∅, (1st
‘𝑤)⟩,
⟨1o, (2nd ‘𝑤)⟩}) |
25 | 15, 24 | eqeqan12d 2193 |
. . . . 5
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ {⟨∅, (1st
‘𝑧)⟩,
⟨1o, (2nd ‘𝑧)⟩} = {⟨∅, (1st
‘𝑤)⟩,
⟨1o, (2nd ‘𝑤)⟩})) |
26 | | fveq1 5514 |
. . . . . . . 8
⊢
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩} =
{⟨∅, (1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩} →
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩}‘∅) = ({⟨∅,
(1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩}‘∅)) |
27 | | 1stexg 6167 |
. . . . . . . . . 10
⊢ (𝑧 ∈ V → (1st
‘𝑧) ∈
V) |
28 | 27 | elv 2741 |
. . . . . . . . 9
⊢
(1st ‘𝑧) ∈ V |
29 | | fvpr0o 12759 |
. . . . . . . . 9
⊢
((1st ‘𝑧) ∈ V → ({⟨∅,
(1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩}‘∅) = (1st
‘𝑧)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . 8
⊢
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩}‘∅) = (1st
‘𝑧) |
31 | | 1stexg 6167 |
. . . . . . . . . 10
⊢ (𝑤 ∈ V → (1st
‘𝑤) ∈
V) |
32 | 31 | elv 2741 |
. . . . . . . . 9
⊢
(1st ‘𝑤) ∈ V |
33 | | fvpr0o 12759 |
. . . . . . . . 9
⊢
((1st ‘𝑤) ∈ V → ({⟨∅,
(1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩}‘∅) = (1st
‘𝑤)) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . 8
⊢
({⟨∅, (1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩}‘∅) = (1st
‘𝑤) |
35 | 26, 30, 34 | 3eqtr3g 2233 |
. . . . . . 7
⊢
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩} =
{⟨∅, (1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩} →
(1st ‘𝑧) =
(1st ‘𝑤)) |
36 | | fveq1 5514 |
. . . . . . . 8
⊢
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩} =
{⟨∅, (1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩} →
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩}‘1o) =
({⟨∅, (1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩}‘1o)) |
37 | | 2ndexg 6168 |
. . . . . . . . . 10
⊢ (𝑧 ∈ V → (2nd
‘𝑧) ∈
V) |
38 | 37 | elv 2741 |
. . . . . . . . 9
⊢
(2nd ‘𝑧) ∈ V |
39 | | fvpr1o 12760 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) ∈ V → ({⟨∅,
(1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩}‘1o) =
(2nd ‘𝑧)) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . 8
⊢
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩}‘1o) =
(2nd ‘𝑧) |
41 | | 2ndexg 6168 |
. . . . . . . . . 10
⊢ (𝑤 ∈ V → (2nd
‘𝑤) ∈
V) |
42 | 41 | elv 2741 |
. . . . . . . . 9
⊢
(2nd ‘𝑤) ∈ V |
43 | | fvpr1o 12760 |
. . . . . . . . 9
⊢
((2nd ‘𝑤) ∈ V → ({⟨∅,
(1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩}‘1o) =
(2nd ‘𝑤)) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . 8
⊢
({⟨∅, (1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩}‘1o) =
(2nd ‘𝑤) |
45 | 36, 40, 44 | 3eqtr3g 2233 |
. . . . . . 7
⊢
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩} =
{⟨∅, (1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩} →
(2nd ‘𝑧) =
(2nd ‘𝑤)) |
46 | 35, 45 | opeq12d 3786 |
. . . . . 6
⊢
({⟨∅, (1st ‘𝑧)⟩, ⟨1o, (2nd
‘𝑧)⟩} =
{⟨∅, (1st ‘𝑤)⟩, ⟨1o, (2nd
‘𝑤)⟩} →
⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ = ⟨(1st ‘𝑤), (2nd ‘𝑤)⟩) |
47 | 7, 16 | eqeqan12d 2193 |
. . . . . 6
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → (𝑧 = 𝑤 ↔ ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ = ⟨(1st
‘𝑤), (2nd
‘𝑤)⟩)) |
48 | 46, 47 | imbitrrid 156 |
. . . . 5
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ({⟨∅, (1st
‘𝑧)⟩,
⟨1o, (2nd ‘𝑧)⟩} = {⟨∅, (1st
‘𝑤)⟩,
⟨1o, (2nd ‘𝑤)⟩} → 𝑧 = 𝑤)) |
49 | 25, 48 | sylbid 150 |
. . . 4
⊢ ((𝑧 ∈ (𝐴 × 𝐵) ∧ 𝑤 ∈ (𝐴 × 𝐵)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
50 | 49 | rgen2 2563 |
. . 3
⊢
∀𝑧 ∈
(𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤) |
51 | | dff13 5768 |
. . 3
⊢ (𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ ∀𝑧 ∈ (𝐴 × 𝐵)∀𝑤 ∈ (𝐴 × 𝐵)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
52 | 6, 50, 51 | mpbir2an 942 |
. 2
⊢ 𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) |
53 | | xpsfrnel 12762 |
. . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝑧 Fn 2o ∧ (𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵)) |
54 | 53 | simp2bi 1013 |
. . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → (𝑧‘∅) ∈ 𝐴) |
55 | 53 | simp3bi 1014 |
. . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → (𝑧‘1o) ∈ 𝐵) |
56 | 4 | xpsfval 12766 |
. . . . . . 7
⊢ (((𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵) → ((𝑧‘∅)𝐹(𝑧‘1o)) = {⟨∅,
(𝑧‘∅)⟩,
⟨1o, (𝑧‘1o)⟩}) |
57 | 54, 55, 56 | syl2anc 411 |
. . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → ((𝑧‘∅)𝐹(𝑧‘1o)) = {⟨∅,
(𝑧‘∅)⟩,
⟨1o, (𝑧‘1o)⟩}) |
58 | | ixpfn 6703 |
. . . . . . 7
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → 𝑧 Fn 2o) |
59 | | xpsfeq 12763 |
. . . . . . 7
⊢ (𝑧 Fn 2o →
{⟨∅, (𝑧‘∅)⟩, ⟨1o,
(𝑧‘1o)⟩} = 𝑧) |
60 | 58, 59 | syl 14 |
. . . . . 6
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → {⟨∅, (𝑧‘∅)⟩,
⟨1o, (𝑧‘1o)⟩} = 𝑧) |
61 | 57, 60 | eqtr2d 2211 |
. . . . 5
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → 𝑧 = ((𝑧‘∅)𝐹(𝑧‘1o))) |
62 | | rspceov 5916 |
. . . . 5
⊢ (((𝑧‘∅) ∈ 𝐴 ∧ (𝑧‘1o) ∈ 𝐵 ∧ 𝑧 = ((𝑧‘∅)𝐹(𝑧‘1o))) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏)) |
63 | 54, 55, 61, 62 | syl3anc 1238 |
. . . 4
⊢ (𝑧 ∈ X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏)) |
64 | 63 | rgen 2530 |
. . 3
⊢
∀𝑧 ∈
X 𝑘
∈ 2o if(𝑘 =
∅, 𝐴, 𝐵)∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏) |
65 | | foov 6020 |
. . 3
⊢ (𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)⟶X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ ∀𝑧 ∈ X 𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵)∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎𝐹𝑏))) |
66 | 6, 64, 65 | mpbir2an 942 |
. 2
⊢ 𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) |
67 | | df-f1o 5223 |
. 2
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) ↔ (𝐹:(𝐴 × 𝐵)–1-1→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵) ∧ 𝐹:(𝐴 × 𝐵)–onto→X𝑘 ∈ 2o if(𝑘 = ∅, 𝐴, 𝐵))) |
68 | 52, 66, 67 | mpbir2an 942 |
1
⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→X𝑘 ∈
2o if(𝑘 =
∅, 𝐴, 𝐵) |