Metamath Proof Explorer


Theorem suppr

Description: The supremum of a pair. (Contributed by NM, 17-Jun-2007) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion suppr ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → sup ( { 𝐵 , 𝐶 } , 𝐴 , 𝑅 ) = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simp1 ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → 𝑅 Or 𝐴 )
2 ifcl ( ( 𝐵𝐴𝐶𝐴 ) → if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) ∈ 𝐴 )
3 2 3adant1 ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) ∈ 𝐴 )
4 ifpr ( ( 𝐵𝐴𝐶𝐴 ) → if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) ∈ { 𝐵 , 𝐶 } )
5 4 3adant1 ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) ∈ { 𝐵 , 𝐶 } )
6 breq1 ( 𝐵 = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) → ( 𝐵 𝑅 𝐵 ↔ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 ) )
7 6 notbid ( 𝐵 = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) → ( ¬ 𝐵 𝑅 𝐵 ↔ ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 ) )
8 breq1 ( 𝐶 = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) → ( 𝐶 𝑅 𝐵 ↔ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 ) )
9 8 notbid ( 𝐶 = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) → ( ¬ 𝐶 𝑅 𝐵 ↔ ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 ) )
10 sonr ( ( 𝑅 Or 𝐴𝐵𝐴 ) → ¬ 𝐵 𝑅 𝐵 )
11 10 3adant3 ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → ¬ 𝐵 𝑅 𝐵 )
12 11 adantr ( ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) ∧ 𝐶 𝑅 𝐵 ) → ¬ 𝐵 𝑅 𝐵 )
13 simpr ( ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) ∧ ¬ 𝐶 𝑅 𝐵 ) → ¬ 𝐶 𝑅 𝐵 )
14 7 9 12 13 ifbothda ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 )
15 breq1 ( 𝐵 = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) → ( 𝐵 𝑅 𝐶 ↔ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 ) )
16 15 notbid ( 𝐵 = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) → ( ¬ 𝐵 𝑅 𝐶 ↔ ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 ) )
17 breq1 ( 𝐶 = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) → ( 𝐶 𝑅 𝐶 ↔ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 ) )
18 17 notbid ( 𝐶 = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) → ( ¬ 𝐶 𝑅 𝐶 ↔ ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 ) )
19 so2nr ( ( 𝑅 Or 𝐴 ∧ ( 𝐶𝐴𝐵𝐴 ) ) → ¬ ( 𝐶 𝑅 𝐵𝐵 𝑅 𝐶 ) )
20 19 3impb ( ( 𝑅 Or 𝐴𝐶𝐴𝐵𝐴 ) → ¬ ( 𝐶 𝑅 𝐵𝐵 𝑅 𝐶 ) )
21 20 3com23 ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → ¬ ( 𝐶 𝑅 𝐵𝐵 𝑅 𝐶 ) )
22 imnan ( ( 𝐶 𝑅 𝐵 → ¬ 𝐵 𝑅 𝐶 ) ↔ ¬ ( 𝐶 𝑅 𝐵𝐵 𝑅 𝐶 ) )
23 21 22 sylibr ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → ( 𝐶 𝑅 𝐵 → ¬ 𝐵 𝑅 𝐶 ) )
24 23 imp ( ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) ∧ 𝐶 𝑅 𝐵 ) → ¬ 𝐵 𝑅 𝐶 )
25 sonr ( ( 𝑅 Or 𝐴𝐶𝐴 ) → ¬ 𝐶 𝑅 𝐶 )
26 25 3adant2 ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → ¬ 𝐶 𝑅 𝐶 )
27 26 adantr ( ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) ∧ ¬ 𝐶 𝑅 𝐵 ) → ¬ 𝐶 𝑅 𝐶 )
28 16 18 24 27 ifbothda ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 )
29 breq2 ( 𝑦 = 𝐵 → ( if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝑦 ↔ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 ) )
30 29 notbid ( 𝑦 = 𝐵 → ( ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝑦 ↔ ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 ) )
31 breq2 ( 𝑦 = 𝐶 → ( if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝑦 ↔ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 ) )
32 31 notbid ( 𝑦 = 𝐶 → ( ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝑦 ↔ ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 ) )
33 30 32 ralprg ( ( 𝐵𝐴𝐶𝐴 ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 } ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝑦 ↔ ( ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 ∧ ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 ) ) )
34 33 3adant1 ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 } ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝑦 ↔ ( ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐵 ∧ ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝐶 ) ) )
35 14 28 34 mpbir2and ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → ∀ 𝑦 ∈ { 𝐵 , 𝐶 } ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝑦 )
36 35 r19.21bi ( ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) ∧ 𝑦 ∈ { 𝐵 , 𝐶 } ) → ¬ if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) 𝑅 𝑦 )
37 1 3 5 36 supmax ( ( 𝑅 Or 𝐴𝐵𝐴𝐶𝐴 ) → sup ( { 𝐵 , 𝐶 } , 𝐴 , 𝑅 ) = if ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) )