xrofsup - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > xrofsup		Structured version Unicode version

Theorem xrofsup 28303

Description: The supremum is preserved by extended addition set operation. (Provided minus infinity is not involved as it does not behave well with addition.) (Contributed by Thierry Arnoux, 20-Mar-2017.)

**Hypotheses**
Ref	Expression
xrofsup.1
xrofsup.2
xrofsup.3
xrofsup.4
xrofsup.5

**Assertion**
Ref	Expression
xrofsup

Proof of Theorem xrofsup Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrofsup.5	. . 3
2		xrofsup.1	. . . . . . . . . 10
3	2	sseld 3406	. . . . . . . . 9
4		xrofsup.2	. . . . . . . . . 10
5	4	sseld 3406	. . . . . . . . 9
6	3, 5	anim12d 565	. . . . . . . 8 $/\$ $/\$
7	6	imp 430	. . . . . . 7 $/\$ $/\$ $/\$
8		xaddcl 11481	. . . . . . 7 $/\$
9	7, 8	syl 17	. . . . . 6 $/\$ $/\$
10	9	ralrimivva 2786	. . . . 5
11		fveq2 5825	. . . . . . . 8
12		df-ov 6252	. . . . . . . 8
13	11, 12	syl6eqr 2480	. . . . . . 7
14	13	eleq1d 2490	. . . . . 6
15	14	ralxp 4938	. . . . 5
16	10, 15	sylibr 215	. . . 4
17		xaddf 11468	. . . . . 6
18		ffun 5691	. . . . . 6
19	17, 18	ax-mp 5	. . . . 5
20		xpss12 4902	. . . . . . 7 $/\$
21	2, 4, 20	syl2anc 665	. . . . . 6
22	17	fdmi 5694	. . . . . 6
23	21, 22	syl6sseqr 3454	. . . . 5
24		funimass4 5876	. . . . 5 $/\$
25	19, 23, 24	sylancr 667	. . . 4
26	16, 25	mpbird 235	. . 3
27	1, 26	eqsstrd 3441	. 2
28		supxrcl 11551	. . . 4
29	2, 28	syl 17	. . 3
30		supxrcl 11551	. . . 4
31	4, 30	syl 17	. . 3
32	29, 31	xaddcld 11538	. 2
33	1	eleq2d 2491	. . . . 5
34	33	pm5.32i 641	. . . 4 $/\$ $/\$
35		nfvd 1756	. . . . 5 $/\$
36		nfvd 1756	. . . . 5 $/\$
37	2	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$ $/\$
38		simprl 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$
39		supxrub 11561	. . . . . . . . . . 11 $/\$
40	37, 38, 39	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$
41	4	ad2antrr 730	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42		simprr 764	. . . . . . . . . . 11 $/\$ $/\$ $/\$
43		supxrub 11561	. . . . . . . . . . 11 $/\$
44	41, 42, 43	syl2anc 665	. . . . . . . . . 10 $/\$ $/\$ $/\$
45	37, 38	sseldd 3408	. . . . . . . . . . 11 $/\$ $/\$ $/\$
46	41, 42	sseldd 3408	. . . . . . . . . . 11 $/\$ $/\$ $/\$
47	37, 28	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
48	41, 30	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		xle2add 11496	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
50	45, 46, 47, 48, 49	syl22anc 1265	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
51	40, 44, 50	mp2and 683	. . . . . . . . 9 $/\$ $/\$ $/\$
52	51	ralrimivva 2786	. . . . . . . 8 $/\$
53		fvelima 5877	. . . . . . . . . . 11 $/\$
54	19, 53	mpan 674	. . . . . . . . . 10
55	54	adantl 467	. . . . . . . . 9 $/\$
56	13	eqeq1d 2430	. . . . . . . . . 10
57	56	rexxp 4939	. . . . . . . . 9
58	55, 57	sylib 199	. . . . . . . 8 $/\$
59	52, 58	r19.29d2r 2910	. . . . . . 7 $/\$ $/\$
60		ancom 451	. . . . . . . 8 $/\$ $/\$
61	60	2rexbii 2867	. . . . . . 7 $/\$ $/\$
62	59, 61	sylib 199	. . . . . 6 $/\$ $/\$
63		breq1 4369	. . . . . . . . 9
64	63	biimpa 486	. . . . . . . 8 $/\$
65	64	reximi 2832	. . . . . . 7 $/\$
66	65	reximi 2832	. . . . . 6 $/\$
67	62, 66	syl 17	. . . . 5 $/\$
68	35, 36, 67	19.9d2r 28055	. . . 4 $/\$
69	34, 68	sylbi 198	. . 3 $/\$
70	69	ralrimiva 2779	. 2
71	2	ad2antrr 730	. . . . . 6 $/\$ $/\$
72	4	ad2antrr 730	. . . . . 6 $/\$ $/\$
73		simplr 760	. . . . . . 7 $/\$ $/\$
74	29	ad2antrr 730	. . . . . . 7 $/\$ $/\$
75	31	ad2antrr 730	. . . . . . 7 $/\$ $/\$
76		xrofsup.3	. . . . . . . 8
77	76	ad2antrr 730	. . . . . . 7 $/\$ $/\$
78		xrofsup.4	. . . . . . . 8
79	78	ad2antrr 730	. . . . . . 7 $/\$ $/\$
80		simpr 462	. . . . . . 7 $/\$ $/\$
81	73, 74, 75, 77, 79, 80	xlt2addrd 28288	. . . . . 6 $/\$ $/\$ $/\$ $/\$
82		nfv 1755	. . . . . . . 8 $/\$
83		nfcv 2569	. . . . . . . . 9
84		nfre1 2825	. . . . . . . . 9 $/\$ $/\$
85	83, 84	nfrex 2827	. . . . . . . 8 $/\$ $/\$
86	82, 85	nfan 1988	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
87		nfvd 1756	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
88		nfvd 1756	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
89		id 22	. . . . . . . . . . . 12 $/\$ $/\$
90	89	ralrimivw 2780	. . . . . . . . . . 11 $/\$ $/\$
91	90	ralrimivw 2780	. . . . . . . . . 10 $/\$ $/\$
92	91	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr 462	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	92, 93	r19.29d2r 2910	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simplrr 769	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	95	3anassrs 1228	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	96	simp1d 1017	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98		simp-4l 774	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simplrl 768	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	3anassrs 1228	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	simpld 460	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		simpllr 767	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	101, 102	sseldd 3408	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	100	simprd 464	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105		simplr 760	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	104, 105	sseldd 3408	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	98, 103, 106	jca32 537	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		simpr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109		xlt2add 11497	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	109	imp 430	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
111		breq1 4369	. . . . . . . . . . . . . . 15
112	111	biimpar 487	. . . . . . . . . . . . . 14 $/\$
113	110, 112	sylan2 476	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	97, 107, 108, 113	syl12anc 1262	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115		simplll 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		simprl 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117		simplr2 1048	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118		supxrlub 11562	. . . . . . . . . . . . . . . 16 $/\$
119	118	biimpa 486	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	115, 116, 117, 119	syl21anc 1263	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		simpllr 767	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122		simprr 764	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123		simplr3 1049	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124		supxrlub 11562	. . . . . . . . . . . . . . . 16 $/\$
125	124	biimpa 486	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	121, 122, 123, 125	syl21anc 1263	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		reeanv 2935	. . . . . . . . . . . . . 14 $/\$ $/\$
128	120, 126, 127	sylanbrc 668	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	128	ancoms 454	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	114, 129	reximddv2 2841	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	ex 435	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
132	131	reximdva 2839	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
133	132	reximia 2830	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
134	94, 133	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
135	86, 87, 88, 134	19.9d2rf 28054	. . . . . 6 $/\$ $/\$ $/\$ $/\$
136	71, 72, 81, 135	syl21anc 1263	. . . . 5 $/\$ $/\$
137		simprl 762	. . . . . . . . . 10 $/\$ $/\$
138		simprr 764	. . . . . . . . . 10 $/\$ $/\$
139	19	a1i 11	. . . . . . . . . 10 $/\$ $/\$
140	23	adantr 466	. . . . . . . . . 10 $/\$ $/\$
141	137, 138, 139, 140	elovimad 6289	. . . . . . . . 9 $/\$ $/\$
142	1	eleq2d 2491	. . . . . . . . . 10
143	142	adantr 466	. . . . . . . . 9 $/\$ $/\$
144	141, 143	mpbird 235	. . . . . . . 8 $/\$ $/\$
145		simpr 462	. . . . . . . . 9 $/\$ $/\$ $/\$
146	145	breq2d 4378	. . . . . . . 8 $/\$ $/\$ $/\$
147	144, 146	rspcedv 3129	. . . . . . 7 $/\$ $/\$
148	147	rexlimdvva 2863	. . . . . 6
149	148	ad2antrr 730	. . . . 5 $/\$ $/\$
150	136, 149	mpd 15	. . . 4 $/\$ $/\$
151	150	ex 435	. . 3 $/\$
152	151	ralrimiva 2779	. 2
153		supxr2 11550	. 2 $/\$ $/\$ $/\$
154	27, 32, 70, 152, 153	syl22anc 1265	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872

