Metamath Proof Explorer

Theorem infsupprpr

Description: The infimum of a proper pair is less than the supremum of this pair. (Contributed by AV, 13-Mar-2023)

Ref Expression
Assertion infsupprpr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → inf B C A R R sup B C A R

Proof

Step Hyp Ref Expression
1 solin ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ∨ B = C ∨ C R B
2 1 3adantr3 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → B R C ∨ B = C ∨ C R B
3 iftrue ⊢ B R C → if B R C B C = B
4 3 adantr ⊢ B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C = B
5 sotric ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C ↔ ¬ B = C ∨ C R B
6 5 3adantr3 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → B R C ↔ ¬ B = C ∨ C R B
7 6 biimpac ⊢ B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → ¬ B = C ∨ C R B
8 ioran ⊢ ¬ B = C ∨ C R B ↔ ¬ B = C ∧ ¬ C R B
9 simprl ⊢ ¬ C R B ∧ B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → B R C
10 iffalse ⊢ ¬ C R B → if C R B B C = C
11 10 adantr ⊢ ¬ C R B ∧ B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if C R B B C = C
12 9 11 breqtrrd ⊢ ¬ C R B ∧ B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → B R if C R B B C
13 12 ex ⊢ ¬ C R B → B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → B R if C R B B C
14 8 13 simplbiim ⊢ ¬ B = C ∨ C R B → B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → B R if C R B B C
15 7 14 mpcom ⊢ B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → B R if C R B B C
16 4 15 eqbrtrd ⊢ B R C ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
17 16 ex ⊢ B R C → R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
18 eqneqall ⊢ B = C → B ≠ C → if B R C B C R if C R B B C
19 18 2a1d ⊢ B = C → B ∈ A → C ∈ A → B ≠ C → if B R C B C R if C R B B C
20 19 3impd ⊢ B = C → B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
21 20 adantld ⊢ B = C → R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
22 pm3.22 ⊢ B ∈ A ∧ C ∈ A → C ∈ A ∧ B ∈ A
23 22 3adant3 ⊢ B ∈ A ∧ C ∈ A ∧ B ≠ C → C ∈ A ∧ B ∈ A
24 sotric ⊢ R Or A ∧ C ∈ A ∧ B ∈ A → C R B ↔ ¬ C = B ∨ B R C
25 24 biimpd ⊢ R Or A ∧ C ∈ A ∧ B ∈ A → C R B → ¬ C = B ∨ B R C
26 23 25 sylan2 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → C R B → ¬ C = B ∨ B R C
27 26 impcom ⊢ C R B ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → ¬ C = B ∨ B R C
28 ioran ⊢ ¬ C = B ∨ B R C ↔ ¬ C = B ∧ ¬ B R C
29 simpr ⊢ ¬ B R C ∧ C R B → C R B
30 iffalse ⊢ ¬ B R C → if B R C B C = C
31 iftrue ⊢ C R B → if C R B B C = B
32 30 31 breqan12d ⊢ ¬ B R C ∧ C R B → if B R C B C R if C R B B C ↔ C R B
33 29 32 mpbird ⊢ ¬ B R C ∧ C R B → if B R C B C R if C R B B C
34 33 a1d ⊢ ¬ B R C ∧ C R B → R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
35 34 expimpd ⊢ ¬ B R C → C R B ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
36 28 35 simplbiim ⊢ ¬ C = B ∨ B R C → C R B ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
37 27 36 mpcom ⊢ C R B ∧ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
38 37 ex ⊢ C R B → R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
39 17 21 38 3jaoi ⊢ B R C ∨ B = C ∨ C R B → R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
40 2 39 mpcom ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → if B R C B C R if C R B B C
41 infpr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → inf B C A R = if B R C B C
42 suppr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → sup B C A R = if C R B B C
43 41 42 breq12d ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → inf B C A R R sup B C A R ↔ if B R C B C R if C R B B C
44 43 3adant3r3 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → inf B C A R R sup B C A R ↔ if B R C B C R if C R B B C
45 40 44 mpbird ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B ≠ C → inf B C A R R sup B C A R