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 breq1 ⊢ y = w → y R x ↔ w R x
4 breq1 ⊢ y = w → y R z ↔ w R z
5 4 rexbidv ⊢ y = w → ∃ z ∈ B y R z ↔ ∃ z ∈ B w R z
6 3 5 imbi12d ⊢ y = w → y R x → ∃ z ∈ B y R z ↔ w R x → ∃ z ∈ B w R z
7 6 cbvralvw ⊢ ∀ y ∈ A y R x → ∃ z ∈ B y R z ↔ ∀ w ∈ A w R x → ∃ z ∈ B w R z
8 7 bilani ⊢ ∀ 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
9 8 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
10 9 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
11 1 supval2 ⊢ φ → sup B A R = ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
12 1 2 supeu ⊢ φ → ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
13 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
14 12 13 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
15 11 14 eqeltrd ⊢ φ → sup B A R ∈ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
16 10 15 sselid ⊢ φ → sup B A R ∈ x ∈ A | ∀ w ∈ A w R x → ∃ z ∈ B w R z
17 breq2 ⊢ x = sup B A R → w R x ↔ w R sup B A R
18 17 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
19 18 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
20 19 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
21 20 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
22 16 21 syl ⊢ φ → ∀ w ∈ A w R sup B A R → ∃ z ∈ B w R z
23 breq1 ⊢ w = C → w R sup B A R ↔ C R sup B A R
24 breq1 ⊢ w = C → w R z ↔ C R z
25 24 rexbidv ⊢ w = C → ∃ z ∈ B w R z ↔ ∃ z ∈ B C R z
26 23 25 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
27 26 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
28 27 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
29 22 28 syl ⊢ φ → C ∈ A ∧ C R sup B A R → ∃ z ∈ B C R z