xrltnrt - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem xrltnrt 5522

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

**Assertion**
Ref	Expression
xrltnrt

**Proof of Theorem xrltnrt**
Step	Hyp	Ref	Expression
1		elxr 5516	. 2 $\/$ $\/$
2		ltnrt 5511	. . 3
3		pnfnre 5476	. . . . . . . . . 10
4		df-nel 1585	. . . . . . . . . 10
5	3, 4	mpbi 189	. . . . . . . . 9
6	5	intnan 690	. . . . . . . 8 $/\$
7	6	intnanr 691	. . . . . . 7 $/\$ $/\$
8		pnfnemnf 5517	. . . . . . . . 9
9		df-ne 1584	. . . . . . . . 9
10	8, 9	mpbi 189	. . . . . . . 8
11	10	intnanr 691	. . . . . . 7 $/\$
12	7, 11	pm3.2ni 579	. . . . . 6 $/\$ $/\$ $\/$ $/\$
13	5	intnanr 691	. . . . . . 7 $/\$
14	5	intnan 690	. . . . . . 7 $/\$
15	13, 14	pm3.2ni 579	. . . . . 6 $/\$ $\/$ $/\$
16	12, 15	pm3.2ni 579	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
17		pnfxr 5473	. . . . . 6
18		ltxrt 5475	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
19	17, 17, 18	mp2an 696	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
20	16, 19	mtbir 192	. . . 4
21		breq12 2619	. . . . 5 $/\$
22	21	anidms 434	. . . 4
23	20, 22	mtbiri 716	. . 3
24		mnfnre 5477	. . . . . . . . . 10
25		df-nel 1585	. . . . . . . . . 10
26	24, 25	mpbi 189	. . . . . . . . 9
27	26	intnan 690	. . . . . . . 8 $/\$
28	27	intnanr 691	. . . . . . 7 $/\$ $/\$
29		necom 1633	. . . . . . . . . 10
30	8, 29	mpbi 189	. . . . . . . . 9
31		df-ne 1584	. . . . . . . . 9
32	30, 31	mpbi 189	. . . . . . . 8
33	32	intnan 690	. . . . . . 7 $/\$
34	28, 33	pm3.2ni 579	. . . . . 6 $/\$ $/\$ $\/$ $/\$
35	26	intnanr 691	. . . . . . 7 $/\$
36	26	intnan 690	. . . . . . 7 $/\$
37	35, 36	pm3.2ni 579	. . . . . 6 $/\$ $\/$ $/\$
38	34, 37	pm3.2ni 579	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
39		mnfxr 5474	. . . . . 6
40		ltxrt 5475	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
41	39, 39, 40	mp2an 696	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
42	38, 41	mtbir 192	. . . 4
43		breq12 2619	. . . . 5 $/\$
44	43	anidms 434	. . . 4
45	42, 44	mtbiri 716	. . 3
46	2, 23, 45	3jaoi 885	. 2 $\/$ $\/$
47	1, 46	sylbi 199	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 146 $\/$ wo 222 $/\$ wa 223 $\/$ w3o 773

wceq 954

wcel 956

wne 1582

wnel 1583 class class class wbr 2614

cr 5213

cltrr 5218

cpnf 5463

cmnf 5464

cxr 5465

clt 5466

This theorem is referenced by: xrltnsymt 5531 xrlttrit 5533 nltpnftt 5547 ngtmnftt 5548 xrsupsslem 6031 xrinfmsslem 6032 xrub 6035

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-9 963 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-rep 2688 ax-sep 2698 ax-nul 2705 ax-pow 2737 ax-pr 2774 ax-un 2861 ax-inf2 4605

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-nel 1585 df-ral 1646 df-rex 1647 df-reu 1648 df-rab 1649 df-v 1808 df-sbc 1938 df-csb 1998 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pss 2051 df-nul 2277 df-if 2358 df-pw 2398 df-sn 2408 df-pr 2409 df-tp 2411 df-op 2412 df-uni 2499 df-int 2529 df-iun 2563 df-br 2615 df-opab 2662 df-tr 2676 df-eprel 2827 df-id 2830 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-on 2947 df-lim 2948 df-suc 2949 df-om 3127 df-xp 3179 df-rel 3180 df-cnv 3181 df-co 3182 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fun 3187 df-fn 3188 df-f 3189 df-f1 3190 df-fo 3191 df-f1o 3192 df-fv 3193 df-rdg 3923 df-opr 3956 df-oprab 3957 df-1st 4069 df-2nd 4070 df-1o 4123 df-oadd 4125 df-omul 4126 df-er 4251 df-ec 4253 df-qs 4256 df-en 4357 df-dom 4358 df-sdom 4359 df-ni 4980 df-pli 4981 df-mi 4982 df-lti 4983 df-plpq 5015 df-mpq 5016 df-enq 5017 df-nq 5018 df-plq 5019 df-mq 5020 df-rq 5021 df-ltq 5022 df-1q 5023 df-np 5066 df-1p 5067 df-plp 5068 df-ltp 5070 df-enr 5146 df-nr 5147 df-ltr 5150 df-0r 5151 df-c 5220 df-r 5224 df-lt 5227 df-pnf 5467 df-mnf 5468 df-xr 5469 df-ltxr 5470