Metamath Proof Explorer

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 ⊢ROrX∧A∈X∧B∈X∧C∈X→ARifBRCBC↔ARB∧ARC

Proof

Step Hyp Ref Expression
1 sopo ⊢ROrX→RPoX
2 1 ad2antrr ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→RPoX
3 simplr1 ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→A∈X
4 simplr2 ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→B∈X
5 simplr3 ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→C∈X
6 4 5 ifcld ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→ifBRCBC∈X
7 3 6 4 3jca ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→A∈X∧ifBRCBC∈X∧B∈X
8 simpr ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→ARifBRCBC
9 simpll ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→ROrX
10 somin1 ⊢ROrX∧B∈X∧C∈X→ifBRCBCR∪IB
11 9 4 5 10 syl12anc ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→ifBRCBCR∪IB
12 poltletr ⊢RPoX∧A∈X∧ifBRCBC∈X∧B∈X→ARifBRCBC∧ifBRCBCR∪IB→ARB
13 12 imp ⊢RPoX∧A∈X∧ifBRCBC∈X∧B∈X∧ARifBRCBC∧ifBRCBCR∪IB→ARB
14 2 7 8 11 13 syl22anc ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→ARB
15 3 6 5 3jca ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→A∈X∧ifBRCBC∈X∧C∈X
16 somin2 ⊢ROrX∧B∈X∧C∈X→ifBRCBCR∪IC
17 9 4 5 16 syl12anc ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→ifBRCBCR∪IC
18 poltletr ⊢RPoX∧A∈X∧ifBRCBC∈X∧C∈X→ARifBRCBC∧ifBRCBCR∪IC→ARC
19 18 imp ⊢RPoX∧A∈X∧ifBRCBC∈X∧C∈X∧ARifBRCBC∧ifBRCBCR∪IC→ARC
20 2 15 8 17 19 syl22anc ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→ARC
21 14 20 jca ⊢ROrX∧A∈X∧B∈X∧C∈X∧ARifBRCBC→ARB∧ARC
22 21 ex ⊢ROrX∧A∈X∧B∈X∧C∈X→ARifBRCBC→ARB∧ARC
23 breq2 ⊢B=ifBRCBC→ARB↔ARifBRCBC
24 breq2 ⊢C=ifBRCBC→ARC↔ARifBRCBC
25 23 24 ifboth ⊢ARB∧ARC→ARifBRCBC
26 22 25 impbid1 ⊢ROrX∧A∈X∧B∈X∧C∈X→ARifBRCBC↔ARB∧ARC