xrofsup - Mathbox for Thierry Arnoux

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

Theorem xrofsup 28428

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 3417	. . . . . . . . 9
4		xrofsup.2	. . . . . . . . . 10
5	4	sseld 3417	. . . . . . . . 9
6	3, 5	anim12d 572	. . . . . . . 8 $/\$ $/\$
7	6	imp 436	. . . . . . 7 $/\$ $/\$ $/\$
8		xaddcl 11554	. . . . . . 7 $/\$
9	7, 8	syl 17	. . . . . 6 $/\$ $/\$
10	9	ralrimivva 2814	. . . . 5
11		fveq2 5879	. . . . . . . 8
12		df-ov 6311	. . . . . . . 8
13	11, 12	syl6eqr 2523	. . . . . . 7
14	13	eleq1d 2533	. . . . . 6
15	14	ralxp 4981	. . . . 5
16	10, 15	sylibr 217	. . . 4
17		xaddf 11540	. . . . . 6
18		ffun 5742	. . . . . 6
19	17, 18	ax-mp 5	. . . . 5
20		xpss12 4945	. . . . . . 7 $/\$
21	2, 4, 20	syl2anc 673	. . . . . 6
22	17	fdmi 5746	. . . . . 6
23	21, 22	syl6sseqr 3465	. . . . 5
24		funimass4 5930	. . . . 5 $/\$
25	19, 23, 24	sylancr 676	. . . 4
26	16, 25	mpbird 240	. . 3
27	1, 26	eqsstrd 3452	. 2
28		supxrcl 11625	. . . 4
29	2, 28	syl 17	. . 3
30		supxrcl 11625	. . . 4
31	4, 30	syl 17	. . 3
32	29, 31	xaddcld 11612	. 2
33	1	eleq2d 2534	. . . . 5
34	33	pm5.32i 649	. . . 4 $/\$ $/\$
35		nfvd 1770	. . . . 5 $/\$
36		nfvd 1770	. . . . 5 $/\$
37	2	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$
38		simprl 772	. . . . . . . . . . 11 $/\$ $/\$ $/\$
39		supxrub 11635	. . . . . . . . . . 11 $/\$
40	37, 38, 39	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$
41	4	ad2antrr 740	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42		simprr 774	. . . . . . . . . . 11 $/\$ $/\$ $/\$
43		supxrub 11635	. . . . . . . . . . 11 $/\$
44	41, 42, 43	syl2anc 673	. . . . . . . . . 10 $/\$ $/\$ $/\$
45	37, 38	sseldd 3419	. . . . . . . . . . 11 $/\$ $/\$ $/\$
46	41, 42	sseldd 3419	. . . . . . . . . . 11 $/\$ $/\$ $/\$
47	37, 28	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
48	41, 30	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		xle2add 11570	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
50	45, 46, 47, 48, 49	syl22anc 1293	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
51	40, 44, 50	mp2and 693	. . . . . . . . 9 $/\$ $/\$ $/\$
52	51	ralrimivva 2814	. . . . . . . 8 $/\$
53		fvelima 5931	. . . . . . . . . . 11 $/\$
54	19, 53	mpan 684	. . . . . . . . . 10
55	54	adantl 473	. . . . . . . . 9 $/\$
56	13	eqeq1d 2473	. . . . . . . . . 10
57	56	rexxp 4982	. . . . . . . . 9
58	55, 57	sylib 201	. . . . . . . 8 $/\$
59	52, 58	r19.29d2r 2919	. . . . . . 7 $/\$ $/\$
60		ancom 457	. . . . . . . 8 $/\$ $/\$
61	60	2rexbii 2882	. . . . . . 7 $/\$ $/\$
62	59, 61	sylib 201	. . . . . 6 $/\$ $/\$
63		breq1 4398	. . . . . . . . 9
64	63	biimpa 492	. . . . . . . 8 $/\$
65	64	reximi 2852	. . . . . . 7 $/\$
66	65	reximi 2852	. . . . . 6 $/\$
67	62, 66	syl 17	. . . . 5 $/\$
68	35, 36, 67	19.9d2r 28194	. . . 4 $/\$
69	34, 68	sylbi 200	. . 3 $/\$
70	69	ralrimiva 2809	. 2
71	2	ad2antrr 740	. . . . . 6 $/\$ $/\$
72	4	ad2antrr 740	. . . . . 6 $/\$ $/\$
73		simplr 770	. . . . . . 7 $/\$ $/\$
74	29	ad2antrr 740	. . . . . . 7 $/\$ $/\$
75	31	ad2antrr 740	. . . . . . 7 $/\$ $/\$
76		xrofsup.3	. . . . . . . 8
77	76	ad2antrr 740	. . . . . . 7 $/\$ $/\$
78		xrofsup.4	. . . . . . . 8
79	78	ad2antrr 740	. . . . . . 7 $/\$ $/\$
80		simpr 468	. . . . . . 7 $/\$ $/\$
81	73, 74, 75, 77, 79, 80	xlt2addrd 28413	. . . . . 6 $/\$ $/\$ $/\$ $/\$
82		nfv 1769	. . . . . . . 8 $/\$
83		nfcv 2612	. . . . . . . . 9
84		nfre1 2846	. . . . . . . . 9 $/\$ $/\$
85	83, 84	nfrex 2848	. . . . . . . 8 $/\$ $/\$
86	82, 85	nfan 2031	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
87		nfvd 1770	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
88		nfvd 1770	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
89		id 22	. . . . . . . . . . . 12 $/\$ $/\$
90	89	ralrimivw 2810	. . . . . . . . . . 11 $/\$ $/\$
91	90	ralrimivw 2810	. . . . . . . . . 10 $/\$ $/\$
92	91	adantr 472	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr 468	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	92, 93	r19.29d2r 2919	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simplrr 779	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	95	3anassrs 1256	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	96	simp1d 1042	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98		simp-4l 784	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simplrl 778	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	3anassrs 1256	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	simpld 466	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		simpllr 777	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	101, 102	sseldd 3419	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	100	simprd 470	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105		simplr 770	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	104, 105	sseldd 3419	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	98, 103, 106	jca32 544	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		simpr 468	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109		xlt2add 11571	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	109	imp 436	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
111		breq1 4398	. . . . . . . . . . . . . . 15
112	111	biimpar 493	. . . . . . . . . . . . . 14 $/\$
113	110, 112	sylan2 482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	97, 107, 108, 113	syl12anc 1290	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115		simplll 776	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		simprl 772	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117		simplr2 1073	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118		supxrlub 11636	. . . . . . . . . . . . . . . 16 $/\$
119	118	biimpa 492	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	115, 116, 117, 119	syl21anc 1291	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		simpllr 777	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122		simprr 774	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123		simplr3 1074	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124		supxrlub 11636	. . . . . . . . . . . . . . . 16 $/\$
125	124	biimpa 492	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	121, 122, 123, 125	syl21anc 1291	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		reeanv 2944	. . . . . . . . . . . . . 14 $/\$ $/\$
128	120, 126, 127	sylanbrc 677	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	128	ancoms 460	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	114, 129	reximddv2 2860	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	ex 441	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
132	131	reximdva 2858	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
133	132	reximia 2850	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
134	94, 133	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
135	86, 87, 88, 134	19.9d2rf 28193	. . . . . 6 $/\$ $/\$ $/\$ $/\$
136	71, 72, 81, 135	syl21anc 1291	. . . . 5 $/\$ $/\$
137		simprl 772	. . . . . . . . . 10 $/\$ $/\$
138		simprr 774	. . . . . . . . . 10 $/\$ $/\$
139	19	a1i 11	. . . . . . . . . 10 $/\$ $/\$
140	23	adantr 472	. . . . . . . . . 10 $/\$ $/\$
141	137, 138, 139, 140	elovimad 6348	. . . . . . . . 9 $/\$ $/\$
142	1	eleq2d 2534	. . . . . . . . . 10
143	142	adantr 472	. . . . . . . . 9 $/\$ $/\$
144	141, 143	mpbird 240	. . . . . . . 8 $/\$ $/\$
145		simpr 468	. . . . . . . . 9 $/\$ $/\$ $/\$
146	145	breq2d 4407	. . . . . . . 8 $/\$ $/\$ $/\$
147	144, 146	rspcedv 3140	. . . . . . 7 $/\$ $/\$
148	147	rexlimdvva 2878	. . . . . 6
149	148	ad2antrr 740	. . . . 5 $/\$ $/\$
150	136, 149	mpd 15	. . . 4 $/\$ $/\$
151	150	ex 441	. . 3 $/\$
152	151	ralrimiva 2809	. 2
153		supxr2 11624	. 2 $/\$ $/\$ $/\$
154	27, 32, 70, 152, 153	syl22anc 1293	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wcel 1904

wne 2641

wral 2756

wrex 2757

wss 3390

cop 3965 class class class wbr 4395

cxp 4837

cdm 4839

cima 4842

wfun 5583

wf 5585

cfv 5589 (class class class)co 6308

csup 7972

cr 9556

cmnf 9691

cxr 9692

clt 9693

cle 9694

cxad 11430

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 ax-pre-sup 9635

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-po 4760 df-so 4761 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-1st 6812 df-2nd 6813 df-er 7381 df-en 7588 df-dom 7589 df-sdom 7590 df-sup 7974 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-div 10292 df-2 10690 df-rp 11326 df-xneg 11432 df-xadd 11433

This theorem is referenced by: (None)

W3C validator