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 27819

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 3488	. . . . . . . . 9
4		xrofsup.2	. . . . . . . . . 10
5	4	sseld 3488	. . . . . . . . 9
6	3, 5	anim12d 561	. . . . . . . 8 $/\$ $/\$
7	6	imp 427	. . . . . . 7 $/\$ $/\$ $/\$
8		xaddcl 11439	. . . . . . 7 $/\$
9	7, 8	syl 16	. . . . . 6 $/\$ $/\$
10	9	ralrimivva 2875	. . . . 5
11		fveq2 5848	. . . . . . . 8
12		df-ov 6273	. . . . . . . 8
13	11, 12	syl6eqr 2513	. . . . . . 7
14	13	eleq1d 2523	. . . . . 6
15	14	ralxp 5133	. . . . 5
16	10, 15	sylibr 212	. . . 4
17		xaddf 11426	. . . . . 6
18		ffun 5715	. . . . . 6
19	17, 18	ax-mp 5	. . . . 5
20		xpss12 5096	. . . . . . 7 $/\$
21	2, 4, 20	syl2anc 659	. . . . . 6
22	17	fdmi 5718	. . . . . 6
23	21, 22	syl6sseqr 3536	. . . . 5
24		funimass4 5899	. . . . 5 $/\$
25	19, 23, 24	sylancr 661	. . . 4
26	16, 25	mpbird 232	. . 3
27	1, 26	eqsstrd 3523	. 2
28		supxrcl 11509	. . . 4
29	2, 28	syl 16	. . 3
30		supxrcl 11509	. . . 4
31	4, 30	syl 16	. . 3
32	29, 31	xaddcld 11496	. 2
33	1	eleq2d 2524	. . . . 5
34	33	pm5.32i 635	. . . 4 $/\$ $/\$
35		nfvd 1713	. . . . 5 $/\$
36		nfvd 1713	. . . . 5 $/\$
37	2	ad2antrr 723	. . . . . . . . . . 11 $/\$ $/\$ $/\$
38		simprl 754	. . . . . . . . . . 11 $/\$ $/\$ $/\$
39		supxrub 11519	. . . . . . . . . . 11 $/\$
40	37, 38, 39	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$
41	4	ad2antrr 723	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42		simprr 755	. . . . . . . . . . 11 $/\$ $/\$ $/\$
43		supxrub 11519	. . . . . . . . . . 11 $/\$
44	41, 42, 43	syl2anc 659	. . . . . . . . . 10 $/\$ $/\$ $/\$
45	37, 38	sseldd 3490	. . . . . . . . . . 11 $/\$ $/\$ $/\$
46	41, 42	sseldd 3490	. . . . . . . . . . 11 $/\$ $/\$ $/\$
47	37, 28	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$
48	41, 30	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$
49		xle2add 11454	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
50	45, 46, 47, 48, 49	syl22anc 1227	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
51	40, 44, 50	mp2and 677	. . . . . . . . 9 $/\$ $/\$ $/\$
52	51	ralrimivva 2875	. . . . . . . 8 $/\$
53		fvelima 5900	. . . . . . . . . . 11 $/\$
54	19, 53	mpan 668	. . . . . . . . . 10
55	54	adantl 464	. . . . . . . . 9 $/\$
56	13	eqeq1d 2456	. . . . . . . . . 10
57	56	rexxp 5134	. . . . . . . . 9
58	55, 57	sylib 196	. . . . . . . 8 $/\$
59	52, 58	r19.29d2r 2997	. . . . . . 7 $/\$ $/\$
60		ancom 448	. . . . . . . 8 $/\$ $/\$
61	60	2rexbii 2957	. . . . . . 7 $/\$ $/\$
62	59, 61	sylib 196	. . . . . 6 $/\$ $/\$
63		breq1 4442	. . . . . . . . 9
64	63	biimpa 482	. . . . . . . 8 $/\$
65	64	reximi 2922	. . . . . . 7 $/\$
66	65	reximi 2922	. . . . . 6 $/\$
67	62, 66	syl 16	. . . . 5 $/\$
68	35, 36, 67	19.9d2r 27579	. . . 4 $/\$
69	34, 68	sylbi 195	. . 3 $/\$
70	69	ralrimiva 2868	. 2
71	2	ad2antrr 723	. . . . . 6 $/\$ $/\$
72	4	ad2antrr 723	. . . . . 6 $/\$ $/\$
73		simplr 753	. . . . . . 7 $/\$ $/\$
74	29	ad2antrr 723	. . . . . . 7 $/\$ $/\$
75	31	ad2antrr 723	. . . . . . 7 $/\$ $/\$
76		xrofsup.3	. . . . . . . 8
77	76	ad2antrr 723	. . . . . . 7 $/\$ $/\$
78		xrofsup.4	. . . . . . . 8
79	78	ad2antrr 723	. . . . . . 7 $/\$ $/\$
80		simpr 459	. . . . . . 7 $/\$ $/\$
81	73, 74, 75, 77, 79, 80	xlt2addrd 27812	. . . . . 6 $/\$ $/\$ $/\$ $/\$
82		nfv 1712	. . . . . . . 8 $/\$
83		nfcv 2616	. . . . . . . . 9
84		nfre1 2915	. . . . . . . . 9 $/\$ $/\$
85	83, 84	nfrex 2917	. . . . . . . 8 $/\$ $/\$
86	82, 85	nfan 1933	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
87		nfvd 1713	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
88		nfvd 1713	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
89		id 22	. . . . . . . . . . . 12 $/\$ $/\$
90	89	ralrimivw 2869	. . . . . . . . . . 11 $/\$ $/\$
91	90	ralrimivw 2869	. . . . . . . . . 10 $/\$ $/\$
92	91	adantr 463	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
93		simpr 459	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
94	92, 93	r19.29d2r 2997	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		simplrr 760	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
96	95	3anassrs 1216	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
97	96	simp1d 1006	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
98		simp-4l 765	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
99		simplrl 759	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
100	99	3anassrs 1216	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
101	100	simpld 457	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
102		simpllr 758	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
103	101, 102	sseldd 3490	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
104	100	simprd 461	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
105		simplr 753	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
106	104, 105	sseldd 3490	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
107	98, 103, 106	jca32 533	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
108		simpr 459	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
109		xlt2add 11455	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
110	109	imp 427	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
111		breq1 4442	. . . . . . . . . . . . . . 15
112	111	biimpar 483	. . . . . . . . . . . . . 14 $/\$
113	110, 112	sylan2 472	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
114	97, 107, 108, 113	syl12anc 1224	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
115		simplll 757	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
116		simprl 754	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
117		simplr2 1037	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
118		supxrlub 11520	. . . . . . . . . . . . . . . 16 $/\$
119	118	biimpa 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
120	115, 116, 117, 119	syl21anc 1225	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121		simpllr 758	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122		simprr 755	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123		simplr3 1038	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124		supxrlub 11520	. . . . . . . . . . . . . . . 16 $/\$
125	124	biimpa 482	. . . . . . . . . . . . . . 15 $/\$ $/\$
126	121, 122, 123, 125	syl21anc 1225	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127		reeanv 3022	. . . . . . . . . . . . . 14 $/\$ $/\$
128	120, 126, 127	sylanbrc 662	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	128	ancoms 451	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130	114, 129	reximddv2 2931	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131	130	ex 432	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
132	131	reximdva 2929	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
133	132	reximia 2920	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
134	94, 133	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
135	86, 87, 88, 134	19.9d2rf 27578	. . . . . 6 $/\$ $/\$ $/\$ $/\$
136	71, 72, 81, 135	syl21anc 1225	. . . . 5 $/\$ $/\$
137		simprl 754	. . . . . . . . . 10 $/\$ $/\$
138		simprr 755	. . . . . . . . . 10 $/\$ $/\$
139	19	a1i 11	. . . . . . . . . 10 $/\$ $/\$
140	23	adantr 463	. . . . . . . . . 10 $/\$ $/\$
141	137, 138, 139, 140	elovimad 6310	. . . . . . . . 9 $/\$ $/\$
142	1	eleq2d 2524	. . . . . . . . . 10
143	142	adantr 463	. . . . . . . . 9 $/\$ $/\$
144	141, 143	mpbird 232	. . . . . . . 8 $/\$ $/\$
145		simpr 459	. . . . . . . . 9 $/\$ $/\$ $/\$
146	145	breq2d 4451	. . . . . . . 8 $/\$ $/\$ $/\$
147	144, 146	rspcedv 3211	. . . . . . 7 $/\$ $/\$
148	147	rexlimdvva 2953	. . . . . 6
149	148	ad2antrr 723	. . . . 5 $/\$ $/\$
150	136, 149	mpd 15	. . . 4 $/\$ $/\$
151	150	ex 432	. . 3 $/\$
152	151	ralrimiva 2868	. 2
153		supxr2 11508	. 2 $/\$ $/\$ $/\$
154	27, 32, 70, 152, 153	syl22anc 1227	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

wne 2649

wral 2804

wrex 2805

wss 3461

cop 4022 class class class wbr 4439

cxp 4986

cdm 4988

cima 4991

wfun 5564

wf 5566

cfv 5570 (class class class)co 6270

csup 7892

cr 9480

cmnf 9615

cxr 9616

clt 9617

cle 9618

cxad 11319

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558 ax-pre-sup 9559

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-op 4023 df-uni 4236 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-id 4784 df-po 4789 df-so 4790 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-1st 6773 df-2nd 6774 df-er 7303 df-en 7510 df-dom 7511 df-sdom 7512 df-sup 7893 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-div 10203 df-2 10590 df-rp 11222 df-xneg 11321 df-xadd 11322

This theorem is referenced by: (None)

W3C validator