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

Proof

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