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

Metamath Proof Explorer

Theorem infpr

Description: The infimum of a pair. (Contributed by AV, 4-Sep-2020)

Ref Expression
Assertion infpr ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → inf ( { 𝐵 , 𝐶 } , 𝐴 , 𝑅 ) = 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 breq2 ⊢ ( 𝐵 = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( 𝐵 𝑅 𝐵 ↔ 𝐵 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
7 6 notbid ⊢ ( 𝐵 = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( ¬ 𝐵 𝑅 𝐵 ↔ ¬ 𝐵 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
8 breq2 ⊢ ( 𝐶 = 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 breq2 ⊢ ( 𝐵 = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( 𝐶 𝑅 𝐵 ↔ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
16 15 notbid ⊢ ( 𝐵 = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( ¬ 𝐶 𝑅 𝐵 ↔ ¬ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
17 breq2 ⊢ ( 𝐶 = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( 𝐶 𝑅 𝐶 ↔ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
18 17 notbid ⊢ ( 𝐶 = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( ¬ 𝐶 𝑅 𝐶 ↔ ¬ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
19 so2nr ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) )
20 19 3impb ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) )
21 imnan ⊢ ( ( 𝐵 𝑅 𝐶 → ¬ 𝐶 𝑅 𝐵 ) ↔ ¬ ( 𝐵 𝑅 𝐶 ∧ 𝐶 𝑅 𝐵 ) )
22 20 21 sylibr ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( 𝐵 𝑅 𝐶 → ¬ 𝐶 𝑅 𝐵 ) )
23 22 imp ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝐵 𝑅 𝐶 ) → ¬ 𝐶 𝑅 𝐵 )
24 sonr ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ¬ 𝐶 𝑅 𝐶 )
25 24 3adant2 ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ¬ 𝐶 𝑅 𝐶 )
26 25 adantr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ∧ ¬ 𝐵 𝑅 𝐶 ) → ¬ 𝐶 𝑅 𝐶 )
27 16 18 23 26 ifbothda ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ¬ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) )
28 breq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ↔ 𝐵 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
29 28 notbid ⊢ ( 𝑦 = 𝐵 → ( ¬ 𝑦 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ↔ ¬ 𝐵 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
30 breq1 ⊢ ( 𝑦 = 𝐶 → ( 𝑦 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ↔ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
31 30 notbid ⊢ ( 𝑦 = 𝐶 → ( ¬ 𝑦 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ↔ ¬ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
32 29 31 ralprg ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 } ¬ 𝑦 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ↔ ( ¬ 𝐵 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∧ ¬ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) ) )
33 32 3adant1 ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ { 𝐵 , 𝐶 } ¬ 𝑦 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ↔ ( ¬ 𝐵 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∧ ¬ 𝐶 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) ) )
34 14 27 33 mpbir2and ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → ∀ 𝑦 ∈ { 𝐵 , 𝐶 } ¬ 𝑦 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) )
35 34 r19.21bi ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) ∧ 𝑦 ∈ { 𝐵 , 𝐶 } ) → ¬ 𝑦 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) )
36 1 3 5 35 infmin ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ) → inf ( { 𝐵 , 𝐶 } , 𝐴 , 𝑅 ) = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) )