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

Metamath Proof Explorer

Theorem somin1

Description: Property of a minimum in a strict order. (Contributed by Stefan O'Rear, 17-Jan-2015)

Ref Expression
Assertion somin1 ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) ( 𝑅 ∪ I ) 𝐴 )

Proof

Step Hyp Ref Expression
1 iftrue ⊢ ( 𝐴 𝑅 𝐵 → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 )
2 1 olcd ⊢ ( 𝐴 𝑅 𝐵 → ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) )
3 2 adantl ⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ 𝐴 𝑅 𝐵 ) → ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) )
4 sotric ⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) ) )
5 orcom ⊢ ( ( 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) ↔ ( 𝐵 𝑅 𝐴 ∨ 𝐴 = 𝐵 ) )
6 eqcom ⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
7 6 orbi2i ⊢ ( ( 𝐵 𝑅 𝐴 ∨ 𝐴 = 𝐵 ) ↔ ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) )
8 5 7 bitri ⊢ ( ( 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) ↔ ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) )
9 8 notbii ⊢ ( ¬ ( 𝐴 = 𝐵 ∨ 𝐵 𝑅 𝐴 ) ↔ ¬ ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) )
10 4 9 bitrdi ⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝑅 𝐵 ↔ ¬ ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) ) )
11 10 con2bid ⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ¬ 𝐴 𝑅 𝐵 ) )
12 11 biimpar ⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ¬ 𝐴 𝑅 𝐵 ) → ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) )
13 iffalse ⊢ ( ¬ 𝐴 𝑅 𝐵 → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐵 )
14 breq1 ⊢ ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐵 → ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ↔ 𝐵 𝑅 𝐴 ) )
15 eqeq1 ⊢ ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐵 → ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ↔ 𝐵 = 𝐴 ) )
16 14 15 orbi12d ⊢ ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐵 → ( ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) ↔ ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) ) )
17 13 16 syl ⊢ ( ¬ 𝐴 𝑅 𝐵 → ( ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) ↔ ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) ) )
18 17 adantl ⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ¬ 𝐴 𝑅 𝐵 ) → ( ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) ↔ ( 𝐵 𝑅 𝐴 ∨ 𝐵 = 𝐴 ) ) )
19 12 18 mpbird ⊢ ( ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ¬ 𝐴 𝑅 𝐵 ) → ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) )
20 3 19 pm2.61dan ⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) )
21 poleloe ⊢ ( 𝐴 ∈ 𝑋 → ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) ( 𝑅 ∪ I ) 𝐴 ↔ ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) ) )
22 21 ad2antrl ⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) ( 𝑅 ∪ I ) 𝐴 ↔ ( if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) 𝑅 𝐴 ∨ if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) = 𝐴 ) ) )
23 20 22 mpbird ⊢ ( ( 𝑅 Or 𝑋 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → if ( 𝐴 𝑅 𝐵 , 𝐴 , 𝐵 ) ( 𝑅 ∪ I ) 𝐴 )