Metamath Proof Explorer

Theorem axpre-sup

Description: A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version with ordering on extended reals is axsup . This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup . (Contributed by NM, 19-May-1996) (Revised by Mario Carneiro, 16-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion axpre-sup ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay<ℝx→∃x∈ℝ∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz

Proof

Step Hyp Ref Expression
1 elreal2 ⊢x∈ℝ↔1st⁡x∈𝑹∧x=1st⁡x0𝑹
2 1 simplbi ⊢x∈ℝ→1st⁡x∈𝑹
3 2 adantl ⊢A⊆ℝ∧A≠∅∧x∈ℝ→1st⁡x∈𝑹
4 fo1st ⊢1st:V⟶ontoV
5 fof ⊢1st:V⟶ontoV→1st:V⟶V
6 ffn ⊢1st:V⟶V→1stFnV
7 4 5 6 mp2b ⊢1stFnV
8 ssv ⊢A⊆V
9 fvelimab ⊢1stFnV∧A⊆V→w∈1stA↔∃y∈A1st⁡y=w
10 7 8 9 mp2an ⊢w∈1stA↔∃y∈A1st⁡y=w
11 r19.29 ⊢∀y∈Ay<ℝx∧∃y∈A1st⁡y=w→∃y∈Ay<ℝx∧1st⁡y=w
12 ssel2 ⊢A⊆ℝ∧y∈A→y∈ℝ
13 ltresr2 ⊢y∈ℝ∧x∈ℝ→y<ℝx↔1st⁡y<𝑹1st⁡x
14 breq1 ⊢1st⁡y=w→1st⁡y<𝑹1st⁡x↔w<𝑹1st⁡x
15 13 14 sylan9bb ⊢y∈ℝ∧x∈ℝ∧1st⁡y=w→y<ℝx↔w<𝑹1st⁡x
16 15 biimpd ⊢y∈ℝ∧x∈ℝ∧1st⁡y=w→y<ℝx→w<𝑹1st⁡x
17 16 exp31 ⊢y∈ℝ→x∈ℝ→1st⁡y=w→y<ℝx→w<𝑹1st⁡x
18 12 17 syl ⊢A⊆ℝ∧y∈A→x∈ℝ→1st⁡y=w→y<ℝx→w<𝑹1st⁡x
19 18 imp4b ⊢A⊆ℝ∧y∈A∧x∈ℝ→1st⁡y=w∧y<ℝx→w<𝑹1st⁡x
20 19 ancomsd ⊢A⊆ℝ∧y∈A∧x∈ℝ→y<ℝx∧1st⁡y=w→w<𝑹1st⁡x
21 20 an32s ⊢A⊆ℝ∧x∈ℝ∧y∈A→y<ℝx∧1st⁡y=w→w<𝑹1st⁡x
22 21 rexlimdva ⊢A⊆ℝ∧x∈ℝ→∃y∈Ay<ℝx∧1st⁡y=w→w<𝑹1st⁡x
23 11 22 syl5 ⊢A⊆ℝ∧x∈ℝ→∀y∈Ay<ℝx∧∃y∈A1st⁡y=w→w<𝑹1st⁡x
24 23 expd ⊢A⊆ℝ∧x∈ℝ→∀y∈Ay<ℝx→∃y∈A1st⁡y=w→w<𝑹1st⁡x
25 10 24 syl7bi ⊢A⊆ℝ∧x∈ℝ→∀y∈Ay<ℝx→w∈1stA→w<𝑹1st⁡x
26 25 impr ⊢A⊆ℝ∧x∈ℝ∧∀y∈Ay<ℝx→w∈1stA→w<𝑹1st⁡x
27 26 adantlr ⊢A⊆ℝ∧A≠∅∧x∈ℝ∧∀y∈Ay<ℝx→w∈1stA→w<𝑹1st⁡x
28 27 ralrimiv ⊢A⊆ℝ∧A≠∅∧x∈ℝ∧∀y∈Ay<ℝx→∀w∈1stAw<𝑹1st⁡x
29 28 expr ⊢A⊆ℝ∧A≠∅∧x∈ℝ→∀y∈Ay<ℝx→∀w∈1stAw<𝑹1st⁡x
30 brralrspcev ⊢1st⁡x∈𝑹∧∀w∈1stAw<𝑹1st⁡x→∃v∈𝑹∀w∈1stAw<𝑹v
31 3 29 30 syl6an ⊢A⊆ℝ∧A≠∅∧x∈ℝ→∀y∈Ay<ℝx→∃v∈𝑹∀w∈1stAw<𝑹v
32 31 rexlimdva ⊢A⊆ℝ∧A≠∅→∃x∈ℝ∀y∈Ay<ℝx→∃v∈𝑹∀w∈1stAw<𝑹v
33 n0 ⊢A≠∅↔∃yy∈A
34 fnfvima ⊢1stFnV∧A⊆V∧y∈A→1st⁡y∈1stA
35 7 8 34 mp3an12 ⊢y∈A→1st⁡y∈1stA
36 35 ne0d ⊢y∈A→1stA≠∅
37 36 exlimiv ⊢∃yy∈A→1stA≠∅
38 33 37 sylbi ⊢A≠∅→1stA≠∅
39 supsr ⊢1stA≠∅∧∃v∈𝑹∀w∈1stAw<𝑹v→∃v∈𝑹∀w∈1stA¬v<𝑹w∧∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u
40 39 ex ⊢1stA≠∅→∃v∈𝑹∀w∈1stAw<𝑹v→∃v∈𝑹∀w∈1stA¬v<𝑹w∧∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u
41 38 40 syl ⊢A≠∅→∃v∈𝑹∀w∈1stAw<𝑹v→∃v∈𝑹∀w∈1stA¬v<𝑹w∧∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u
42 41 adantl ⊢A⊆ℝ∧A≠∅→∃v∈𝑹∀w∈1stAw<𝑹v→∃v∈𝑹∀w∈1stA¬v<𝑹w∧∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u
43 breq2 ⊢w=1st⁡y→v<𝑹w↔v<𝑹1st⁡y
44 43 notbid ⊢w=1st⁡y→¬v<𝑹w↔¬v<𝑹1st⁡y
45 44 rspccv ⊢∀w∈1stA¬v<𝑹w→1st⁡y∈1stA→¬v<𝑹1st⁡y
46 35 45 syl5com ⊢y∈A→∀w∈1stA¬v<𝑹w→¬v<𝑹1st⁡y
47 46 adantl ⊢A⊆ℝ∧y∈A→∀w∈1stA¬v<𝑹w→¬v<𝑹1st⁡y
48 elreal2 ⊢y∈ℝ↔1st⁡y∈𝑹∧y=1st⁡y0𝑹
49 48 simprbi ⊢y∈ℝ→y=1st⁡y0𝑹
50 49 breq2d ⊢y∈ℝ→v0𝑹<ℝy↔v0𝑹<ℝ1st⁡y0𝑹
51 ltresr ⊢v0𝑹<ℝ1st⁡y0𝑹↔v<𝑹1st⁡y
52 50 51 bitrdi ⊢y∈ℝ→v0𝑹<ℝy↔v<𝑹1st⁡y
53 12 52 syl ⊢A⊆ℝ∧y∈A→v0𝑹<ℝy↔v<𝑹1st⁡y
54 53 notbid ⊢A⊆ℝ∧y∈A→¬v0𝑹<ℝy↔¬v<𝑹1st⁡y
55 47 54 sylibrd ⊢A⊆ℝ∧y∈A→∀w∈1stA¬v<𝑹w→¬v0𝑹<ℝy
56 55 ralrimdva ⊢A⊆ℝ→∀w∈1stA¬v<𝑹w→∀y∈A¬v0𝑹<ℝy
57 56 ad2antrr ⊢A⊆ℝ∧A≠∅∧v∈𝑹→∀w∈1stA¬v<𝑹w→∀y∈A¬v0𝑹<ℝy
58 49 breq1d ⊢y∈ℝ→y<ℝv0𝑹↔1st⁡y0𝑹<ℝv0𝑹
59 ltresr ⊢1st⁡y0𝑹<ℝv0𝑹↔1st⁡y<𝑹v
60 58 59 bitrdi ⊢y∈ℝ→y<ℝv0𝑹↔1st⁡y<𝑹v
61 48 simplbi ⊢y∈ℝ→1st⁡y∈𝑹
62 breq1 ⊢w=1st⁡y→w<𝑹v↔1st⁡y<𝑹v
63 breq1 ⊢w=1st⁡y→w<𝑹u↔1st⁡y<𝑹u
64 63 rexbidv ⊢w=1st⁡y→∃u∈1stAw<𝑹u↔∃u∈1stA1st⁡y<𝑹u
65 62 64 imbi12d ⊢w=1st⁡y→w<𝑹v→∃u∈1stAw<𝑹u↔1st⁡y<𝑹v→∃u∈1stA1st⁡y<𝑹u
66 65 rspccv ⊢∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→1st⁡y∈𝑹→1st⁡y<𝑹v→∃u∈1stA1st⁡y<𝑹u
67 61 66 syl5 ⊢∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→y∈ℝ→1st⁡y<𝑹v→∃u∈1stA1st⁡y<𝑹u
68 67 com3l ⊢y∈ℝ→1st⁡y<𝑹v→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→∃u∈1stA1st⁡y<𝑹u
69 60 68 sylbid ⊢y∈ℝ→y<ℝv0𝑹→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→∃u∈1stA1st⁡y<𝑹u
70 69 adantr ⊢y∈ℝ∧A⊆ℝ→y<ℝv0𝑹→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→∃u∈1stA1st⁡y<𝑹u
71 fvelimab ⊢1stFnV∧A⊆V→u∈1stA↔∃z∈A1st⁡z=u
72 7 8 71 mp2an ⊢u∈1stA↔∃z∈A1st⁡z=u
73 ssel2 ⊢A⊆ℝ∧z∈A→z∈ℝ
74 ltresr2 ⊢y∈ℝ∧z∈ℝ→y<ℝz↔1st⁡y<𝑹1st⁡z
75 73 74 sylan2 ⊢y∈ℝ∧A⊆ℝ∧z∈A→y<ℝz↔1st⁡y<𝑹1st⁡z
76 breq2 ⊢1st⁡z=u→1st⁡y<𝑹1st⁡z↔1st⁡y<𝑹u
77 75 76 sylan9bb ⊢y∈ℝ∧A⊆ℝ∧z∈A∧1st⁡z=u→y<ℝz↔1st⁡y<𝑹u
78 77 exbiri ⊢y∈ℝ∧A⊆ℝ∧z∈A→1st⁡z=u→1st⁡y<𝑹u→y<ℝz
79 78 expr ⊢y∈ℝ∧A⊆ℝ→z∈A→1st⁡z=u→1st⁡y<𝑹u→y<ℝz
80 79 com4r ⊢1st⁡y<𝑹u→y∈ℝ∧A⊆ℝ→z∈A→1st⁡z=u→y<ℝz
81 80 imp ⊢1st⁡y<𝑹u∧y∈ℝ∧A⊆ℝ→z∈A→1st⁡z=u→y<ℝz
82 81 reximdvai ⊢1st⁡y<𝑹u∧y∈ℝ∧A⊆ℝ→∃z∈A1st⁡z=u→∃z∈Ay<ℝz
83 72 82 biimtrid ⊢1st⁡y<𝑹u∧y∈ℝ∧A⊆ℝ→u∈1stA→∃z∈Ay<ℝz
84 83 expcom ⊢y∈ℝ∧A⊆ℝ→1st⁡y<𝑹u→u∈1stA→∃z∈Ay<ℝz
85 84 com23 ⊢y∈ℝ∧A⊆ℝ→u∈1stA→1st⁡y<𝑹u→∃z∈Ay<ℝz
86 85 rexlimdv ⊢y∈ℝ∧A⊆ℝ→∃u∈1stA1st⁡y<𝑹u→∃z∈Ay<ℝz
87 70 86 syl6d ⊢y∈ℝ∧A⊆ℝ→y<ℝv0𝑹→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→∃z∈Ay<ℝz
88 87 com23 ⊢y∈ℝ∧A⊆ℝ→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→y<ℝv0𝑹→∃z∈Ay<ℝz
89 88 ex ⊢y∈ℝ→A⊆ℝ→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→y<ℝv0𝑹→∃z∈Ay<ℝz
90 89 com3l ⊢A⊆ℝ→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→y∈ℝ→y<ℝv0𝑹→∃z∈Ay<ℝz
91 90 ad2antrr ⊢A⊆ℝ∧A≠∅∧v∈𝑹→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→y∈ℝ→y<ℝv0𝑹→∃z∈Ay<ℝz
92 91 ralrimdv ⊢A⊆ℝ∧A≠∅∧v∈𝑹→∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→∀y∈ℝy<ℝv0𝑹→∃z∈Ay<ℝz
93 opelreal ⊢v0𝑹∈ℝ↔v∈𝑹
94 93 biimpri ⊢v∈𝑹→v0𝑹∈ℝ
95 94 adantl ⊢A⊆ℝ∧A≠∅∧v∈𝑹→v0𝑹∈ℝ
96 breq1 ⊢x=v0𝑹→x<ℝy↔v0𝑹<ℝy
97 96 notbid ⊢x=v0𝑹→¬x<ℝy↔¬v0𝑹<ℝy
98 97 ralbidv ⊢x=v0𝑹→∀y∈A¬x<ℝy↔∀y∈A¬v0𝑹<ℝy
99 breq2 ⊢x=v0𝑹→y<ℝx↔y<ℝv0𝑹
100 99 imbi1d ⊢x=v0𝑹→y<ℝx→∃z∈Ay<ℝz↔y<ℝv0𝑹→∃z∈Ay<ℝz
101 100 ralbidv ⊢x=v0𝑹→∀y∈ℝy<ℝx→∃z∈Ay<ℝz↔∀y∈ℝy<ℝv0𝑹→∃z∈Ay<ℝz
102 98 101 anbi12d ⊢x=v0𝑹→∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz↔∀y∈A¬v0𝑹<ℝy∧∀y∈ℝy<ℝv0𝑹→∃z∈Ay<ℝz
103 102 rspcev ⊢v0𝑹∈ℝ∧∀y∈A¬v0𝑹<ℝy∧∀y∈ℝy<ℝv0𝑹→∃z∈Ay<ℝz→∃x∈ℝ∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz
104 103 ex ⊢v0𝑹∈ℝ→∀y∈A¬v0𝑹<ℝy∧∀y∈ℝy<ℝv0𝑹→∃z∈Ay<ℝz→∃x∈ℝ∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz
105 95 104 syl ⊢A⊆ℝ∧A≠∅∧v∈𝑹→∀y∈A¬v0𝑹<ℝy∧∀y∈ℝy<ℝv0𝑹→∃z∈Ay<ℝz→∃x∈ℝ∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz
106 57 92 105 syl2and ⊢A⊆ℝ∧A≠∅∧v∈𝑹→∀w∈1stA¬v<𝑹w∧∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→∃x∈ℝ∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz
107 106 rexlimdva ⊢A⊆ℝ∧A≠∅→∃v∈𝑹∀w∈1stA¬v<𝑹w∧∀w∈𝑹w<𝑹v→∃u∈1stAw<𝑹u→∃x∈ℝ∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz
108 32 42 107 3syld ⊢A⊆ℝ∧A≠∅→∃x∈ℝ∀y∈Ay<ℝx→∃x∈ℝ∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz
109 108 3impia ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ay<ℝx→∃x∈ℝ∀y∈A¬x<ℝy∧∀y∈ℝy<ℝx→∃z∈Ay<ℝz