Step |
Hyp |
Ref |
Expression |
1 |
|
rrx2plord.o |
⊢ 𝑂 = { 〈 𝑥 , 𝑦 〉 ∣ ( ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ∧ ( ( 𝑥 ‘ 1 ) < ( 𝑦 ‘ 1 ) ∨ ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ∧ ( 𝑥 ‘ 2 ) < ( 𝑦 ‘ 2 ) ) ) ) } |
2 |
|
simp3 |
⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) |
3 |
2
|
orcd |
⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) |
4 |
1
|
rrx2plord |
⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ) → ( 𝑋 𝑂 𝑌 ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) ) |
5 |
4
|
3adant3 |
⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → ( 𝑋 𝑂 𝑌 ↔ ( ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ∨ ( ( 𝑋 ‘ 1 ) = ( 𝑌 ‘ 1 ) ∧ ( 𝑋 ‘ 2 ) < ( 𝑌 ‘ 2 ) ) ) ) ) |
6 |
3 5
|
mpbird |
⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑅 ∧ ( 𝑋 ‘ 1 ) < ( 𝑌 ‘ 1 ) ) → 𝑋 𝑂 𝑌 ) |