wne 2599

wral 2714

wrex 2715

wss 3379

cop 3947 class class class wbr 4366

cxp 4794

cdm 4796

cima 4799

wfun 5538

wf 5540

cfv 5544 (class class class)co 6249

csup 7907

cr 9489

cmnf 9624

cxr 9625

clt 9626

cle 9627

cxad 11358

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2063 ax-ext 2408 ax-sep 4489 ax-nul 4498 ax-pow 4545 ax-pr 4603 ax-un 6541 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567 ax-pre-sup 9568

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-nel 2602 df-ral 2719 df-rex 2720 df-reu 2721 df-rmo 2722 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-nul 3705 df-if 3855 df-pw 3926 df-sn 3942 df-pr 3944 df-op 3948 df-uni 4163 df-iun 4244 df-br 4367 df-opab 4426 df-mpt 4427 df-id 4711 df-po 4717 df-so 4718 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-dm 4806 df-rn 4807 df-res 4808 df-ima 4809 df-iota 5508 df-fun 5546 df-fn 5547 df-f 5548 df-f1 5549 df-fo 5550 df-f1o 5551 df-fv 5552 df-riota 6211 df-ov 6252 df-oprab 6253 df-mpt2 6254 df-1st 6751 df-2nd 6752 df-er 7318 df-en 7525 df-dom 7526 df-sdom 7527 df-sup 7909 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9813 df-neg 9814 df-div 10221 df-2 10619 df-rp 11254 df-xneg 11360 df-xadd 11361

This theorem is referenced by: (None)

W3C validator