Metamath Proof Explorer

Theorem suppr

Description: The supremum of a pair. (Contributed by NM, 17-Jun-2007) (Proof shortened by Mario Carneiro, 24-Dec-2016)

Ref Expression
Assertion suppr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → sup B C A R = if C R B 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 C R B B C ∈ A
3 2 3adant1 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → if C R B B C ∈ A
4 ifpr ⊢ B ∈ A ∧ C ∈ A → if C R B B C ∈ B C
5 4 3adant1 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → if C R B B C ∈ B C
6 breq1 ⊢ B = if C R B B C → B R B ↔ if C R B B C R B
7 6 notbid ⊢ B = if C R B B C → ¬ B R B ↔ ¬ if C R B B C R B
8 breq1 ⊢ C = if C R B B C → C R B ↔ if C R B B C R B
9 8 notbid ⊢ C = if C R B B C → ¬ C R B ↔ ¬ if C R B B C R B
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 ∧ C R B → ¬ B R B
13 simpr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ ¬ C R B → ¬ C R B
14 7 9 12 13 ifbothda ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ if C R B B C R B
15 breq1 ⊢ B = if C R B B C → B R C ↔ if C R B B C R C
16 15 notbid ⊢ B = if C R B B C → ¬ B R C ↔ ¬ if C R B B C R C
17 breq1 ⊢ C = if C R B B C → C R C ↔ if C R B B C R C
18 17 notbid ⊢ C = if C R B B C → ¬ C R C ↔ ¬ if C R B B C R C
19 so2nr ⊢ R Or A ∧ C ∈ A ∧ B ∈ A → ¬ C R B ∧ B R C
20 19 3impb ⊢ R Or A ∧ C ∈ A ∧ B ∈ A → ¬ C R B ∧ B R C
21 20 3com23 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ C R B ∧ B R C
22 imnan ⊢ C R B → ¬ B R C ↔ ¬ C R B ∧ B R C
23 21 22 sylibr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → C R B → ¬ B R C
24 23 imp ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ C R B → ¬ B R C
25 sonr ⊢ R Or A ∧ C ∈ A → ¬ C R C
26 25 3adant2 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ C R C
27 26 adantr ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ ¬ C R B → ¬ C R C
28 16 18 24 27 ifbothda ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ¬ if C R B B C R C
29 breq2 ⊢ y = B → if C R B B C R y ↔ if C R B B C R B
30 29 notbid ⊢ y = B → ¬ if C R B B C R y ↔ ¬ if C R B B C R B
31 breq2 ⊢ y = C → if C R B B C R y ↔ if C R B B C R C
32 31 notbid ⊢ y = C → ¬ if C R B B C R y ↔ ¬ if C R B B C R C
33 30 32 ralprg ⊢ B ∈ A ∧ C ∈ A → ∀ y ∈ B C ¬ if C R B B C R y ↔ ¬ if C R B B C R B ∧ ¬ if C R B B C R C
34 33 3adant1 ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ∀ y ∈ B C ¬ if C R B B C R y ↔ ¬ if C R B B C R B ∧ ¬ if C R B B C R C
35 14 28 34 mpbir2and ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → ∀ y ∈ B C ¬ if C R B B C R y
36 35 r19.21bi ⊢ R Or A ∧ B ∈ A ∧ C ∈ A ∧ y ∈ B C → ¬ if C R B B C R y
37 1 3 5 36 supmax ⊢ R Or A ∧ B ∈ A ∧ C ∈ A → sup B C A R = if C R B B C