Theorem soltmin

Description: Being less than a minimum, for a general total order. (Contributed by Stefan O'Rear, 17-Jan-2015)

	Ref	Expression
Assertion	soltmin	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑅 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sopo	⊢ ( 𝑅 Or 𝑋 → 𝑅 Po 𝑋 )
2	1	ad2antrr	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → 𝑅 Po 𝑋 )
3		simplr1	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → 𝐴 ∈ 𝑋 )
4		simplr2	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → 𝐵 ∈ 𝑋 )
5		simplr3	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → 𝐶 ∈ 𝑋 )
6	4 5	ifcld	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∈ 𝑋 )
7	3 6 4	3jca	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → ( 𝐴 ∈ 𝑋 ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
8		simpr	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) )
9		simpll	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → 𝑅 Or 𝑋 )
10		somin1	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ( 𝑅 ∪ I ) 𝐵 )
11	9 4 5 10	syl12anc	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ( 𝑅 ∪ I ) 𝐵 )
12		poltletr	⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ( 𝑅 ∪ I ) 𝐵 ) → 𝐴 𝑅 𝐵 ) )
13	12	imp	⊢ ( ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ( 𝑅 ∪ I ) 𝐵 ) ) → 𝐴 𝑅 𝐵 )
14	2 7 8 11 13	syl22anc	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → 𝐴 𝑅 𝐵 )
15	3 6 5	3jca	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → ( 𝐴 ∈ 𝑋 ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) )
16		somin2	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ( 𝑅 ∪ I ) 𝐶 )
17	9 4 5 16	syl12anc	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ( 𝑅 ∪ I ) 𝐶 )
18		poltletr	⊢ ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ( 𝑅 ∪ I ) 𝐶 ) → 𝐴 𝑅 𝐶 ) )
19	18	imp	⊢ ( ( ( 𝑅 Po 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ∧ if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ( 𝑅 ∪ I ) 𝐶 ) ) → 𝐴 𝑅 𝐶 )
20	2 15 8 17 19	syl22anc	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → 𝐴 𝑅 𝐶 )
21	14 20	jca	⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) → ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑅 𝐶 ) )
22	21	ex	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑅 𝐶 ) ) )
23		breq2	⊢ ( 𝐵 = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 𝑅 𝐵 ↔ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
24		breq2	⊢ ( 𝐶 = if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) → ( 𝐴 𝑅 𝐶 ↔ 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ) )
25	23 24	ifboth	⊢ ( ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑅 𝐶 ) → 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) )
26	22 25	impbid1	⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑅 if ( 𝐵 𝑅 𝐶 , 𝐵 , 𝐶 ) ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑅 𝐶 ) ) )