Theorem ivthlem9 7379

Description: Lemma for isupivthi 7380.

Hypotheses

Ref	Expression
ivthlem4.1	|- A e. RR
ivthlem4.2	|- B e. RR
ivthlem4.3	|- U e. RR
ivthlem4.4	|- A < B
ivthlem4.5	|- ((F` A) < U /\ U < (F` B))
ivthlem4.6	|- C = sup(S, RR, < )
ivthlem4.7	|- S = {c e. (A[,]B) | (F` c) <_ U}
ivthlem4.8	|- F e. ((A[,]B)-cn->RR)
ivthlem9.9	|- T = {d e. (A[,]B) | (F` d) = U}
ivthlem9.10	|- (F` C) = U

Assertion

Ref	Expression
ivthlem9	|- C = sup(T, RR, < )

Distinct variable groups:   A,c,d   B,c,d   C,d   F,c,d   U,c,d

Proof of Theorem ivthlem9

Step	Hyp	Ref	Expression
1		ivthlem4.1	. . . . 5 |- A e. RR
2		ivthlem4.2	. . . . 5 |- B e. RR
3		iccssre 6422	. . . . 5 |- ((A e. RR /\ B e. RR) -> (A[,]B) (_ RR)
4	1, 2, 3	mp2an 709	. . . 4 |- (A[,]B) (_ RR
5		ivthlem4.3	. . . . 5 |- U e. RR
6		ivthlem4.4	. . . . 5 |- A < B
7		ivthlem4.5	. . . . 5 |- ((F` A) < U /\ U < (F` B))
8		ivthlem4.6	. . . . 5 |- C = sup(S, RR, < )
9		ivthlem4.7	. . . . 5 |- S = {c e. (A[,]B) | (F` c) <_ U}
10		ivthlem4.8	. . . . 5 |- F e. ((A[,]B)-cn->RR)
11	1, 2, 5, 6, 7, 8, 9, 10	ivthlem5 7375	. . . 4 |- C e. (A[,]B)
12	4, 11	sselii 2117	. . 3 |- C e. RR
13		ivthlem9.9	. . . . . . 7 |- T = {d e. (A[,]B) | (F` d) = U}
14		ssrab2 2182	. . . . . . 7 |- {d e. (A[,]B) | (F` d) = U} (_ (A[,]B)
15	13, 14	eqsstri 2142	. . . . . 6 |- T (_ (A[,]B)
16		fveq2 3781	. . . . . . . . 9 |- (d = C -> (F` d) = (F` C))
17	16	eqeq1d 1530	. . . . . . . 8 |- (d = C -> ((F` d) = U <-> (F` C) = U))
18	17, 13	elrab2 1954	. . . . . . 7 |- (C e. T <-> (C e. (A[,]B) /\ (F` C) = U))
19		ivthlem9.10	. . . . . . 7 |- (F` C) = U
20	18, 11, 19	mpbir2an 742	. . . . . 6 |- C e. T
21		iccsupr 6424	. . . . . 6 |- (((A e. RR /\ B e. RR) /\ T (_ (A[,]B) /\ C e. T) -> (T (_ RR /\ T =/= (/) /\ E.v e. RR A.w e. T w <_ v))
22	15, 20, 21	mp3an23 920	. . . . 5 |- ((A e. RR /\ B e. RR) -> (T (_ RR /\ T =/= (/) /\ E.v e. RR A.w e. T w <_ v))
23	1, 2, 22	mp2an 709	. . . 4 |- (T (_ RR /\ T =/= (/) /\ E.v e. RR A.w e. T w <_ v)
24	23	suprclii 6143	. . 3 |- sup(T, RR, < ) e. RR
25	12, 24	letri3i 5639	. 2 |- (C = sup(T, RR, < ) <-> (C <_ sup(T, RR, < ) /\ sup(T, RR, < ) <_ C))
26	23	suprubii 6144	. . 3 |- (C e. T -> C <_ sup(T, RR, < ))
27	20, 26	ax-mp 7	. 2 |- C <_ sup(T, RR, < )
28		fveq2 3781	. . . . . . 7 |- (d = x -> (F` d) = (F` x))
29	28	eqeq1d 1530	. . . . . 6 |- (d = x -> ((F` d) = U <-> (F` x) = U))
30	29, 13	elrab2 1954	. . . . 5 |- (x e. T <-> (x e. (A[,]B) /\ (F` x) = U))
31		axresscn 5333	. . . . . . . . . 10 |- RR (_ CC
32	4, 31	sstri 2124	. . . . . . . . 9 |- (A[,]B) (_ CC
33		cncffvelrn 7358	. . . . . . . . 9 |- (((A[,]B) (_ CC /\ RR (_ CC /\ F e. ((A[,]B)-cn->RR)) -> (x e. (A[,]B) -> (F` x) e. RR))
34	32, 31, 10, 33	mp3an 928	. . . . . . . 8 |- (x e. (A[,]B) -> (F` x) e. RR)
35		eqle 5636	. . . . . . . . 9 |- (((F` x) e. RR /\ (F` x) = U) -> (F` x) <_ U)
36	35	ex 380	. . . . . . . 8 |- ((F` x) e. RR -> ((F` x) = U -> (F` x) <_ U))
37	34, 36	syl 10	. . . . . . 7 |- (x e. (A[,]B) -> ((F` x) = U -> (F` x) <_ U))
38		fveq2 3781	. . . . . . . . . . 11 |- (c = x -> (F` c) = (F` x))
39	38	breq1d 2684	. . . . . . . . . 10 |- (c = x -> ((F` c) <_ U <-> (F` x) <_ U))
40	39, 9	elrab2 1954	. . . . . . . . 9 |- (x e. S <-> (x e. (A[,]B) /\ (F` x) <_ U))
41	1, 2, 5, 6, 7, 8, 9, 10	ivthlem4 7374	. . . . . . . . . . . 12 |- ((S (_ RR /\ S =/= (/) /\ E.v e. RR A.w e. S w <_ v) /\ A e. S)
42	41	pm3.26i 327	. . . . . . . . . . 11 |- (S (_ RR /\ S =/= (/) /\ E.v e. RR A.w e. S w <_ v)
43	42	suprubii 6144	. . . . . . . . . 10 |- (x e. S -> x <_ sup(S, RR, < ))
44	43, 8	syl6breqr 2710	. . . . . . . . 9 |- (x e. S -> x <_ C)
45	40, 44	sylbir 208	. . . . . . . 8 |- ((x e. (A[,]B) /\ (F` x) <_ U) -> x <_ C)
46	45	ex 380	. . . . . . 7 |- (x e. (A[,]B) -> ((F` x) <_ U -> x <_ C))
47	37, 46	syld 27	. . . . . 6 |- (x e. (A[,]B) -> ((F` x) = U -> x <_ C))
48	47	imp 357	. . . . 5 |- ((x e. (A[,]B) /\ (F` x) = U) -> x <_ C)
49	30, 48	sylbi 206	. . . 4 |- (x e. T -> x <_ C)
50	49	rgen 1745	. . 3 |- A.x e. T x <_ C
51	23	suprleubii 6147	. . 3 |- ((C e. RR /\ A.x e. T x <_ C) -> sup(T, RR, < ) <_ C)
52	12, 50, 51	mp2an 709	. 2 |- sup(T, RR, < ) <_ C
53	25, 27, 52	mpbir2an 742	1 |- C = sup(T, RR, < )

Syntax hints:   -> wi 3   /\ wa 230   /\ w3a 787   = wceq 997   e. wcel 999   =/= wne 1632  A.wral 1692  E.wrex 1693  {crab 1695   (_ wss 2098  (/)c0 2331   class class class wbr 2674  ` cfv 3239  (class class class)co 4021  supcsup 4633  CCcc 5297  RRcr 5298   <_ cle 5360   < clt 5551  [,]cicc 6385  -cn->ccncf 7352

This theorem is referenced by:  isupivthi 7380

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-nel 1635  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-pss 2106  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-f1 3252  df-fo 3253  df-f1o 3254  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-1o 4191  df-oadd 4193  df-omul 4194  df-er 4319  df-ec 4321  df-qs 4324  df-en 4429  df-dom 4430  df-sdom 4431  df-sup 4634  df-ni 5065  df-pli 5066  df-mi 5067  df-lti 5068  df-plpq 5100  df-mpq 5101  df-enq 5102  df-nq 5103  df-plq 5104  df-mq 5105  df-rq 5106  df-ltq 5107  df-1q 5108  df-np 5151  df-1p 5152  df-plp 5153  df-mp 5154  df-ltp 5155  df-plpr 5229  df-mpr 5230  df-enr 5231  df-nr 5232  df-plr 5233  df-mr 5234  df-ltr 5235  df-0r 5236  df-1r 5237  df-m1r 5238  df-c 5305  df-0 5306  df-1 5307  df-i 5308  df-r 5309  df-plus 5310  df-mul 5311  df-lt 5312  df-sub 5421  df-neg 5423  df-pnf 5552  df-mnf 5553  df-xr 5554  df-ltxr 5555  df-le 5556  df-icc 6389  df-cncf 7353

Copyright terms: Public domain