Metamath Proof Explorer

Theorem supub

Description: A supremum is an upper bound. See also supcl and suplub .

This proof demonstrates how to expand an iota-based definition ( df-iota ) using riotacl2 .

(Contributed by NM, 12-Oct-2004) (Proof shortened 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 supub ⊢ φ → C ∈ B → ¬ sup B A R R C

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 simpl ⊢ ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∀ y ∈ B ¬ x R y
4 3 a1i ⊢ x ∈ A → ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z → ∀ y ∈ B ¬ x R y
5 4 ss2rabi ⊢ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z ⊆ x ∈ A | ∀ y ∈ B ¬ x R y
6 1 supval2 ⊢ φ → sup B A R = ι x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
7 1 2 supeu ⊢ φ → ∃! x ∈ A ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
8 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
9 7 8 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
10 6 9 eqeltrd ⊢ φ → sup B A R ∈ x ∈ A | ∀ y ∈ B ¬ x R y ∧ ∀ y ∈ A y R x → ∃ z ∈ B y R z
11 5 10 sselid ⊢ φ → sup B A R ∈ x ∈ A | ∀ y ∈ B ¬ x R y
12 breq2 ⊢ y = w → x R y ↔ x R w
13 12 notbid ⊢ y = w → ¬ x R y ↔ ¬ x R w
14 13 cbvralvw ⊢ ∀ y ∈ B ¬ x R y ↔ ∀ w ∈ B ¬ x R w
15 breq1 ⊢ x = sup B A R → x R w ↔ sup B A R R w
16 15 notbid ⊢ x = sup B A R → ¬ x R w ↔ ¬ sup B A R R w
17 16 ralbidv ⊢ x = sup B A R → ∀ w ∈ B ¬ x R w ↔ ∀ w ∈ B ¬ sup B A R R w
18 14 17 bitrid ⊢ x = sup B A R → ∀ y ∈ B ¬ x R y ↔ ∀ w ∈ B ¬ sup B A R R w
19 18 elrab ⊢ sup B A R ∈ x ∈ A | ∀ y ∈ B ¬ x R y ↔ sup B A R ∈ A ∧ ∀ w ∈ B ¬ sup B A R R w
20 19 simprbi ⊢ sup B A R ∈ x ∈ A | ∀ y ∈ B ¬ x R y → ∀ w ∈ B ¬ sup B A R R w
21 11 20 syl ⊢ φ → ∀ w ∈ B ¬ sup B A R R w
22 breq2 ⊢ w = C → sup B A R R w ↔ sup B A R R C
23 22 notbid ⊢ w = C → ¬ sup B A R R w ↔ ¬ sup B A R R C
24 23 rspccv ⊢ ∀ w ∈ B ¬ sup B A R R w → C ∈ B → ¬ sup B A R R C
25 21 24 syl ⊢ φ → C ∈ B → ¬ sup B A R R C