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