Step |
Hyp |
Ref |
Expression |
1 |
|
rrx2plord.o |
⊢ 𝑂 = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) } |
2 |
|
df-br |
⊢ ( 𝑋 𝑂 𝑌 ↔ 〈 𝑋 , 𝑌 〉 ∈ 𝑂 ) |
3 |
1
|
eleq2i |
⊢ ( 〈 𝑋 , 𝑌 〉 ∈ 𝑂 ↔ 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) } ) |
4 |
2 3
|
bitri |
⊢ ( 𝑋 𝑂 𝑌 ↔ 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) } ) |
5 |
|
fveq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 1 ) = ( 𝑋 ‘ 1 ) ) |
6 |
|
fveq1 |
⊢ ( 𝑦 = 𝑌 → ( 𝑦 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) |
7 |
5 6
|
breqan12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ↔ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) ) |
8 |
5 6
|
eqeqan12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ↔ ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ) ) |
9 |
|
fveq1 |
⊢ ( 𝑥 = 𝑋 → ( 𝑥 ‘ 2 ) = ( 𝑋 ‘ 2 ) ) |
10 |
|
fveq1 |
⊢ ( 𝑦 = 𝑌 → ( 𝑦 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) |
11 |
9 10
|
breqan12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ↔ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) |
12 |
8 11
|
anbi12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ↔ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) |
13 |
7 12
|
orbi12d |
⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) ) |
14 |
13
|
opelopab2a |
⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 〈 𝑋 , 𝑌 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) } ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) ) |
15 |
4 14
|
syl5bb |
⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑋 𝑂 𝑌 ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) ) |