Step |
Hyp |
Ref |
Expression |
1 |
|
legval.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
legval.d |
⊢ − = ( dist ‘ 𝐺 ) |
3 |
|
legval.i |
⊢ 𝐼 = ( Itv ‘ 𝐺 ) |
4 |
|
legval.l |
⊢ ≤ = ( ≤G ‘ 𝐺 ) |
5 |
|
legval.g |
⊢ ( 𝜑 → 𝐺 ∈ TarskiG ) |
6 |
|
legso.a |
⊢ 𝐸 = ( − “ ( 𝑃 × 𝑃 ) ) |
7 |
|
legso.f |
⊢ ( 𝜑 → Fun − ) |
8 |
|
legso.l |
⊢ < = ( ( ≤ ↾ 𝐸 ) ∖ I ) |
9 |
|
legso.d |
⊢ ( 𝜑 → ( 𝑃 × 𝑃 ) ⊆ dom − ) |
10 |
|
ltgov.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑃 ) |
11 |
|
ltgov.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑃 ) |
12 |
8
|
breqi |
⊢ ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) ( ( ≤ ↾ 𝐸 ) ∖ I ) ( 𝐶 − 𝐷 ) ) |
13 |
|
brdif |
⊢ ( ( 𝐴 − 𝐵 ) ( ( ≤ ↾ 𝐸 ) ∖ I ) ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ( ≤ ↾ 𝐸 ) ( 𝐶 − 𝐷 ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) |
14 |
12 13
|
bitri |
⊢ ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ( ≤ ↾ 𝐸 ) ( 𝐶 − 𝐷 ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) |
15 |
|
ovex |
⊢ ( 𝐶 − 𝐷 ) ∈ V |
16 |
15
|
brresi |
⊢ ( ( 𝐴 − 𝐵 ) ( ≤ ↾ 𝐸 ) ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ) |
17 |
16
|
anbi1i |
⊢ ( ( ( 𝐴 − 𝐵 ) ( ≤ ↾ 𝐸 ) ( 𝐶 − 𝐷 ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ↔ ( ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) |
18 |
|
an21 |
⊢ ( ( ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ) ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) ) |
19 |
14 17 18
|
3bitri |
⊢ ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) ) |
20 |
10 11 7 9
|
elovimad |
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ ( − “ ( 𝑃 × 𝑃 ) ) ) |
21 |
20 6
|
eleqtrrdi |
⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) ∈ 𝐸 ) |
22 |
21
|
biantrurd |
⊢ ( 𝜑 → ( ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) ) |
23 |
15
|
ideq |
⊢ ( ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) = ( 𝐶 − 𝐷 ) ) |
24 |
23
|
necon3bbii |
⊢ ( ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ↔ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) |
25 |
22 24
|
bitr3di |
⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ↔ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) |
26 |
25
|
anbi2d |
⊢ ( 𝜑 → ( ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( ( 𝐴 − 𝐵 ) ∈ 𝐸 ∧ ¬ ( 𝐴 − 𝐵 ) I ( 𝐶 − 𝐷 ) ) ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) ) |
27 |
19 26
|
syl5bb |
⊢ ( 𝜑 → ( ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) ↔ ( ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐷 ) ∧ ( 𝐴 − 𝐵 ) ≠ ( 𝐶 − 𝐷 ) ) ) ) |