| Step | Hyp | Ref
| Expression |
| 1 | | rrx2plord2.r |
. . . . 5
⊢ 𝑅 = (ℝ ↑m
{1, 2}) |
| 2 | | eqid 2737 |
. . . . 5
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}) |
| 3 | 1, 2 | rrx2xpref1o 48639 |
. . . 4
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}):(ℝ ×
ℝ)–1-1-onto→𝑅 |
| 4 | | elxpi 5707 |
. . . . . 6
⊢ (𝑎 ∈ (ℝ ×
ℝ) → ∃𝑐∃𝑑(𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ))) |
| 5 | | elxpi 5707 |
. . . . . 6
⊢ (𝑏 ∈ (ℝ ×
ℝ) → ∃𝑒∃𝑓(𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) |
| 6 | | df-br 5144 |
. . . . . . . . . . . . 13
⊢ (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ 〈𝑎, 𝑏〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}) |
| 7 | | opelxpi 5722 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) →
〈𝑐, 𝑑〉 ∈ (ℝ ×
ℝ)) |
| 8 | 7 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → 〈𝑐, 𝑑〉 ∈ (ℝ ×
ℝ)) |
| 9 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 〈𝑐, 𝑑〉 → (𝑎 ∈ (ℝ × ℝ) ↔
〈𝑐, 𝑑〉 ∈ (ℝ ×
ℝ))) |
| 10 | 9 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎 ∈ (ℝ × ℝ) ↔
〈𝑐, 𝑑〉 ∈ (ℝ ×
ℝ))) |
| 11 | 8, 10 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → 𝑎 ∈ (ℝ ×
ℝ)) |
| 12 | | opelxpi 5722 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) →
〈𝑒, 𝑓〉 ∈ (ℝ ×
ℝ)) |
| 13 | 12 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → 〈𝑒, 𝑓〉 ∈ (ℝ ×
ℝ)) |
| 14 | | eleq1 2829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 〈𝑒, 𝑓〉 → (𝑏 ∈ (ℝ × ℝ) ↔
〈𝑒, 𝑓〉 ∈ (ℝ ×
ℝ))) |
| 15 | 14 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → (𝑏 ∈ (ℝ × ℝ) ↔
〈𝑒, 𝑓〉 ∈ (ℝ ×
ℝ))) |
| 16 | 13, 15 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → 𝑏 ∈ (ℝ ×
ℝ)) |
| 17 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (1st ‘𝑥) = (1st ‘𝑎)) |
| 18 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑏 → (1st ‘𝑦) = (1st ‘𝑏)) |
| 19 | 17, 18 | breqan12d 5159 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((1st ‘𝑥) < (1st
‘𝑦) ↔
(1st ‘𝑎)
< (1st ‘𝑏))) |
| 20 | 17, 18 | eqeqan12d 2751 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((1st ‘𝑥) = (1st ‘𝑦) ↔ (1st
‘𝑎) = (1st
‘𝑏))) |
| 21 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → (2nd ‘𝑥) = (2nd ‘𝑎)) |
| 22 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑏 → (2nd ‘𝑦) = (2nd ‘𝑏)) |
| 23 | 21, 22 | breqan12d 5159 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((2nd ‘𝑥) < (2nd
‘𝑦) ↔
(2nd ‘𝑎)
< (2nd ‘𝑏))) |
| 24 | 20, 23 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd
‘𝑥) <
(2nd ‘𝑦))
↔ ((1st ‘𝑎) = (1st ‘𝑏) ∧ (2nd ‘𝑎) < (2nd
‘𝑏)))) |
| 25 | 19, 24 | orbi12d 919 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (((1st ‘𝑥) < (1st
‘𝑦) ∨
((1st ‘𝑥)
= (1st ‘𝑦)
∧ (2nd ‘𝑥) < (2nd ‘𝑦))) ↔ ((1st
‘𝑎) <
(1st ‘𝑏)
∨ ((1st ‘𝑎) = (1st ‘𝑏) ∧ (2nd ‘𝑎) < (2nd
‘𝑏))))) |
| 26 | 25 | opelopab2a 5540 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ (ℝ ×
ℝ) ∧ 𝑏 ∈
(ℝ × ℝ)) → (〈𝑎, 𝑏〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))} ↔ ((1st ‘𝑎) < (1st
‘𝑏) ∨
((1st ‘𝑎)
= (1st ‘𝑏)
∧ (2nd ‘𝑎) < (2nd ‘𝑏))))) |
| 27 | 11, 16, 26 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (〈𝑎, 𝑏〉 ∈ {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))} ↔ ((1st ‘𝑎) < (1st
‘𝑏) ∨
((1st ‘𝑎)
= (1st ‘𝑏)
∧ (2nd ‘𝑎) < (2nd ‘𝑏))))) |
| 28 | 6, 27 | bitrid 283 |
. . . . . . . . . . . 12
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((1st ‘𝑎) < (1st
‘𝑏) ∨
((1st ‘𝑎)
= (1st ‘𝑏)
∧ (2nd ‘𝑎) < (2nd ‘𝑏))))) |
| 29 | | 1ne2 12474 |
. . . . . . . . . . . . . . . 16
⊢ 1 ≠
2 |
| 30 | | 1ex 11257 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
V |
| 31 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑐 ∈ V |
| 32 | 30, 31 | fvpr1 7212 |
. . . . . . . . . . . . . . . 16
⊢ (1 ≠ 2
→ ({〈1, 𝑐〉,
〈2, 𝑑〉}‘1)
= 𝑐) |
| 33 | 29, 32 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ({〈1, 𝑐〉, 〈2, 𝑑〉}‘1) = 𝑐) |
| 34 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑒 ∈ V |
| 35 | 30, 34 | fvpr1 7212 |
. . . . . . . . . . . . . . . 16
⊢ (1 ≠ 2
→ ({〈1, 𝑒〉,
〈2, 𝑓〉}‘1)
= 𝑒) |
| 36 | 29, 35 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ({〈1, 𝑒〉, 〈2, 𝑓〉}‘1) = 𝑒) |
| 37 | 33, 36 | breq12d 5156 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (({〈1, 𝑐〉, 〈2, 𝑑〉}‘1) < ({〈1,
𝑒〉, 〈2, 𝑓〉}‘1) ↔ 𝑐 < 𝑒)) |
| 38 | 33, 36 | eqeq12d 2753 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (({〈1, 𝑐〉, 〈2, 𝑑〉}‘1) = ({〈1,
𝑒〉, 〈2, 𝑓〉}‘1) ↔ 𝑐 = 𝑒)) |
| 39 | | 2ex 12343 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
V |
| 40 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑑 ∈ V |
| 41 | 39, 40 | fvpr2 7213 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ≠ 2
→ ({〈1, 𝑐〉,
〈2, 𝑑〉}‘2)
= 𝑑) |
| 42 | 29, 41 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ({〈1, 𝑐〉, 〈2, 𝑑〉}‘2) = 𝑑) |
| 43 | | vex 3484 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑓 ∈ V |
| 44 | 39, 43 | fvpr2 7213 |
. . . . . . . . . . . . . . . . 17
⊢ (1 ≠ 2
→ ({〈1, 𝑒〉,
〈2, 𝑓〉}‘2)
= 𝑓) |
| 45 | 29, 44 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ({〈1, 𝑒〉, 〈2, 𝑓〉}‘2) = 𝑓) |
| 46 | 42, 45 | breq12d 5156 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (({〈1, 𝑐〉, 〈2, 𝑑〉}‘2) < ({〈1,
𝑒〉, 〈2, 𝑓〉}‘2) ↔ 𝑑 < 𝑓)) |
| 47 | 38, 46 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ((({〈1, 𝑐〉, 〈2, 𝑑〉}‘1) = ({〈1,
𝑒〉, 〈2, 𝑓〉}‘1) ∧
({〈1, 𝑐〉,
〈2, 𝑑〉}‘2)
< ({〈1, 𝑒〉,
〈2, 𝑓〉}‘2))
↔ (𝑐 = 𝑒 ∧ 𝑑 < 𝑓))) |
| 48 | 37, 47 | orbi12d 919 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ((({〈1, 𝑐〉, 〈2, 𝑑〉}‘1) < ({〈1,
𝑒〉, 〈2, 𝑓〉}‘1) ∨
(({〈1, 𝑐〉,
〈2, 𝑑〉}‘1)
= ({〈1, 𝑒〉,
〈2, 𝑓〉}‘1)
∧ ({〈1, 𝑐〉,
〈2, 𝑑〉}‘2)
< ({〈1, 𝑒〉,
〈2, 𝑓〉}‘2))) ↔ (𝑐 < 𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑 < 𝑓)))) |
| 49 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ {1, 2} =
{1, 2} |
| 50 | 49, 1 | prelrrx2 48634 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) →
{〈1, 𝑐〉, 〈2,
𝑑〉} ∈ 𝑅) |
| 51 | 50 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → {〈1, 𝑐〉, 〈2, 𝑑〉} ∈ 𝑅) |
| 52 | 49, 1 | prelrrx2 48634 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) →
{〈1, 𝑒〉, 〈2,
𝑓〉} ∈ 𝑅) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → {〈1, 𝑒〉, 〈2, 𝑓〉} ∈ 𝑅) |
| 54 | | rrx2plord.o |
. . . . . . . . . . . . . . 15
⊢ 𝑂 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅) ∧ ((𝑥‘1) < (𝑦‘1) ∨ ((𝑥‘1) = (𝑦‘1) ∧ (𝑥‘2) < (𝑦‘2))))} |
| 55 | 54 | rrx2plord 48641 |
. . . . . . . . . . . . . 14
⊢
(({〈1, 𝑐〉,
〈2, 𝑑〉} ∈
𝑅 ∧ {〈1, 𝑒〉, 〈2, 𝑓〉} ∈ 𝑅) → ({〈1, 𝑐〉, 〈2, 𝑑〉}𝑂{〈1, 𝑒〉, 〈2, 𝑓〉} ↔ (({〈1, 𝑐〉, 〈2, 𝑑〉}‘1) < ({〈1, 𝑒〉, 〈2, 𝑓〉}‘1) ∨
(({〈1, 𝑐〉,
〈2, 𝑑〉}‘1)
= ({〈1, 𝑒〉,
〈2, 𝑓〉}‘1)
∧ ({〈1, 𝑐〉,
〈2, 𝑑〉}‘2)
< ({〈1, 𝑒〉,
〈2, 𝑓〉}‘2))))) |
| 56 | 51, 53, 55 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ({〈1, 𝑐〉, 〈2, 𝑑〉}𝑂{〈1, 𝑒〉, 〈2, 𝑓〉} ↔ (({〈1, 𝑐〉, 〈2, 𝑑〉}‘1) < ({〈1, 𝑒〉, 〈2, 𝑓〉}‘1) ∨
(({〈1, 𝑐〉,
〈2, 𝑑〉}‘1)
= ({〈1, 𝑒〉,
〈2, 𝑓〉}‘1)
∧ ({〈1, 𝑐〉,
〈2, 𝑑〉}‘2)
< ({〈1, 𝑒〉,
〈2, 𝑓〉}‘2))))) |
| 57 | 31, 40 | op1std 8024 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 〈𝑐, 𝑑〉 → (1st ‘𝑎) = 𝑐) |
| 58 | 57 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (1st
‘𝑎) = 𝑐) |
| 59 | 34, 43 | op1std 8024 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 〈𝑒, 𝑓〉 → (1st ‘𝑏) = 𝑒) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → (1st
‘𝑏) = 𝑒) |
| 61 | 58, 60 | breqan12d 5159 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ((1st
‘𝑎) <
(1st ‘𝑏)
↔ 𝑐 < 𝑒)) |
| 62 | 58, 60 | eqeqan12d 2751 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ((1st
‘𝑎) = (1st
‘𝑏) ↔ 𝑐 = 𝑒)) |
| 63 | 31, 40 | op2ndd 8025 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 〈𝑐, 𝑑〉 → (2nd ‘𝑎) = 𝑑) |
| 64 | 63 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (2nd
‘𝑎) = 𝑑) |
| 65 | 34, 43 | op2ndd 8025 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 〈𝑒, 𝑓〉 → (2nd ‘𝑏) = 𝑓) |
| 66 | 65 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → (2nd
‘𝑏) = 𝑓) |
| 67 | 64, 66 | breqan12d 5159 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ((2nd
‘𝑎) <
(2nd ‘𝑏)
↔ 𝑑 < 𝑓)) |
| 68 | 62, 67 | anbi12d 632 |
. . . . . . . . . . . . . 14
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (((1st
‘𝑎) = (1st
‘𝑏) ∧
(2nd ‘𝑎)
< (2nd ‘𝑏)) ↔ (𝑐 = 𝑒 ∧ 𝑑 < 𝑓))) |
| 69 | 61, 68 | orbi12d 919 |
. . . . . . . . . . . . 13
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (((1st
‘𝑎) <
(1st ‘𝑏)
∨ ((1st ‘𝑎) = (1st ‘𝑏) ∧ (2nd ‘𝑎) < (2nd
‘𝑏))) ↔ (𝑐 < 𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑 < 𝑓)))) |
| 70 | 48, 56, 69 | 3bitr4rd 312 |
. . . . . . . . . . . 12
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (((1st
‘𝑎) <
(1st ‘𝑏)
∨ ((1st ‘𝑎) = (1st ‘𝑏) ∧ (2nd ‘𝑎) < (2nd
‘𝑏))) ↔
{〈1, 𝑐〉, 〈2,
𝑑〉}𝑂{〈1, 𝑒〉, 〈2, 𝑓〉})) |
| 71 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 〈𝑐, 𝑑〉 → ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎) = ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘〈𝑐, 𝑑〉)) |
| 72 | | df-ov 7434 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})𝑑) = ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘〈𝑐, 𝑑〉) |
| 73 | 71, 72 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 〈𝑐, 𝑑〉 → ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎) = (𝑐(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})𝑑)) |
| 74 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉})) |
| 75 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑐 → 〈1, 𝑥〉 = 〈1, 𝑐〉) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → 〈1, 𝑥〉 = 〈1, 𝑐〉) |
| 77 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑑 → 〈2, 𝑦〉 = 〈2, 𝑑〉) |
| 78 | 77 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → 〈2, 𝑦〉 = 〈2, 𝑑〉) |
| 79 | 76, 78 | preq12d 4741 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑐 ∧ 𝑦 = 𝑑) → {〈1, 𝑥〉, 〈2, 𝑦〉} = {〈1, 𝑐〉, 〈2, 𝑑〉}) |
| 80 | 79 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) ∧ (𝑥 = 𝑐 ∧ 𝑦 = 𝑑)) → {〈1, 𝑥〉, 〈2, 𝑦〉} = {〈1, 𝑐〉, 〈2, 𝑑〉}) |
| 81 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → 𝑐 ∈
ℝ) |
| 82 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → 𝑑 ∈
ℝ) |
| 83 | | prex 5437 |
. . . . . . . . . . . . . . . . 17
⊢ {〈1,
𝑐〉, 〈2, 𝑑〉} ∈
V |
| 84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) →
{〈1, 𝑐〉, 〈2,
𝑑〉} ∈
V) |
| 85 | 74, 80, 81, 82, 84 | ovmpod 7585 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ) → (𝑐(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})𝑑) = {〈1, 𝑐〉, 〈2, 𝑑〉}) |
| 86 | 73, 85 | sylan9eq 2797 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎) = {〈1, 𝑐〉, 〈2, 𝑑〉}) |
| 87 | 86 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → {〈1, 𝑐〉, 〈2, 𝑑〉} = ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)) |
| 88 | | fveq2 6906 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 〈𝑒, 𝑓〉 → ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏) = ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘〈𝑒, 𝑓〉)) |
| 89 | | df-ov 7434 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})𝑓) = ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘〈𝑒, 𝑓〉) |
| 90 | 88, 89 | eqtr4di 2795 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 〈𝑒, 𝑓〉 → ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏) = (𝑒(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})𝑓)) |
| 91 | | eqidd 2738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}) = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉})) |
| 92 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑒 → 〈1, 𝑥〉 = 〈1, 𝑒〉) |
| 93 | 92 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑒 ∧ 𝑦 = 𝑓) → 〈1, 𝑥〉 = 〈1, 𝑒〉) |
| 94 | | opeq2 4874 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑓 → 〈2, 𝑦〉 = 〈2, 𝑓〉) |
| 95 | 94 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑒 ∧ 𝑦 = 𝑓) → 〈2, 𝑦〉 = 〈2, 𝑓〉) |
| 96 | 93, 95 | preq12d 4741 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 𝑒 ∧ 𝑦 = 𝑓) → {〈1, 𝑥〉, 〈2, 𝑦〉} = {〈1, 𝑒〉, 〈2, 𝑓〉}) |
| 97 | 96 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) ∧ (𝑥 = 𝑒 ∧ 𝑦 = 𝑓)) → {〈1, 𝑥〉, 〈2, 𝑦〉} = {〈1, 𝑒〉, 〈2, 𝑓〉}) |
| 98 | | simpl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → 𝑒 ∈
ℝ) |
| 99 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → 𝑓 ∈
ℝ) |
| 100 | | prex 5437 |
. . . . . . . . . . . . . . . . 17
⊢ {〈1,
𝑒〉, 〈2, 𝑓〉} ∈
V |
| 101 | 100 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) →
{〈1, 𝑒〉, 〈2,
𝑓〉} ∈
V) |
| 102 | 91, 97, 98, 99, 101 | ovmpod 7585 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ) → (𝑒(𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})𝑓) = {〈1, 𝑒〉, 〈2, 𝑓〉}) |
| 103 | 90, 102 | sylan9eq 2797 |
. . . . . . . . . . . . . 14
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏) = {〈1, 𝑒〉, 〈2, 𝑓〉}) |
| 104 | 103 | eqcomd 2743 |
. . . . . . . . . . . . 13
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → {〈1, 𝑒〉, 〈2, 𝑓〉} = ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏)) |
| 105 | 87, 104 | breqan12d 5159 |
. . . . . . . . . . . 12
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → ({〈1, 𝑐〉, 〈2, 𝑑〉}𝑂{〈1, 𝑒〉, 〈2, 𝑓〉} ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏))) |
| 106 | 28, 70, 105 | 3bitrd 305 |
. . . . . . . . . . 11
⊢ (((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ (𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏))) |
| 107 | 106 | expcom 413 |
. . . . . . . . . 10
⊢ ((𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏)))) |
| 108 | 107 | exlimivv 1932 |
. . . . . . . . 9
⊢
(∃𝑒∃𝑓(𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏)))) |
| 109 | 108 | com12 32 |
. . . . . . . 8
⊢ ((𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (∃𝑒∃𝑓(𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏)))) |
| 110 | 109 | exlimivv 1932 |
. . . . . . 7
⊢
(∃𝑐∃𝑑(𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) → (∃𝑒∃𝑓(𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ)) → (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏)))) |
| 111 | 110 | imp 406 |
. . . . . 6
⊢
((∃𝑐∃𝑑(𝑎 = 〈𝑐, 𝑑〉 ∧ (𝑐 ∈ ℝ ∧ 𝑑 ∈ ℝ)) ∧ ∃𝑒∃𝑓(𝑏 = 〈𝑒, 𝑓〉 ∧ (𝑒 ∈ ℝ ∧ 𝑓 ∈ ℝ))) → (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏))) |
| 112 | 4, 5, 111 | syl2an 596 |
. . . . 5
⊢ ((𝑎 ∈ (ℝ ×
ℝ) ∧ 𝑏 ∈
(ℝ × ℝ)) → (𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏))) |
| 113 | 112 | rgen2 3199 |
. . . 4
⊢
∀𝑎 ∈
(ℝ × ℝ)∀𝑏 ∈ (ℝ × ℝ)(𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏)) |
| 114 | | df-isom 6570 |
. . . 4
⊢ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}) Isom {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}, 𝑂((ℝ × ℝ), 𝑅) ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}):(ℝ ×
ℝ)–1-1-onto→𝑅 ∧ ∀𝑎 ∈ (ℝ ×
ℝ)∀𝑏 ∈
(ℝ × ℝ)(𝑎{〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}𝑏 ↔ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑎)𝑂((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉})‘𝑏)))) |
| 115 | 3, 113, 114 | mpbir2an 711 |
. . 3
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}) Isom {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}, 𝑂((ℝ × ℝ), 𝑅) |
| 116 | | rrx2plordisom.t |
. . . 4
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))} |
| 117 | | isoeq2 7338 |
. . . 4
⊢ (𝑇 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))} → ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅) ↔ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) Isom {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}, 𝑂((ℝ × ℝ), 𝑅))) |
| 118 | 116, 117 | ax-mp 5 |
. . 3
⊢ ((𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}) Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅) ↔ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) Isom {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ (ℝ × ℝ) ∧ 𝑦 ∈ (ℝ ×
ℝ)) ∧ ((1st ‘𝑥) < (1st ‘𝑦) ∨ ((1st
‘𝑥) = (1st
‘𝑦) ∧
(2nd ‘𝑥)
< (2nd ‘𝑦))))}, 𝑂((ℝ × ℝ), 𝑅)) |
| 119 | 115, 118 | mpbir 231 |
. 2
⊢ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦
{〈1, 𝑥〉, 〈2,
𝑦〉}) Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅) |
| 120 | | rrx2plordisom.f |
. . 3
⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) |
| 121 | | isoeq1 7337 |
. . 3
⊢ (𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) → (𝐹 Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅) ↔ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅))) |
| 122 | 120, 121 | ax-mp 5 |
. 2
⊢ (𝐹 Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅) ↔ (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ {〈1, 𝑥〉, 〈2, 𝑦〉}) Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅)) |
| 123 | 119, 122 | mpbir 231 |
1
⊢ 𝐹 Isom 𝑇, 𝑂 ((ℝ × ℝ), 𝑅) |