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 ⊢ROrX∧A∈X∧B∈X→ifARBABR∪IA

Proof

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