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

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