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 C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y E. x e. RR ( A. y e. A -. x E. z e. A y

Proof

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