xrltnr - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xrltnr		Unicode version

Theorem xrltnr 8931

Description: The extended real 'less than' is irreflexive. (Contributed by NM, 14-Oct-2005.)

**Assertion**
Ref	Expression
xrltnr

**Proof of Theorem xrltnr**
Step	Hyp	Ref	Expression
1		elxr 8928	. 2 $\/$ $\/$
2		ltnr 7255	. . 3
3		pnfnre 7222	. . . . . . . . . 10
4	3	neli 2342	. . . . . . . . 9
5	4	intnan 872	. . . . . . . 8 $/\$
6	5	intnanr 873	. . . . . . 7 $/\$ $/\$
7		pnfnemnf 7235	. . . . . . . . 9
8	7	neii 2248	. . . . . . . 8
9	8	intnanr 873	. . . . . . 7 $/\$
10	6, 9	pm3.2ni 760	. . . . . 6 $/\$ $/\$ $\/$ $/\$
11	4	intnanr 873	. . . . . . 7 $/\$
12	4	intnan 872	. . . . . . 7 $/\$
13	11, 12	pm3.2ni 760	. . . . . 6 $/\$ $\/$ $/\$
14	10, 13	pm3.2ni 760	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
15		pnfxr 7233	. . . . . 6
16		ltxr 8927	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
17	15, 15, 16	mp2an 417	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
18	14, 17	mtbir 629	. . . 4
19		breq12 3798	. . . . 5 $/\$
20	19	anidms 389	. . . 4
21	18, 20	mtbiri 633	. . 3
22		mnfnre 7223	. . . . . . . . . 10
23	22	neli 2342	. . . . . . . . 9
24	23	intnan 872	. . . . . . . 8 $/\$
25	24	intnanr 873	. . . . . . 7 $/\$ $/\$
26	7	nesymi 2292	. . . . . . . 8
27	26	intnan 872	. . . . . . 7 $/\$
28	25, 27	pm3.2ni 760	. . . . . 6 $/\$ $/\$ $\/$ $/\$
29	23	intnanr 873	. . . . . . 7 $/\$
30	23	intnan 872	. . . . . . 7 $/\$
31	29, 30	pm3.2ni 760	. . . . . 6 $/\$ $\/$ $/\$
32	28, 31	pm3.2ni 760	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33		mnfxr 7237	. . . . . 6
34		ltxr 8927	. . . . . 6 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
35	33, 33, 34	mp2an 417	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
36	32, 35	mtbir 629	. . . 4
37		breq12 3798	. . . . 5 $/\$
38	37	anidms 389	. . . 4
39	36, 38	mtbiri 633	. . 3
40	2, 21, 39	3jaoi 1235	. 2 $\/$ $\/$
41	1, 40	sylbi 119	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 102

wb 103 $\/$ wo 662 $\/$ w3o 919

wceq 1285

wcel 1434 class class class wbr 3793

cr 7042

cltrr 7047

cpnf 7212

cmnf 7213

cxr 7214

clt 7215

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3904 ax-pow 3956 ax-pr 3972 ax-un 4196 ax-setind 4288 ax-cnex 7129 ax-resscn 7130 ax-pre-ltirr 7150

This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-nel 2341 df-ral 2354 df-rex 2355 df-rab 2358 df-v 2604 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-br 3794 df-opab 3848 df-xp 4377 df-pnf 7217 df-mnf 7218 df-xr 7219 df-ltxr 7220

This theorem is referenced by: xrltnsym 8944 xrltso 8947 xrlttri3 8948 xrleid 8950 xrltne 8959 nltpnft 8960 ngtmnft 8961 xrrebnd 8962 lbioog 9012 ubioog 9013