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 ⊢ R Or X ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A R if B R C B C ↔ A R B ∧ A R C

Proof

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