Metamath Proof Explorer

Theorem suplub

Description: A supremum is the least upper bound. See also supcl and supub . (Contributed by NM, 13-Oct-2004) (Revised by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypotheses supmo.1 ⊢ φ → R Or A
supcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
Assertion suplub ⊢ φ → C ∈ A ∧ C R sup B A R → ∃ z ∈ B C R z

Proof

Step Hyp Ref Expression
1 supmo.1 ⊢ φ → R Or A
2 supcl.2 ⊢ φ → ∃ x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
3 simpr ⊢ ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∀ y ∈ A y R x → ∃ z ∈ B y R z
4 breq1 ⊢ y = w → y R x ↔ w R x
5 breq1 ⊢ y = w → y R z ↔ w R z
6 5 rexbidv ⊢ y = w → ∃ z ∈ B y R z ↔ ∃ z ∈ B w R z
7 4 6 imbi12d ⊢ y = w → y R x → ∃ z ∈ B y R z ↔ w R x → ∃ z ∈ B w R z
8 7 cbvralvw ⊢ ∀ y ∈ A y R x → ∃ z ∈ B y R z ↔ ∀ w ∈ A w R x → ∃ z ∈ B w R z
9 3 8 sylib ⊢ ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∀ w ∈ A w R x → ∃ z ∈ B w R z
10 9 a1i ⊢ x ∈ A → ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∀ w ∈ A w R x → ∃ z ∈ B w R z
11 10 ss2rabi ⊢ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ⊆ x ∈ A | ∀ w ∈ A w R x → ∃ z ∈ B w R z
12 1 supval2 ⊢ φ → sup B A R = ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
13 1 2 supeu ⊢ φ → ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
14 riotacl2 ⊢ ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ∈ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
15 13 14 syl ⊢ φ → ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ∈ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
16 12 15 eqeltrd ⊢ φ → sup B A R ∈ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
17 11 16 sselid ⊢ φ → sup B A R ∈ x ∈ A | ∀ w ∈ A w R x → ∃ z ∈ B w R z
18 breq2 ⊢ x = sup B A R → w R x ↔ w R sup B A R
19 18 imbi1d ⊢ x = sup B A R → w R x → ∃ z ∈ B w R z ↔ w R sup B A R → ∃ z ∈ B w R z
20 19 ralbidv ⊢ x = sup B A R → ∀ w ∈ A w R x → ∃ z ∈ B w R z ↔ ∀ w ∈ A w R sup B A R → ∃ z ∈ B w R z
21 20 elrab ⊢ sup B A R ∈ x ∈ A | ∀ w ∈ A w R x → ∃ z ∈ B w R z ↔ sup B A R ∈ A ∧ ∀ w ∈ A w R sup B A R → ∃ z ∈ B w R z
22 21 simprbi ⊢ sup B A R ∈ x ∈ A | ∀ w ∈ A w R x → ∃ z ∈ B w R z → ∀ w ∈ A w R sup B A R → ∃ z ∈ B w R z
23 17 22 syl ⊢ φ → ∀ w ∈ A w R sup B A R → ∃ z ∈ B w R z
24 breq1 ⊢ w = C → w R sup B A R ↔ C R sup B A R
25 breq1 ⊢ w = C → w R z ↔ C R z
26 25 rexbidv ⊢ w = C → ∃ z ∈ B w R z ↔ ∃ z ∈ B C R z
27 24 26 imbi12d ⊢ w = C → w R sup B A R → ∃ z ∈ B w R z ↔ C R sup B A R → ∃ z ∈ B C R z
28 27 rspccv ⊢ ∀ w ∈ A w R sup B A R → ∃ z ∈ B w R z → C ∈ A → C R sup B A R → ∃ z ∈ B C R z
29 28 impd ⊢ ∀ w ∈ A w R sup B A R → ∃ z ∈ B w R z → C ∈ A ∧ C R sup B A R → ∃ z ∈ B C R z
30 23 29 syl ⊢ φ → C ∈ A ∧ C R sup B A R → ∃ z ∈ B C R z