| Step | Hyp | Ref
| Expression |
| 1 | | rrx2xpref1o.1 |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) |
| 2 | | prex 5437 |
. . . . 5
⊢ {〈1,
𝑥〉, 〈2, 𝑦〉} ∈
V |
| 3 | 1, 2 | fnmpoi 8095 |
. . . 4
⊢ 𝐹 Fn (ℝ ×
ℝ) |
| 4 | | 1st2nd2 8053 |
. . . . . . . . 9
⊢ (𝑧 ∈ (ℝ ×
ℝ) → 𝑧 =
〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 5 | 4 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (𝐹‘𝑧) = (𝐹‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) |
| 6 | | df-ov 7434 |
. . . . . . . 8
⊢
((1st ‘𝑧)𝐹(2nd ‘𝑧)) = (𝐹‘〈(1st ‘𝑧), (2nd ‘𝑧)〉) |
| 7 | 5, 6 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (𝐹‘𝑧) = ((1st ‘𝑧)𝐹(2nd ‘𝑧))) |
| 8 | | xp1st 8046 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (1st ‘𝑧) ∈ ℝ) |
| 9 | | xp2nd 8047 |
. . . . . . . 8
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (2nd ‘𝑧) ∈ ℝ) |
| 10 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑧) → 〈1, 𝑥〉 = 〈1,
(1st ‘𝑧)〉) |
| 11 | 10 | preq1d 4739 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) → {〈1, 𝑥〉, 〈2, 𝑦〉} = {〈1,
(1st ‘𝑧)〉, 〈2, 𝑦〉}) |
| 12 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑧) → 〈2, 𝑦〉 = 〈2,
(2nd ‘𝑧)〉) |
| 13 | 12 | preq2d 4740 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑧) → {〈1,
(1st ‘𝑧)〉, 〈2, 𝑦〉} = {〈1, (1st
‘𝑧)〉, 〈2,
(2nd ‘𝑧)〉}) |
| 14 | | prex 5437 |
. . . . . . . . 9
⊢ {〈1,
(1st ‘𝑧)〉, 〈2, (2nd
‘𝑧)〉} ∈
V |
| 15 | 11, 13, 1, 14 | ovmpo 7593 |
. . . . . . . 8
⊢
(((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈ ℝ)
→ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = {〈1, (1st ‘𝑧)〉, 〈2,
(2nd ‘𝑧)〉}) |
| 16 | 8, 9, 15 | syl2anc 584 |
. . . . . . 7
⊢ (𝑧 ∈ (ℝ ×
ℝ) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = {〈1, (1st ‘𝑧)〉, 〈2,
(2nd ‘𝑧)〉}) |
| 17 | 7, 16 | eqtrd 2777 |
. . . . . 6
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (𝐹‘𝑧) = {〈1, (1st ‘𝑧)〉, 〈2,
(2nd ‘𝑧)〉}) |
| 18 | | eqid 2737 |
. . . . . . . 8
⊢ {1, 2} =
{1, 2} |
| 19 | | rrx2xpreen.r |
. . . . . . . 8
⊢ 𝑅 = (ℝ ↑m
{1, 2}) |
| 20 | 18, 19 | prelrrx2 48634 |
. . . . . . 7
⊢
(((1st ‘𝑧) ∈ ℝ ∧ (2nd
‘𝑧) ∈ ℝ)
→ {〈1, (1st ‘𝑧)〉, 〈2, (2nd
‘𝑧)〉} ∈
𝑅) |
| 21 | 8, 9, 20 | syl2anc 584 |
. . . . . 6
⊢ (𝑧 ∈ (ℝ ×
ℝ) → {〈1, (1st ‘𝑧)〉, 〈2, (2nd
‘𝑧)〉} ∈
𝑅) |
| 22 | 17, 21 | eqeltrd 2841 |
. . . . 5
⊢ (𝑧 ∈ (ℝ ×
ℝ) → (𝐹‘𝑧) ∈ 𝑅) |
| 23 | 22 | rgen 3063 |
. . . 4
⊢
∀𝑧 ∈
(ℝ × ℝ)(𝐹‘𝑧) ∈ 𝑅 |
| 24 | | ffnfv 7139 |
. . . 4
⊢ (𝐹:(ℝ ×
ℝ)⟶𝑅 ↔
(𝐹 Fn (ℝ ×
ℝ) ∧ ∀𝑧
∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ 𝑅)) |
| 25 | 3, 23, 24 | mpbir2an 711 |
. . 3
⊢ 𝐹:(ℝ ×
ℝ)⟶𝑅 |
| 26 | | opex 5469 |
. . . . . . . 8
⊢ 〈1,
(1st ‘𝑧)〉 ∈ V |
| 27 | | opex 5469 |
. . . . . . . 8
⊢ 〈2,
(2nd ‘𝑧)〉 ∈ V |
| 28 | | opex 5469 |
. . . . . . . 8
⊢ 〈1,
(1st ‘𝑤)〉 ∈ V |
| 29 | | opex 5469 |
. . . . . . . 8
⊢ 〈2,
(2nd ‘𝑤)〉 ∈ V |
| 30 | 26, 27, 28, 29 | preq12b 4850 |
. . . . . . 7
⊢
({〈1, (1st ‘𝑧)〉, 〈2, (2nd
‘𝑧)〉} =
{〈1, (1st ‘𝑤)〉, 〈2, (2nd
‘𝑤)〉} ↔
((〈1, (1st ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉 ∧
〈2, (2nd ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉) ∨
(〈1, (1st ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉 ∧
〈2, (2nd ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉))) |
| 31 | | 1ex 11257 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
| 32 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑧) ∈ V |
| 33 | 31, 32 | opth 5481 |
. . . . . . . . . . 11
⊢ (〈1,
(1st ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉 ↔ (1 =
1 ∧ (1st ‘𝑧) = (1st ‘𝑤))) |
| 34 | 33 | simprbi 496 |
. . . . . . . . . 10
⊢ (〈1,
(1st ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉 →
(1st ‘𝑧) =
(1st ‘𝑤)) |
| 35 | | 2ex 12343 |
. . . . . . . . . . . 12
⊢ 2 ∈
V |
| 36 | | fvex 6919 |
. . . . . . . . . . . 12
⊢
(2nd ‘𝑧) ∈ V |
| 37 | 35, 36 | opth 5481 |
. . . . . . . . . . 11
⊢ (〈2,
(2nd ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉 ↔ (2 =
2 ∧ (2nd ‘𝑧) = (2nd ‘𝑤))) |
| 38 | 37 | simprbi 496 |
. . . . . . . . . 10
⊢ (〈2,
(2nd ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉 →
(2nd ‘𝑧) =
(2nd ‘𝑤)) |
| 39 | 34, 38 | anim12i 613 |
. . . . . . . . 9
⊢
((〈1, (1st ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉 ∧
〈2, (2nd ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉) →
((1st ‘𝑧)
= (1st ‘𝑤)
∧ (2nd ‘𝑧) = (2nd ‘𝑤))) |
| 40 | 39 | a1d 25 |
. . . . . . . 8
⊢
((〈1, (1st ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉 ∧
〈2, (2nd ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉) →
((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤)))) |
| 41 | 31, 32 | opth 5481 |
. . . . . . . . 9
⊢ (〈1,
(1st ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉 ↔ (1 =
2 ∧ (1st ‘𝑧) = (2nd ‘𝑤))) |
| 42 | 35, 36 | opth 5481 |
. . . . . . . . 9
⊢ (〈2,
(2nd ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉 ↔ (2 =
1 ∧ (2nd ‘𝑧) = (1st ‘𝑤))) |
| 43 | | 1ne2 12474 |
. . . . . . . . . . 11
⊢ 1 ≠
2 |
| 44 | | eqneqall 2951 |
. . . . . . . . . . 11
⊢ (1 = 2
→ (1 ≠ 2 → ((𝑧
∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) →
((1st ‘𝑧)
= (1st ‘𝑤)
∧ (2nd ‘𝑧) = (2nd ‘𝑤))))) |
| 45 | 43, 44 | mpi 20 |
. . . . . . . . . 10
⊢ (1 = 2
→ ((𝑧 ∈ (ℝ
× ℝ) ∧ 𝑤
∈ (ℝ × ℝ)) → ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd
‘𝑧) = (2nd
‘𝑤)))) |
| 46 | 45 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((1 = 2
∧ (1st ‘𝑧) = (2nd ‘𝑤)) ∧ (2 = 1 ∧ (2nd
‘𝑧) = (1st
‘𝑤))) → ((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤)))) |
| 47 | 41, 42, 46 | syl2anb 598 |
. . . . . . . 8
⊢
((〈1, (1st ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉 ∧
〈2, (2nd ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉) →
((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤)))) |
| 48 | 40, 47 | jaoi 858 |
. . . . . . 7
⊢
(((〈1, (1st ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉 ∧
〈2, (2nd ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉) ∨
(〈1, (1st ‘𝑧)〉 = 〈2, (2nd
‘𝑤)〉 ∧
〈2, (2nd ‘𝑧)〉 = 〈1, (1st
‘𝑤)〉)) →
((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤)))) |
| 49 | 30, 48 | sylbi 217 |
. . . . . 6
⊢
({〈1, (1st ‘𝑧)〉, 〈2, (2nd
‘𝑧)〉} =
{〈1, (1st ‘𝑤)〉, 〈2, (2nd
‘𝑤)〉} →
((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤)))) |
| 50 | 49 | com12 32 |
. . . . 5
⊢ ((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → ({〈1, (1st ‘𝑧)〉, 〈2,
(2nd ‘𝑧)〉} = {〈1, (1st
‘𝑤)〉, 〈2,
(2nd ‘𝑤)〉} → ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd
‘𝑧) = (2nd
‘𝑤)))) |
| 51 | | 1st2nd2 8053 |
. . . . . . . . 9
⊢ (𝑤 ∈ (ℝ ×
ℝ) → 𝑤 =
〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
| 52 | 51 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑤 ∈ (ℝ ×
ℝ) → (𝐹‘𝑤) = (𝐹‘〈(1st ‘𝑤), (2nd ‘𝑤)〉)) |
| 53 | | df-ov 7434 |
. . . . . . . 8
⊢
((1st ‘𝑤)𝐹(2nd ‘𝑤)) = (𝐹‘〈(1st ‘𝑤), (2nd ‘𝑤)〉) |
| 54 | 52, 53 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑤 ∈ (ℝ ×
ℝ) → (𝐹‘𝑤) = ((1st ‘𝑤)𝐹(2nd ‘𝑤))) |
| 55 | | xp1st 8046 |
. . . . . . . 8
⊢ (𝑤 ∈ (ℝ ×
ℝ) → (1st ‘𝑤) ∈ ℝ) |
| 56 | | xp2nd 8047 |
. . . . . . . 8
⊢ (𝑤 ∈ (ℝ ×
ℝ) → (2nd ‘𝑤) ∈ ℝ) |
| 57 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑥 = (1st ‘𝑤) → 〈1, 𝑥〉 = 〈1,
(1st ‘𝑤)〉) |
| 58 | 57 | preq1d 4739 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑤) → {〈1, 𝑥〉, 〈2, 𝑦〉} = {〈1,
(1st ‘𝑤)〉, 〈2, 𝑦〉}) |
| 59 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑦 = (2nd ‘𝑤) → 〈2, 𝑦〉 = 〈2,
(2nd ‘𝑤)〉) |
| 60 | 59 | preq2d 4740 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑤) → {〈1,
(1st ‘𝑤)〉, 〈2, 𝑦〉} = {〈1, (1st
‘𝑤)〉, 〈2,
(2nd ‘𝑤)〉}) |
| 61 | | prex 5437 |
. . . . . . . . 9
⊢ {〈1,
(1st ‘𝑤)〉, 〈2, (2nd
‘𝑤)〉} ∈
V |
| 62 | 58, 60, 1, 61 | ovmpo 7593 |
. . . . . . . 8
⊢
(((1st ‘𝑤) ∈ ℝ ∧ (2nd
‘𝑤) ∈ ℝ)
→ ((1st ‘𝑤)𝐹(2nd ‘𝑤)) = {〈1, (1st ‘𝑤)〉, 〈2,
(2nd ‘𝑤)〉}) |
| 63 | 55, 56, 62 | syl2anc 584 |
. . . . . . 7
⊢ (𝑤 ∈ (ℝ ×
ℝ) → ((1st ‘𝑤)𝐹(2nd ‘𝑤)) = {〈1, (1st ‘𝑤)〉, 〈2,
(2nd ‘𝑤)〉}) |
| 64 | 54, 63 | eqtrd 2777 |
. . . . . 6
⊢ (𝑤 ∈ (ℝ ×
ℝ) → (𝐹‘𝑤) = {〈1, (1st ‘𝑤)〉, 〈2,
(2nd ‘𝑤)〉}) |
| 65 | 17, 64 | eqeqan12d 2751 |
. . . . 5
⊢ ((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ {〈1, (1st
‘𝑧)〉, 〈2,
(2nd ‘𝑧)〉} = {〈1, (1st
‘𝑤)〉, 〈2,
(2nd ‘𝑤)〉})) |
| 66 | 4, 51 | eqeqan12d 2751 |
. . . . . 6
⊢ ((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → (𝑧 = 𝑤 ↔ 〈(1st ‘𝑧), (2nd ‘𝑧)〉 = 〈(1st
‘𝑤), (2nd
‘𝑤)〉)) |
| 67 | 32, 36 | opth 5481 |
. . . . . 6
⊢
(〈(1st ‘𝑧), (2nd ‘𝑧)〉 = 〈(1st ‘𝑤), (2nd ‘𝑤)〉 ↔ ((1st
‘𝑧) = (1st
‘𝑤) ∧
(2nd ‘𝑧) =
(2nd ‘𝑤))) |
| 68 | 66, 67 | bitrdi 287 |
. . . . 5
⊢ ((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd
‘𝑧) = (2nd
‘𝑤)))) |
| 69 | 50, 65, 68 | 3imtr4d 294 |
. . . 4
⊢ ((𝑧 ∈ (ℝ ×
ℝ) ∧ 𝑤 ∈
(ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
| 70 | 69 | rgen2 3199 |
. . 3
⊢
∀𝑧 ∈
(ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤) |
| 71 | | dff13 7275 |
. . 3
⊢ (𝐹:(ℝ ×
ℝ)–1-1→𝑅 ↔ (𝐹:(ℝ × ℝ)⟶𝑅 ∧ ∀𝑧 ∈ (ℝ ×
ℝ)∀𝑤 ∈
(ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
| 72 | 25, 70, 71 | mpbir2an 711 |
. 2
⊢ 𝐹:(ℝ ×
ℝ)–1-1→𝑅 |
| 73 | 19 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑅 ↔ 𝑤 ∈ (ℝ ↑m {1,
2})) |
| 74 | | reex 11246 |
. . . . . . . . 9
⊢ ℝ
∈ V |
| 75 | | prex 5437 |
. . . . . . . . 9
⊢ {1, 2}
∈ V |
| 76 | 74, 75 | elmap 8911 |
. . . . . . . 8
⊢ (𝑤 ∈ (ℝ
↑m {1, 2}) ↔ 𝑤:{1, 2}⟶ℝ) |
| 77 | | 1re 11261 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
| 78 | | 2re 12340 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
| 79 | | fpr2g 7231 |
. . . . . . . . 9
⊢ ((1
∈ ℝ ∧ 2 ∈ ℝ) → (𝑤:{1, 2}⟶ℝ ↔ ((𝑤‘1) ∈ ℝ ∧
(𝑤‘2) ∈ ℝ
∧ 𝑤 = {〈1, (𝑤‘1)〉, 〈2, (𝑤‘2)〉}))) |
| 80 | 77, 78, 79 | mp2an 692 |
. . . . . . . 8
⊢ (𝑤:{1, 2}⟶ℝ ↔
((𝑤‘1) ∈ ℝ
∧ (𝑤‘2) ∈
ℝ ∧ 𝑤 = {〈1,
(𝑤‘1)〉, 〈2,
(𝑤‘2)〉})) |
| 81 | 73, 76, 80 | 3bitri 297 |
. . . . . . 7
⊢ (𝑤 ∈ 𝑅 ↔ ((𝑤‘1) ∈ ℝ ∧ (𝑤‘2) ∈ ℝ ∧
𝑤 = {〈1, (𝑤‘1)〉, 〈2, (𝑤‘2)〉})) |
| 82 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑤‘1) → 〈1, 𝑢〉 = 〈1, (𝑤‘1)〉) |
| 83 | 82 | preq1d 4739 |
. . . . . . . . 9
⊢ (𝑢 = (𝑤‘1) → {〈1, 𝑢〉, 〈2, 𝑣〉} = {〈1, (𝑤‘1)〉, 〈2, 𝑣〉}) |
| 84 | 83 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑢 = (𝑤‘1) → (𝑤 = {〈1, 𝑢〉, 〈2, 𝑣〉} ↔ 𝑤 = {〈1, (𝑤‘1)〉, 〈2, 𝑣〉})) |
| 85 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑤‘2) → 〈2, 𝑣〉 = 〈2, (𝑤‘2)〉) |
| 86 | 85 | preq2d 4740 |
. . . . . . . . 9
⊢ (𝑣 = (𝑤‘2) → {〈1, (𝑤‘1)〉, 〈2, 𝑣〉} = {〈1, (𝑤‘1)〉, 〈2, (𝑤‘2)〉}) |
| 87 | 86 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑣 = (𝑤‘2) → (𝑤 = {〈1, (𝑤‘1)〉, 〈2, 𝑣〉} ↔ 𝑤 = {〈1, (𝑤‘1)〉, 〈2, (𝑤‘2)〉})) |
| 88 | 84, 87 | rspc2ev 3635 |
. . . . . . 7
⊢ (((𝑤‘1) ∈ ℝ ∧
(𝑤‘2) ∈ ℝ
∧ 𝑤 = {〈1, (𝑤‘1)〉, 〈2, (𝑤‘2)〉}) →
∃𝑢 ∈ ℝ
∃𝑣 ∈ ℝ
𝑤 = {〈1, 𝑢〉, 〈2, 𝑣〉}) |
| 89 | 81, 88 | sylbi 217 |
. . . . . 6
⊢ (𝑤 ∈ 𝑅 → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {〈1, 𝑢〉, 〈2, 𝑣〉}) |
| 90 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑢 → 〈1, 𝑥〉 = 〈1, 𝑢〉) |
| 91 | 90 | preq1d 4739 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → {〈1, 𝑥〉, 〈2, 𝑦〉} = {〈1, 𝑢〉, 〈2, 𝑦〉}) |
| 92 | | opeq2 4874 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑣 → 〈2, 𝑦〉 = 〈2, 𝑣〉) |
| 93 | 92 | preq2d 4740 |
. . . . . . . . 9
⊢ (𝑦 = 𝑣 → {〈1, 𝑢〉, 〈2, 𝑦〉} = {〈1, 𝑢〉, 〈2, 𝑣〉}) |
| 94 | | prex 5437 |
. . . . . . . . 9
⊢ {〈1,
𝑢〉, 〈2, 𝑣〉} ∈
V |
| 95 | 91, 93, 1, 94 | ovmpo 7593 |
. . . . . . . 8
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢𝐹𝑣) = {〈1, 𝑢〉, 〈2, 𝑣〉}) |
| 96 | 95 | eqeq2d 2748 |
. . . . . . 7
⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑤 = (𝑢𝐹𝑣) ↔ 𝑤 = {〈1, 𝑢〉, 〈2, 𝑣〉})) |
| 97 | 96 | 2rexbiia 3218 |
. . . . . 6
⊢
(∃𝑢 ∈
ℝ ∃𝑣 ∈
ℝ 𝑤 = (𝑢𝐹𝑣) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = {〈1, 𝑢〉, 〈2, 𝑣〉}) |
| 98 | 89, 97 | sylibr 234 |
. . . . 5
⊢ (𝑤 ∈ 𝑅 → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣)) |
| 99 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (𝐹‘𝑧) = (𝐹‘〈𝑢, 𝑣〉)) |
| 100 | | df-ov 7434 |
. . . . . . . 8
⊢ (𝑢𝐹𝑣) = (𝐹‘〈𝑢, 𝑣〉) |
| 101 | 99, 100 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (𝐹‘𝑧) = (𝑢𝐹𝑣)) |
| 102 | 101 | eqeq2d 2748 |
. . . . . 6
⊢ (𝑧 = 〈𝑢, 𝑣〉 → (𝑤 = (𝐹‘𝑧) ↔ 𝑤 = (𝑢𝐹𝑣))) |
| 103 | 102 | rexxp 5853 |
. . . . 5
⊢
(∃𝑧 ∈
(ℝ × ℝ)𝑤
= (𝐹‘𝑧) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣)) |
| 104 | 98, 103 | sylibr 234 |
. . . 4
⊢ (𝑤 ∈ 𝑅 → ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)) |
| 105 | 104 | rgen 3063 |
. . 3
⊢
∀𝑤 ∈
𝑅 ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧) |
| 106 | | dffo3 7122 |
. . 3
⊢ (𝐹:(ℝ ×
ℝ)–onto→𝑅 ↔ (𝐹:(ℝ × ℝ)⟶𝑅 ∧ ∀𝑤 ∈ 𝑅 ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧))) |
| 107 | 25, 105, 106 | mpbir2an 711 |
. 2
⊢ 𝐹:(ℝ ×
ℝ)–onto→𝑅 |
| 108 | | df-f1o 6568 |
. 2
⊢ (𝐹:(ℝ ×
ℝ)–1-1-onto→𝑅 ↔ (𝐹:(ℝ × ℝ)–1-1→𝑅 ∧ 𝐹:(ℝ × ℝ)–onto→𝑅)) |
| 109 | 72, 107, 108 | mpbir2an 711 |
1
⊢ 𝐹:(ℝ ×
ℝ)–1-1-onto→𝑅 |