# Metamath Proof Explorer

## Theorem suplem2pr

Description: The union of a set of positive reals (if a positive real) is its supremum (the least upper bound). Part of Proposition 9-3.3 of Gleason p. 122. (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion suplem2pr ${⊢}{A}\subseteq 𝑷\to \left(\left({y}\in {A}\to ¬\bigcup {A}{<}_{𝑷}{y}\right)\wedge \left({y}{<}_{𝑷}\bigcup {A}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ltrelpr ${⊢}{<}_{𝑷}\subseteq 𝑷×𝑷$
2 1 brel ${⊢}{y}{<}_{𝑷}\bigcup {A}\to \left({y}\in 𝑷\wedge \bigcup {A}\in 𝑷\right)$
3 2 simpld ${⊢}{y}{<}_{𝑷}\bigcup {A}\to {y}\in 𝑷$
4 ralnex ${⊢}\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{<}_{𝑷}{z}↔¬\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}$
5 ssel2 ${⊢}\left({A}\subseteq 𝑷\wedge {z}\in {A}\right)\to {z}\in 𝑷$
6 ltsopr ${⊢}{<}_{𝑷}\mathrm{Or}𝑷$
7 sotric ${⊢}\left({<}_{𝑷}\mathrm{Or}𝑷\wedge \left({y}\in 𝑷\wedge {z}\in 𝑷\right)\right)\to \left({y}{<}_{𝑷}{z}↔¬\left({y}={z}\vee {z}{<}_{𝑷}{y}\right)\right)$
8 6 7 mpan ${⊢}\left({y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left({y}{<}_{𝑷}{z}↔¬\left({y}={z}\vee {z}{<}_{𝑷}{y}\right)\right)$
9 8 con2bid ${⊢}\left({y}\in 𝑷\wedge {z}\in 𝑷\right)\to \left(\left({y}={z}\vee {z}{<}_{𝑷}{y}\right)↔¬{y}{<}_{𝑷}{z}\right)$
10 9 ancoms ${⊢}\left({z}\in 𝑷\wedge {y}\in 𝑷\right)\to \left(\left({y}={z}\vee {z}{<}_{𝑷}{y}\right)↔¬{y}{<}_{𝑷}{z}\right)$
11 ltprord ${⊢}\left({z}\in 𝑷\wedge {y}\in 𝑷\right)\to \left({z}{<}_{𝑷}{y}↔{z}\subset {y}\right)$
12 11 orbi2d ${⊢}\left({z}\in 𝑷\wedge {y}\in 𝑷\right)\to \left(\left({y}={z}\vee {z}{<}_{𝑷}{y}\right)↔\left({y}={z}\vee {z}\subset {y}\right)\right)$
13 sspss ${⊢}{z}\subseteq {y}↔\left({z}\subset {y}\vee {z}={y}\right)$
14 equcom ${⊢}{z}={y}↔{y}={z}$
15 14 orbi2i ${⊢}\left({z}\subset {y}\vee {z}={y}\right)↔\left({z}\subset {y}\vee {y}={z}\right)$
16 orcom ${⊢}\left({z}\subset {y}\vee {y}={z}\right)↔\left({y}={z}\vee {z}\subset {y}\right)$
17 13 15 16 3bitri ${⊢}{z}\subseteq {y}↔\left({y}={z}\vee {z}\subset {y}\right)$
18 12 17 syl6bbr ${⊢}\left({z}\in 𝑷\wedge {y}\in 𝑷\right)\to \left(\left({y}={z}\vee {z}{<}_{𝑷}{y}\right)↔{z}\subseteq {y}\right)$
19 10 18 bitr3d ${⊢}\left({z}\in 𝑷\wedge {y}\in 𝑷\right)\to \left(¬{y}{<}_{𝑷}{z}↔{z}\subseteq {y}\right)$
20 5 19 sylan ${⊢}\left(\left({A}\subseteq 𝑷\wedge {z}\in {A}\right)\wedge {y}\in 𝑷\right)\to \left(¬{y}{<}_{𝑷}{z}↔{z}\subseteq {y}\right)$
21 20 an32s ${⊢}\left(\left({A}\subseteq 𝑷\wedge {y}\in 𝑷\right)\wedge {z}\in {A}\right)\to \left(¬{y}{<}_{𝑷}{z}↔{z}\subseteq {y}\right)$
22 21 ralbidva ${⊢}\left({A}\subseteq 𝑷\wedge {y}\in 𝑷\right)\to \left(\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}¬{y}{<}_{𝑷}{z}↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}\right)$
23 4 22 syl5bbr ${⊢}\left({A}\subseteq 𝑷\wedge {y}\in 𝑷\right)\to \left(¬\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}\right)$
24 unissb ${⊢}\bigcup {A}\subseteq {y}↔\forall {z}\in {A}\phantom{\rule{.4em}{0ex}}{z}\subseteq {y}$
25 23 24 syl6bbr ${⊢}\left({A}\subseteq 𝑷\wedge {y}\in 𝑷\right)\to \left(¬\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}↔\bigcup {A}\subseteq {y}\right)$
26 ssnpss ${⊢}\bigcup {A}\subseteq {y}\to ¬{y}\subset \bigcup {A}$
27 ltprord ${⊢}\left({y}\in 𝑷\wedge \bigcup {A}\in 𝑷\right)\to \left({y}{<}_{𝑷}\bigcup {A}↔{y}\subset \bigcup {A}\right)$
28 27 biimpd ${⊢}\left({y}\in 𝑷\wedge \bigcup {A}\in 𝑷\right)\to \left({y}{<}_{𝑷}\bigcup {A}\to {y}\subset \bigcup {A}\right)$
29 2 28 mpcom ${⊢}{y}{<}_{𝑷}\bigcup {A}\to {y}\subset \bigcup {A}$
30 26 29 nsyl ${⊢}\bigcup {A}\subseteq {y}\to ¬{y}{<}_{𝑷}\bigcup {A}$
31 25 30 syl6bi ${⊢}\left({A}\subseteq 𝑷\wedge {y}\in 𝑷\right)\to \left(¬\exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}\to ¬{y}{<}_{𝑷}\bigcup {A}\right)$
32 31 con4d ${⊢}\left({A}\subseteq 𝑷\wedge {y}\in 𝑷\right)\to \left({y}{<}_{𝑷}\bigcup {A}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}\right)$
33 32 ex ${⊢}{A}\subseteq 𝑷\to \left({y}\in 𝑷\to \left({y}{<}_{𝑷}\bigcup {A}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}\right)\right)$
34 3 33 syl5 ${⊢}{A}\subseteq 𝑷\to \left({y}{<}_{𝑷}\bigcup {A}\to \left({y}{<}_{𝑷}\bigcup {A}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}\right)\right)$
35 34 pm2.43d ${⊢}{A}\subseteq 𝑷\to \left({y}{<}_{𝑷}\bigcup {A}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}\right)$
36 elssuni ${⊢}{y}\in {A}\to {y}\subseteq \bigcup {A}$
37 ssnpss ${⊢}{y}\subseteq \bigcup {A}\to ¬\bigcup {A}\subset {y}$
38 36 37 syl ${⊢}{y}\in {A}\to ¬\bigcup {A}\subset {y}$
39 1 brel ${⊢}\bigcup {A}{<}_{𝑷}{y}\to \left(\bigcup {A}\in 𝑷\wedge {y}\in 𝑷\right)$
40 ltprord ${⊢}\left(\bigcup {A}\in 𝑷\wedge {y}\in 𝑷\right)\to \left(\bigcup {A}{<}_{𝑷}{y}↔\bigcup {A}\subset {y}\right)$
41 40 biimpd ${⊢}\left(\bigcup {A}\in 𝑷\wedge {y}\in 𝑷\right)\to \left(\bigcup {A}{<}_{𝑷}{y}\to \bigcup {A}\subset {y}\right)$
42 39 41 mpcom ${⊢}\bigcup {A}{<}_{𝑷}{y}\to \bigcup {A}\subset {y}$
43 38 42 nsyl ${⊢}{y}\in {A}\to ¬\bigcup {A}{<}_{𝑷}{y}$
44 35 43 jctil ${⊢}{A}\subseteq 𝑷\to \left(\left({y}\in {A}\to ¬\bigcup {A}{<}_{𝑷}{y}\right)\wedge \left({y}{<}_{𝑷}\bigcup {A}\to \exists {z}\in {A}\phantom{\rule{.4em}{0ex}}{y}{<}_{𝑷}{z}\right)\right)$