Theorem xposdif 9506

Description: Extended real version of posdif 8084. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)

Assertion

Ref	Expression
xposdif	|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> 0 < ( B +e -e A ) ) )

Proof of Theorem xposdif

Step	Hyp	Ref	Expression
1		elxr 9404	. . 3 |- ( B e. RR* <-> ( B e. RR \/ B = +oo \/ B = -oo ) )
2		elxr 9404	. . . . 5 |- ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
3		posdif 8084	. . . . . . . 8 |- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B - A ) ) )
4		rexsub 9477	. . . . . . . . . 10 |- ( ( B e. RR /\ A e. RR ) -> ( B +e -e A ) = ( B - A ) )
5	4	ancoms 266	. . . . . . . . 9 |- ( ( A e. RR /\ B e. RR ) -> ( B +e -e A ) = ( B - A ) )
6	5	breq2d 3887	. . . . . . . 8 |- ( ( A e. RR /\ B e. RR ) -> ( 0 < ( B +e -e A ) <-> 0 < ( B - A ) ) )
7	3, 6	bitr4d 190	. . . . . . 7 |- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
8	7	ex 114	. . . . . 6 |- ( A e. RR -> ( B e. RR -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
9		rexr 7683	. . . . . . . . . 10 |- ( B e. RR -> B e. RR* )
10		pnfnlt 9414	. . . . . . . . . . 11 |- ( B e. RR* -> -. +oo < B )
11	10	adantl 273	. . . . . . . . . 10 |- ( ( A = +oo /\ B e. RR* ) -> -. +oo < B )
12	9, 11	sylan2 282	. . . . . . . . 9 |- ( ( A = +oo /\ B e. RR ) -> -. +oo < B )
13		simpl 108	. . . . . . . . . 10 |- ( ( A = +oo /\ B e. RR ) -> A = +oo )
14	13	breq1d 3885	. . . . . . . . 9 |- ( ( A = +oo /\ B e. RR ) -> ( A < B <-> +oo < B ) )
15	12, 14	mtbird 639	. . . . . . . 8 |- ( ( A = +oo /\ B e. RR ) -> -. A < B )
16		0xr 7684	. . . . . . . . . 10 |- 0 e. RR*
17		nltmnf 9415	. . . . . . . . . 10 |- ( 0 e. RR* -> -. 0 < -oo )
18	16, 17	ax-mp 7	. . . . . . . . 9 |- -. 0 < -oo
19		xnegeq 9451	. . . . . . . . . . . . . 14 |- ( A = +oo -> -e A = -e +oo )
20	19	adantr 272	. . . . . . . . . . . . 13 |- ( ( A = +oo /\ B e. RR ) -> -e A = -e +oo )
21		xnegpnf 9452	. . . . . . . . . . . . 13 |- -e +oo = -oo
22	20, 21	syl6eq 2148	. . . . . . . . . . . 12 |- ( ( A = +oo /\ B e. RR ) -> -e A = -oo )
23	22	oveq2d 5722	. . . . . . . . . . 11 |- ( ( A = +oo /\ B e. RR ) -> ( B +e -e A ) = ( B +e -oo ) )
24		renepnf 7685	. . . . . . . . . . . . 13 |- ( B e. RR -> B =/= +oo )
25	24	adantl 273	. . . . . . . . . . . 12 |- ( ( A = +oo /\ B e. RR ) -> B =/= +oo )
26		xaddmnf1 9472	. . . . . . . . . . . 12 |- ( ( B e. RR* /\ B =/= +oo ) -> ( B +e -oo ) = -oo )
27	9, 25, 26	syl2an2 564	. . . . . . . . . . 11 |- ( ( A = +oo /\ B e. RR ) -> ( B +e -oo ) = -oo )
28	23, 27	eqtrd 2132	. . . . . . . . . 10 |- ( ( A = +oo /\ B e. RR ) -> ( B +e -e A ) = -oo )
29	28	breq2d 3887	. . . . . . . . 9 |- ( ( A = +oo /\ B e. RR ) -> ( 0 < ( B +e -e A ) <-> 0 < -oo ) )
30	18, 29	mtbiri 641	. . . . . . . 8 |- ( ( A = +oo /\ B e. RR ) -> -. 0 < ( B +e -e A ) )
31	15, 30	2falsed 659	. . . . . . 7 |- ( ( A = +oo /\ B e. RR ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
32	31	ex 114	. . . . . 6 |- ( A = +oo -> ( B e. RR -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
33		simpl 108	. . . . . . . . 9 |- ( ( A = -oo /\ B e. RR ) -> A = -oo )
34		mnflt 9410	. . . . . . . . . 10 |- ( B e. RR -> -oo < B )
35	34	adantl 273	. . . . . . . . 9 |- ( ( A = -oo /\ B e. RR ) -> -oo < B )
36	33, 35	eqbrtrd 3895	. . . . . . . 8 |- ( ( A = -oo /\ B e. RR ) -> A < B )
37		0ltpnf 9409	. . . . . . . . 9 |- 0 < +oo
38		xnegeq 9451	. . . . . . . . . . . . 13 |- ( A = -oo -> -e A = -e -oo )
39		xnegmnf 9453	. . . . . . . . . . . . 13 |- -e -oo = +oo
40	38, 39	syl6eq 2148	. . . . . . . . . . . 12 |- ( A = -oo -> -e A = +oo )
41	40	oveq2d 5722	. . . . . . . . . . 11 |- ( A = -oo -> ( B +e -e A ) = ( B +e +oo ) )
42	41	adantr 272	. . . . . . . . . 10 |- ( ( A = -oo /\ B e. RR ) -> ( B +e -e A ) = ( B +e +oo ) )
43		renemnf 7686	. . . . . . . . . . . 12 |- ( B e. RR -> B =/= -oo )
44	43	adantl 273	. . . . . . . . . . 11 |- ( ( A = -oo /\ B e. RR ) -> B =/= -oo )
45		xaddpnf1 9470	. . . . . . . . . . 11 |- ( ( B e. RR* /\ B =/= -oo ) -> ( B +e +oo ) = +oo )
46	9, 44, 45	syl2an2 564	. . . . . . . . . 10 |- ( ( A = -oo /\ B e. RR ) -> ( B +e +oo ) = +oo )
47	42, 46	eqtrd 2132	. . . . . . . . 9 |- ( ( A = -oo /\ B e. RR ) -> ( B +e -e A ) = +oo )
48	37, 47	syl5breqr 3911	. . . . . . . 8 |- ( ( A = -oo /\ B e. RR ) -> 0 < ( B +e -e A ) )
49	36, 48	2thd 174	. . . . . . 7 |- ( ( A = -oo /\ B e. RR ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
50	49	ex 114	. . . . . 6 |- ( A = -oo -> ( B e. RR -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
51	8, 32, 50	3jaoi 1249	. . . . 5 |- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( B e. RR -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
52	2, 51	sylbi 120	. . . 4 |- ( A e. RR* -> ( B e. RR -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
53		ltpnf 9408	. . . . . . . . . 10 |- ( A e. RR -> A < +oo )
54	53	adantr 272	. . . . . . . . 9 |- ( ( A e. RR /\ B = +oo ) -> A < +oo )
55		simpr 109	. . . . . . . . 9 |- ( ( A e. RR /\ B = +oo ) -> B = +oo )
56	54, 55	breqtrrd 3901	. . . . . . . 8 |- ( ( A e. RR /\ B = +oo ) -> A < B )
57	55	oveq1d 5721	. . . . . . . . . 10 |- ( ( A e. RR /\ B = +oo ) -> ( B +e -e A ) = ( +oo +e -e A ) )
58		rexneg 9454	. . . . . . . . . . . . . 14 |- ( A e. RR -> -e A = -u A )
59		renegcl 7894	. . . . . . . . . . . . . 14 |- ( A e. RR -> -u A e. RR )
60	58, 59	eqeltrd 2176	. . . . . . . . . . . . 13 |- ( A e. RR -> -e A e. RR )
61	60	rexrd 7687	. . . . . . . . . . . 12 |- ( A e. RR -> -e A e. RR* )
62	61	adantr 272	. . . . . . . . . . 11 |- ( ( A e. RR /\ B = +oo ) -> -e A e. RR* )
63	60	renemnfd 7689	. . . . . . . . . . . 12 |- ( A e. RR -> -e A =/= -oo )
64	63	adantr 272	. . . . . . . . . . 11 |- ( ( A e. RR /\ B = +oo ) -> -e A =/= -oo )
65		xaddpnf2 9471	. . . . . . . . . . 11 |- ( ( -e A e. RR* /\ -e A =/= -oo ) -> ( +oo +e -e A ) = +oo )
66	62, 64, 65	syl2anc 406	. . . . . . . . . 10 |- ( ( A e. RR /\ B = +oo ) -> ( +oo +e -e A ) = +oo )
67	57, 66	eqtrd 2132	. . . . . . . . 9 |- ( ( A e. RR /\ B = +oo ) -> ( B +e -e A ) = +oo )
68	37, 67	syl5breqr 3911	. . . . . . . 8 |- ( ( A e. RR /\ B = +oo ) -> 0 < ( B +e -e A ) )
69	56, 68	2thd 174	. . . . . . 7 |- ( ( A e. RR /\ B = +oo ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
70	69	ex 114	. . . . . 6 |- ( A e. RR -> ( B = +oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
71		pnfxr 7690	. . . . . . . . . 10 |- +oo e. RR*
72		xrltnr 9407	. . . . . . . . . 10 |- ( +oo e. RR* -> -. +oo < +oo )
73	71, 72	ax-mp 7	. . . . . . . . 9 |- -. +oo < +oo
74		breq12 3880	. . . . . . . . 9 |- ( ( A = +oo /\ B = +oo ) -> ( A < B <-> +oo < +oo ) )
75	73, 74	mtbiri 641	. . . . . . . 8 |- ( ( A = +oo /\ B = +oo ) -> -. A < B )
76		0re 7638	. . . . . . . . . 10 |- 0 e. RR
77	76	ltnri 7727	. . . . . . . . 9 |- -. 0 < 0
78		simpr 109	. . . . . . . . . . . 12 |- ( ( A = +oo /\ B = +oo ) -> B = +oo )
79	19, 21	syl6eq 2148	. . . . . . . . . . . . 13 |- ( A = +oo -> -e A = -oo )
80	79	adantr 272	. . . . . . . . . . . 12 |- ( ( A = +oo /\ B = +oo ) -> -e A = -oo )
81	78, 80	oveq12d 5724	. . . . . . . . . . 11 |- ( ( A = +oo /\ B = +oo ) -> ( B +e -e A ) = ( +oo +e -oo ) )
82		pnfaddmnf 9474	. . . . . . . . . . 11 |- ( +oo +e -oo ) = 0
83	81, 82	syl6eq 2148	. . . . . . . . . 10 |- ( ( A = +oo /\ B = +oo ) -> ( B +e -e A ) = 0 )
84	83	breq2d 3887	. . . . . . . . 9 |- ( ( A = +oo /\ B = +oo ) -> ( 0 < ( B +e -e A ) <-> 0 < 0 ) )
85	77, 84	mtbiri 641	. . . . . . . 8 |- ( ( A = +oo /\ B = +oo ) -> -. 0 < ( B +e -e A ) )
86	75, 85	2falsed 659	. . . . . . 7 |- ( ( A = +oo /\ B = +oo ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
87	86	ex 114	. . . . . 6 |- ( A = +oo -> ( B = +oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
88		mnfltpnf 9412	. . . . . . . . 9 |- -oo < +oo
89		breq12 3880	. . . . . . . . 9 |- ( ( A = -oo /\ B = +oo ) -> ( A < B <-> -oo < +oo ) )
90	88, 89	mpbiri 167	. . . . . . . 8 |- ( ( A = -oo /\ B = +oo ) -> A < B )
91		oveq1 5713	. . . . . . . . . . 11 |- ( B = +oo -> ( B +e +oo ) = ( +oo +e +oo ) )
92	41, 91	sylan9eq 2152	. . . . . . . . . 10 |- ( ( A = -oo /\ B = +oo ) -> ( B +e -e A ) = ( +oo +e +oo ) )
93		pnfnemnf 7692	. . . . . . . . . . 11 |- +oo =/= -oo
94		xaddpnf1 9470	. . . . . . . . . . 11 |- ( ( +oo e. RR* /\ +oo =/= -oo ) -> ( +oo +e +oo ) = +oo )
95	71, 93, 94	mp2an 420	. . . . . . . . . 10 |- ( +oo +e +oo ) = +oo
96	92, 95	syl6eq 2148	. . . . . . . . 9 |- ( ( A = -oo /\ B = +oo ) -> ( B +e -e A ) = +oo )
97	37, 96	syl5breqr 3911	. . . . . . . 8 |- ( ( A = -oo /\ B = +oo ) -> 0 < ( B +e -e A ) )
98	90, 97	2thd 174	. . . . . . 7 |- ( ( A = -oo /\ B = +oo ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
99	98	ex 114	. . . . . 6 |- ( A = -oo -> ( B = +oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
100	70, 87, 99	3jaoi 1249	. . . . 5 |- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( B = +oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
101	2, 100	sylbi 120	. . . 4 |- ( A e. RR* -> ( B = +oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
102		rexr 7683	. . . . . . . . . . 11 |- ( A e. RR -> A e. RR* )
103	102	adantr 272	. . . . . . . . . 10 |- ( ( A e. RR /\ B = -oo ) -> A e. RR* )
104		nltmnf 9415	. . . . . . . . . 10 |- ( A e. RR* -> -. A < -oo )
105	103, 104	syl 14	. . . . . . . . 9 |- ( ( A e. RR /\ B = -oo ) -> -. A < -oo )
106		simpr 109	. . . . . . . . . 10 |- ( ( A e. RR /\ B = -oo ) -> B = -oo )
107	106	breq2d 3887	. . . . . . . . 9 |- ( ( A e. RR /\ B = -oo ) -> ( A < B <-> A < -oo ) )
108	105, 107	mtbird 639	. . . . . . . 8 |- ( ( A e. RR /\ B = -oo ) -> -. A < B )
109	106	oveq1d 5721	. . . . . . . . . . 11 |- ( ( A e. RR /\ B = -oo ) -> ( B +e -e A ) = ( -oo +e -e A ) )
110		rexr 7683	. . . . . . . . . . . . . 14 |- ( -e A e. RR -> -e A e. RR* )
111		renepnf 7685	. . . . . . . . . . . . . 14 |- ( -e A e. RR -> -e A =/= +oo )
112		xaddmnf2 9473	. . . . . . . . . . . . . 14 |- ( ( -e A e. RR* /\ -e A =/= +oo ) -> ( -oo +e -e A ) = -oo )
113	110, 111, 112	syl2anc 406	. . . . . . . . . . . . 13 |- ( -e A e. RR -> ( -oo +e -e A ) = -oo )
114	60, 113	syl 14	. . . . . . . . . . . 12 |- ( A e. RR -> ( -oo +e -e A ) = -oo )
115	114	adantr 272	. . . . . . . . . . 11 |- ( ( A e. RR /\ B = -oo ) -> ( -oo +e -e A ) = -oo )
116	109, 115	eqtrd 2132	. . . . . . . . . 10 |- ( ( A e. RR /\ B = -oo ) -> ( B +e -e A ) = -oo )
117	116	breq2d 3887	. . . . . . . . 9 |- ( ( A e. RR /\ B = -oo ) -> ( 0 < ( B +e -e A ) <-> 0 < -oo ) )
118	18, 117	mtbiri 641	. . . . . . . 8 |- ( ( A e. RR /\ B = -oo ) -> -. 0 < ( B +e -e A ) )
119	108, 118	2falsed 659	. . . . . . 7 |- ( ( A e. RR /\ B = -oo ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
120	119	ex 114	. . . . . 6 |- ( A e. RR -> ( B = -oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
121		eleq1 2162	. . . . . . . . . . . 12 |- ( A = +oo -> ( A e. RR* <-> +oo e. RR* ) )
122	71, 121	mpbiri 167	. . . . . . . . . . 11 |- ( A = +oo -> A e. RR* )
123	122	adantr 272	. . . . . . . . . 10 |- ( ( A = +oo /\ B = -oo ) -> A e. RR* )
124	123, 104	syl 14	. . . . . . . . 9 |- ( ( A = +oo /\ B = -oo ) -> -. A < -oo )
125		simpr 109	. . . . . . . . . 10 |- ( ( A = +oo /\ B = -oo ) -> B = -oo )
126	125	breq2d 3887	. . . . . . . . 9 |- ( ( A = +oo /\ B = -oo ) -> ( A < B <-> A < -oo ) )
127	124, 126	mtbird 639	. . . . . . . 8 |- ( ( A = +oo /\ B = -oo ) -> -. A < B )
128	79	oveq2d 5722	. . . . . . . . . . . 12 |- ( A = +oo -> ( B +e -e A ) = ( B +e -oo ) )
129	128	adantr 272	. . . . . . . . . . 11 |- ( ( A = +oo /\ B = -oo ) -> ( B +e -e A ) = ( B +e -oo ) )
130		mnfxr 7694	. . . . . . . . . . . . 13 |- -oo e. RR*
131		eleq1 2162	. . . . . . . . . . . . 13 |- ( B = -oo -> ( B e. RR* <-> -oo e. RR* ) )
132	130, 131	mpbiri 167	. . . . . . . . . . . 12 |- ( B = -oo -> B e. RR* )
133		mnfnepnf 7693	. . . . . . . . . . . . . 14 |- -oo =/= +oo
134		neeq1 2280	. . . . . . . . . . . . . 14 |- ( B = -oo -> ( B =/= +oo <-> -oo =/= +oo ) )
135	133, 134	mpbiri 167	. . . . . . . . . . . . 13 |- ( B = -oo -> B =/= +oo )
136	135	adantl 273	. . . . . . . . . . . 12 |- ( ( A = +oo /\ B = -oo ) -> B =/= +oo )
137	132, 136, 26	syl2an2 564	. . . . . . . . . . 11 |- ( ( A = +oo /\ B = -oo ) -> ( B +e -oo ) = -oo )
138	129, 137	eqtrd 2132	. . . . . . . . . 10 |- ( ( A = +oo /\ B = -oo ) -> ( B +e -e A ) = -oo )
139	138	breq2d 3887	. . . . . . . . 9 |- ( ( A = +oo /\ B = -oo ) -> ( 0 < ( B +e -e A ) <-> 0 < -oo ) )
140	18, 139	mtbiri 641	. . . . . . . 8 |- ( ( A = +oo /\ B = -oo ) -> -. 0 < ( B +e -e A ) )
141	127, 140	2falsed 659	. . . . . . 7 |- ( ( A = +oo /\ B = -oo ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
142	141	ex 114	. . . . . 6 |- ( A = +oo -> ( B = -oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
143		xrltnr 9407	. . . . . . . . . 10 |- ( -oo e. RR* -> -. -oo < -oo )
144	130, 143	ax-mp 7	. . . . . . . . 9 |- -. -oo < -oo
145		breq12 3880	. . . . . . . . 9 |- ( ( A = -oo /\ B = -oo ) -> ( A < B <-> -oo < -oo ) )
146	144, 145	mtbiri 641	. . . . . . . 8 |- ( ( A = -oo /\ B = -oo ) -> -. A < B )
147		oveq1 5713	. . . . . . . . . . . 12 |- ( B = -oo -> ( B +e +oo ) = ( -oo +e +oo ) )
148	41, 147	sylan9eq 2152	. . . . . . . . . . 11 |- ( ( A = -oo /\ B = -oo ) -> ( B +e -e A ) = ( -oo +e +oo ) )
149		mnfaddpnf 9475	. . . . . . . . . . 11 |- ( -oo +e +oo ) = 0
150	148, 149	syl6eq 2148	. . . . . . . . . 10 |- ( ( A = -oo /\ B = -oo ) -> ( B +e -e A ) = 0 )
151	150	breq2d 3887	. . . . . . . . 9 |- ( ( A = -oo /\ B = -oo ) -> ( 0 < ( B +e -e A ) <-> 0 < 0 ) )
152	77, 151	mtbiri 641	. . . . . . . 8 |- ( ( A = -oo /\ B = -oo ) -> -. 0 < ( B +e -e A ) )
153	146, 152	2falsed 659	. . . . . . 7 |- ( ( A = -oo /\ B = -oo ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
154	153	ex 114	. . . . . 6 |- ( A = -oo -> ( B = -oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
155	120, 142, 154	3jaoi 1249	. . . . 5 |- ( ( A e. RR \/ A = +oo \/ A = -oo ) -> ( B = -oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
156	2, 155	sylbi 120	. . . 4 |- ( A e. RR* -> ( B = -oo -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
157	52, 101, 156	3jaod 1250	. . 3 |- ( A e. RR* -> ( ( B e. RR \/ B = +oo \/ B = -oo ) -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
158	1, 157	syl5bi 151	. 2 |- ( A e. RR* -> ( B e. RR* -> ( A < B <-> 0 < ( B +e -e A ) ) ) )
159	158	imp 123	1 |- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> 0 < ( B +e -e A ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ w3o 929   = wceq 1299   e. wcel 1448   =/= wne 2267   class class class wbr 3875  (class class class)co 5706   RRcr 7499   0cc0 7500   +oocpnf 7669   -oocmnf 7670   RR*cxr 7671   < clt 7672   - cmin 7804   -ucneg 7805   -ecxne 9397   +ecxad 9398

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 584  ax-in2 585  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-13 1459  ax-14 1460  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-sep 3986  ax-pow 4038  ax-pr 4069  ax-un 4293  ax-setind 4390  ax-cnex 7586  ax-resscn 7587  ax-1cn 7588  ax-1re 7589  ax-icn 7590  ax-addcl 7591  ax-addrcl 7592  ax-mulcl 7593  ax-addcom 7595  ax-addass 7597  ax-distr 7599  ax-i2m1 7600  ax-0id 7603  ax-rnegex 7604  ax-cnre 7606  ax-pre-ltirr 7607  ax-pre-ltadd 7611

This theorem depends on definitions:  df-bi 116  df-dc 787  df-3or 931  df-3an 932  df-tru 1302  df-fal 1305  df-nf 1405  df-sb 1704  df-eu 1963  df-mo 1964  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ne 2268  df-nel 2363  df-ral 2380  df-rex 2381  df-reu 2382  df-rab 2384  df-v 2643  df-sbc 2863  df-dif 3023  df-un 3025  df-in 3027  df-ss 3034  df-if 3422  df-pw 3459  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-opab 3930  df-id 4153  df-xp 4483  df-rel 4484  df-cnv 4485  df-co 4486  df-dm 4487  df-iota 5024  df-fun 5061  df-fv 5067  df-riota 5662  df-ov 5709  df-oprab 5710  df-mpo 5711  df-pnf 7674  df-mnf 7675  df-xr 7676  df-ltxr 7677  df-sub 7806  df-neg 7807  df-xneg 9400  df-xadd 9401

This theorem is referenced by: (None)