xrltnr - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem xrltnr 6716

Description: The extended real 'less than' is irreflexive.

**Assertion**
Ref	Expression
xrltnr

**Proof of Theorem xrltnr**
Step	Hyp	Ref	Expression
1		elxr 6706	. 2 $\/$ $\/$
2		ltnr 6700	. . 3
3		pnfnre 6665	. . . . . . . . . 10
4		df-nel 2020	. . . . . . . . . 10
5	3, 4	mpbi 206	. . . . . . . . 9
6	5	intnan 755	. . . . . . . 8 $/\$
7	6	intnanr 756	. . . . . . 7 $/\$ $/\$
8		pnfnemnf 6707	. . . . . . . . 9
9		df-ne 2019	. . . . . . . . 9
10	8, 9	mpbi 206	. . . . . . . 8
11	10	intnanr 756	. . . . . . 7 $/\$
12	7, 11	pm3.2ni 640	. . . . . 6 $/\$ $/\$ $\/$ $/\$
13	5	intnanr 756	. . . . . . 7 $/\$
14	5	intnan 755	. . . . . . 7 $/\$
15	13, 14	pm3.2ni 640	. . . . . 6 $/\$ $\/$ $/\$
16	12, 15	pm3.2ni 640	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
17		pnfxr 6660	. . . . . 6
18		ltxr 6664	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
19	17, 17, 18	mp2an 761	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
20	16, 19	mtbir 209	. . . 4
21		breq12 3343	. . . . 5 $/\$
22	21	anidms 480	. . . 4
23	20, 22	mtbiri 785	. . 3
24		mnfnre 6666	. . . . . . . . . 10
25		df-nel 2020	. . . . . . . . . 10
26	24, 25	mpbi 206	. . . . . . . . 9
27	26	intnan 755	. . . . . . . 8 $/\$
28	27	intnanr 756	. . . . . . 7 $/\$ $/\$
29		necom 2094	. . . . . . . . . 10
30	8, 29	mpbi 206	. . . . . . . . 9
31		df-ne 2019	. . . . . . . . 9
32	30, 31	mpbi 206	. . . . . . . 8
33	32	intnan 755	. . . . . . 7 $/\$
34	28, 33	pm3.2ni 640	. . . . . 6 $/\$ $/\$ $\/$ $/\$
35	26	intnanr 756	. . . . . . 7 $/\$
36	26	intnan 755	. . . . . . 7 $/\$
37	35, 36	pm3.2ni 640	. . . . . 6 $/\$ $\/$ $/\$
38	34, 37	pm3.2ni 640	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
39		mnfxr 6662	. . . . . 6
40		ltxr 6664	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
41	39, 39, 40	mp2an 761	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
42	38, 41	mtbir 209	. . . 4
43		breq12 3343	. . . . 5 $/\$
44	43	anidms 480	. . . 4
45	42, 44	mtbiri 785	. . 3
46	2, 23, 45	3jaoi 1160	. 2 $\/$ $\/$
47	1, 46	sylbi 216	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 163 $\/$ wo 239 $/\$ wa 240 $\/$ w3o 857

wceq 1298

wcel 1300

wne 2017

wnel 2018 class class class wbr 3338

cr 6385

cltrr 6390

cpnf 6650

cmnf 6651

cxr 6652

clt 6653

This theorem is referenced by: xrltnsym 6725 xrlttri 6727 nltpnft 6741 ngtmnft 6742 xrsupsslem 7285 xrinfmsslem 7286 xrub 7289 xrltneNEW 16434

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-nel 2020 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-1st 5020 df-2nd 5021 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-en 5427 df-dom 5428 df-sdom 5429 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 df-plp 6240 df-ltp 6242 df-enr 6318 df-nr 6319 df-ltr 6322 df-0r 6323 df-c 6392 df-r 6396 df-lt 6399 df-pnf 6654 df-mnf 6655 df-xr 6656 df-ltxr 6657