This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐵 ≠ 𝐶 ) ) → inf ( { 𝐵 , 𝐶 } , 𝐴 , 𝑅 ) 𝑅 sup ( { 𝐵 , 𝐶 } , 𝐴 , 𝑅 ) )

Proof

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