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 ( 𝐶 𝑅 𝐵 , 𝐵 , 𝐶 ) )