Theorem infnsuprnmpt 39465

Description: The indexed infimum of real numbers is the negative of the indexed supremum of the negative values. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
infnsuprnmpt.x	|- F/ x ph
infnsuprnmpt.a	|- ( ph -> A =/= (/) )
infnsuprnmpt.b	|- ( ( ph /\ x e. A ) -> B e. RR )
infnsuprnmpt.l	|- ( ph -> E. y e. RR A. x e. A y <_ B )

Assertion

Ref	Expression
infnsuprnmpt	|- ( ph -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )

Distinct variable groups:   x, A, y   y, B

Allowed substitution hints:   ph( x, y)   B( x)

Proof of Theorem infnsuprnmpt

Dummy variables w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		infnsuprnmpt.x	. . . 4 |- F/ x ph
2		eqid 2622	. . . 4 |- ( x e. A |-> B ) = ( x e. A |-> B )
3		infnsuprnmpt.b	. . . 4 |- ( ( ph /\ x e. A ) -> B e. RR )
4	1, 2, 3	rnmptssd 39385	. . 3 |- ( ph -> ran ( x e. A |-> B ) C_ RR )
5		infnsuprnmpt.a	. . . 4 |- ( ph -> A =/= (/) )
6	1, 3, 2, 5	rnmptn0 39413	. . 3 |- ( ph -> ran ( x e. A |-> B ) =/= (/) )
7		infnsuprnmpt.l	. . . 4 |- ( ph -> E. y e. RR A. x e. A y <_ B )
8	7	rnmptlb 39453	. . 3 |- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z )
9		infrenegsup 11006	. . 3 |- ( ( ran ( x e. A |-> B ) C_ RR /\ ran ( x e. A |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) )
10	4, 6, 8, 9	syl3anc 1326	. 2 |- ( ph -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) )
11		eqid 2622	. . . . . . . . 9 |- ( x e. A |-> -u B ) = ( x e. A |-> -u B )
12		rabidim2 39284	. . . . . . . . . . . 12 |- ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } -> -u w e. ran ( x e. A |-> B ) )
13	12	adantl 482	. . . . . . . . . . 11 |- ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> -u w e. ran ( x e. A |-> B ) )
14		negex 10279	. . . . . . . . . . . 12 |- -u w e. _V
15	2	elrnmpt 5372	. . . . . . . . . . . 12 |- ( -u w e. _V -> ( -u w e. ran ( x e. A |-> B ) <-> E. x e. A -u w = B ) )
16	14, 15	ax-mp 5	. . . . . . . . . . 11 |- ( -u w e. ran ( x e. A |-> B ) <-> E. x e. A -u w = B )
17	13, 16	sylib 208	. . . . . . . . . 10 |- ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> E. x e. A -u w = B )
18		nfcv 2764	. . . . . . . . . . . . 13 |- F/_ x w
19	18	nfneg 10277	. . . . . . . . . . . . . . 15 |- F/_ x -u w
20		nfmpt1 4747	. . . . . . . . . . . . . . . 16 |- F/_ x ( x e. A |-> B )
21	20	nfrn 5368	. . . . . . . . . . . . . . 15 |- F/_ x ran ( x e. A |-> B )
22	19, 21	nfel 2777	. . . . . . . . . . . . . 14 |- F/ x -u w e. ran ( x e. A |-> B )
23		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ x RR
24	22, 23	nfrab 3123	. . . . . . . . . . . . 13 |- F/_ x { w e. RR | -u w e. ran ( x e. A |-> B ) }
25	18, 24	nfel 2777	. . . . . . . . . . . 12 |- F/ x w e. { w e. RR | -u w e. ran ( x e. A |-> B ) }
26	1, 25	nfan 1828	. . . . . . . . . . 11 |- F/ x ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } )
27		rabidim1 3117	. . . . . . . . . . . . 13 |- ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } -> w e. RR )
28	27	adantl 482	. . . . . . . . . . . 12 |- ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> w e. RR )
29		negeq 10273	. . . . . . . . . . . . . . . 16 |- ( -u w = B -> -u -u w = -u B )
30	29	eqcomd 2628	. . . . . . . . . . . . . . 15 |- ( -u w = B -> -u B = -u -u w )
31	30	3ad2ant3 1084	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. RR ) /\ x e. A /\ -u w = B ) -> -u B = -u -u w )
32		simp1r 1086	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. RR ) /\ x e. A /\ -u w = B ) -> w e. RR )
33		recn 10026	. . . . . . . . . . . . . . . 16 |- ( w e. RR -> w e. CC )
34	33	negnegd 10383	. . . . . . . . . . . . . . 15 |- ( w e. RR -> -u -u w = w )
35	32, 34	syl 17	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. RR ) /\ x e. A /\ -u w = B ) -> -u -u w = w )
36	31, 35	eqtr2d 2657	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. RR ) /\ x e. A /\ -u w = B ) -> w = -u B )
37	36	3exp 1264	. . . . . . . . . . . 12 |- ( ( ph /\ w e. RR ) -> ( x e. A -> ( -u w = B -> w = -u B ) ) )
38	28, 37	syldan 487	. . . . . . . . . . 11 |- ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> ( x e. A -> ( -u w = B -> w = -u B ) ) )
39	26, 38	reximdai 3012	. . . . . . . . . 10 |- ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> ( E. x e. A -u w = B -> E. x e. A w = -u B ) )
40	17, 39	mpd 15	. . . . . . . . 9 |- ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> E. x e. A w = -u B )
41		simpr 477	. . . . . . . . 9 |- ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } )
42	11, 40, 41	elrnmptd 39366	. . . . . . . 8 |- ( ( ph /\ w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) -> w e. ran ( x e. A |-> -u B ) )
43	42	ex 450	. . . . . . 7 |- ( ph -> ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } -> w e. ran ( x e. A |-> -u B ) ) )
44		vex 3203	. . . . . . . . . . . . 13 |- w e. _V
45	11	elrnmpt 5372	. . . . . . . . . . . . 13 |- ( w e. _V -> ( w e. ran ( x e. A |-> -u B ) <-> E. x e. A w = -u B ) )
46	44, 45	ax-mp 5	. . . . . . . . . . . 12 |- ( w e. ran ( x e. A |-> -u B ) <-> E. x e. A w = -u B )
47	46	biimpi 206	. . . . . . . . . . 11 |- ( w e. ran ( x e. A |-> -u B ) -> E. x e. A w = -u B )
48	47	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ w e. ran ( x e. A |-> -u B ) ) -> E. x e. A w = -u B )
49	18, 23	nfel 2777	. . . . . . . . . . . . 13 |- F/ x w e. RR
50	49, 22	nfan 1828	. . . . . . . . . . . 12 |- F/ x ( w e. RR /\ -u w e. ran ( x e. A |-> B ) )
51		simp3 1063	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A /\ w = -u B ) -> w = -u B )
52	3	renegcld 10457	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A ) -> -u B e. RR )
53	52	3adant3 1081	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A /\ w = -u B ) -> -u B e. RR )
54	51, 53	eqeltrd 2701	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A /\ w = -u B ) -> w e. RR )
55		simp2 1062	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A /\ w = -u B ) -> x e. A )
56	51	negeqd 10275	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. A /\ w = -u B ) -> -u w = -u -u B )
57	3	recnd 10068	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. A ) -> B e. CC )
58	57	negnegd 10383	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. A ) -> -u -u B = B )
59	58	3adant3 1081	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. A /\ w = -u B ) -> -u -u B = B )
60	56, 59	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. A /\ w = -u B ) -> -u w = B )
61		rspe 3003	. . . . . . . . . . . . . . . 16 |- ( ( x e. A /\ -u w = B ) -> E. x e. A -u w = B )
62	55, 60, 61	syl2anc 693	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A /\ w = -u B ) -> E. x e. A -u w = B )
63	14	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. A /\ w = -u B ) -> -u w e. _V )
64	2, 62, 63	elrnmptd 39366	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A /\ w = -u B ) -> -u w e. ran ( x e. A |-> B ) )
65	54, 64	jca 554	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A /\ w = -u B ) -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) )
66	65	3exp 1264	. . . . . . . . . . . 12 |- ( ph -> ( x e. A -> ( w = -u B -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) ) ) )
67	1, 50, 66	rexlimd 3026	. . . . . . . . . . 11 |- ( ph -> ( E. x e. A w = -u B -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) ) )
68	67	imp 445	. . . . . . . . . 10 |- ( ( ph /\ E. x e. A w = -u B ) -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) )
69	48, 68	syldan 487	. . . . . . . . 9 |- ( ( ph /\ w e. ran ( x e. A |-> -u B ) ) -> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) )
70		rabid 3116	. . . . . . . . 9 |- ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } <-> ( w e. RR /\ -u w e. ran ( x e. A |-> B ) ) )
71	69, 70	sylibr 224	. . . . . . . 8 |- ( ( ph /\ w e. ran ( x e. A |-> -u B ) ) -> w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } )
72	71	ex 450	. . . . . . 7 |- ( ph -> ( w e. ran ( x e. A |-> -u B ) -> w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } ) )
73	43, 72	impbid 202	. . . . . 6 |- ( ph -> ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } <-> w e. ran ( x e. A |-> -u B ) ) )
74	73	alrimiv 1855	. . . . 5 |- ( ph -> A. w ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } <-> w e. ran ( x e. A |-> -u B ) ) )
75		nfrab1 3122	. . . . . 6 |- F/_ w { w e. RR | -u w e. ran ( x e. A |-> B ) }
76		nfcv 2764	. . . . . 6 |- F/_ w ran ( x e. A |-> -u B )
77	75, 76	dfcleqf 39255	. . . . 5 |- ( { w e. RR | -u w e. ran ( x e. A |-> B ) } = ran ( x e. A |-> -u B ) <-> A. w ( w e. { w e. RR | -u w e. ran ( x e. A |-> B ) } <-> w e. ran ( x e. A |-> -u B ) ) )
78	74, 77	sylibr 224	. . . 4 |- ( ph -> { w e. RR | -u w e. ran ( x e. A |-> B ) } = ran ( x e. A |-> -u B ) )
79	78	supeq1d 8352	. . 3 |- ( ph -> sup ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) = sup ( ran ( x e. A |-> -u B ) , RR , < ) )
80	79	negeqd 10275	. 2 |- ( ph -> -u sup ( { w e. RR | -u w e. ran ( x e. A |-> B ) } , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )
81		eqidd 2623	. 2 |- ( ph -> -u sup ( ran ( x e. A |-> -u B ) , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )
82	10, 80, 81	3eqtrd 2660	1 |- ( ph -> inf ( ran ( x e. A |-> B ) , RR , < ) = -u sup ( ran ( x e. A |-> -u B ) , RR , < ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   F/wnf 1708   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   C_ wss 3574   (/)c0 3915   class class class wbr 4653   |-> cmpt 4729   ran crn 5115   supcsup 8346  infcinf 8347   RRcr 9935   < clt 10074   <_ cle 10075   -ucneg 10267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-po 5035  df-so 5036  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-sup 8348  df-inf 8349  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269

This theorem is referenced by:  smfinflem  41023