Metamath Proof Explorer

Theorem infpr

Description: The infimum of a pair. (Contributed by AV, 4-Sep-2020)

Ref Expression
Assertion infpr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → inf B C A R = if B R C B C

Proof

Step Hyp Ref Expression
1 simp1 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → R Or A
2 ifcl ⊢ B ∈ A ∧ C ∈ A → if B R C B C ∈ A
3 2 3adant1 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → if B R C B C ∈ A
4 ifpr ⊢ B ∈ A ∧ C ∈ A → if B R C B C ∈ B C
5 4 3adant1 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → if B R C B C ∈ B C
6 breq2 ⊢ B = if B R C B C → B R B ↔ B R if B R C B C
7 6 notbid ⊢ B = if B R C B C → ¬ B R B ↔ ¬ B R if B R C B C
8 breq2 ⊢ C = if B R C B C → B R C ↔ B R if B R C B C
9 8 notbid ⊢ C = if B R C B C → ¬ B R C ↔ ¬ B R if B R C B C
10 sonr ⊢ R Or A ∧ B ∈ A → ¬ B R B
11 10 3adant3 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R B
12 11 adantr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B R C → ¬ B R B
13 simpr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ ¬ B R C → ¬ B R C
14 7 9 12 13 ifbothda ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R if B R C B C
15 breq2 ⊢ B = if B R C B C → C R B ↔ C R if B R C B C
16 15 notbid ⊢ B = if B R C B C → ¬ C R B ↔ ¬ C R if B R C B C
17 breq2 ⊢ C = if B R C B C → C R C ↔ C R if B R C B C
18 17 notbid ⊢ C = if B R C B C → ¬ C R C ↔ ¬ C R if B R C B C
19 so2nr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R C ∧ C R B
20 19 3impb ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ B R C ∧ C R B
21 imnan ⊢ B R C → ¬ C R B ↔ ¬ B R C ∧ C R B
22 20 21 sylibr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → B R C → ¬ C R B
23 22 imp ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ B R C → ¬ C R B
24 sonr ⊢ R Or A ∧ C ∈ A → ¬ C R C
25 24 3adant2 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ C R C
26 25 adantr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ ¬ B R C → ¬ C R C
27 16 18 23 26 ifbothda ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ C R if B R C B C
28 breq1 ⊢ y = B → y R if B R C B C ↔ B R if B R C B C
29 28 notbid ⊢ y = B → ¬ y R if B R C B C ↔ ¬ B R if B R C B C
30 breq1 ⊢ y = C → y R if B R C B C ↔ C R if B R C B C
31 30 notbid ⊢ y = C → ¬ y R if B R C B C ↔ ¬ C R if B R C B C
32 29 31 ralprg ⊢ B ∈ A ∧ C ∈ A → ∀ y ∈ B C ¬ y R if B R C B C ↔ ¬ B R if B R C B C ∧ ¬ C R if B R C B C
33 32 3adant1 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ∀ y ∈ B C ¬ y R if B R C B C ↔ ¬ B R if B R C B C ∧ ¬ C R if B R C B C
34 14 27 33 mpbir2and ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ∀ y ∈ B C ¬ y R if B R C B C
35 34 r19.21bi ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ y ∈ B C → ¬ y R if B R C B C
36 1 3 5 35 infmin ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → inf B C A R = if B R C B C