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 ⊢φ→ROrA
supcl.2 ⊢φ→∃x∈A∀y∈B¬xRy∧∀y∈AyRx→∃z∈ByRz
Assertion suplub ⊢φ→C∈A∧CRsupBAR→∃z∈BCRz

Proof

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