ltxr - Intuitionistic Logic Explorer

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

Theorem ltxr 9867

Description: The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 14-Oct-2005.)

**Assertion**
Ref	Expression
ltxr	$/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Proof of Theorem ltxr Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq12 4039	. . . . 5 $/\$
2		df-3an 982	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4101	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4739	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 9	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4085	. . . 4 $\/$
7		brxp 4695	. . . . . . 7 $/\$
8		elun 3305	. . . . . . . . . . 11 $\/$
9		orcom 729	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 184	. . . . . . . . . 10 $\/$
11		elsng 3638	. . . . . . . . . . 11
12	11	orbi1d 792	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	bitrid 192	. . . . . . . . 9 $\/$
14		elsng 3638	. . . . . . . . 9
15	13, 14	bi2anan9 606	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 820	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	bitrdi 196	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	bitrid 192	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 4695	. . . . . . 7 $/\$
20	11	anbi1d 465	. . . . . . . 8 $/\$ $/\$
21	20	adantr 276	. . . . . . 7 $/\$ $/\$ $/\$
22	19, 21	bitrid 192	. . . . . 6 $/\$ $/\$
23	18, 22	orbi12d 794	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		orass 768	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
25	23, 24	bitrdi 196	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	6, 25	bitrid 192	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
27	5, 26	orbi12d 794	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
28		df-ltxr 8083	. . . 4 $/\$ $/\$
29	28	breqi 4040	. . 3 $/\$ $/\$
30		brun 4085	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
31	29, 30	bitri 184	. 2 $/\$ $/\$ $\/$
32		orass 768	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33	27, 31, 32	3bitr4g 223	1 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 $/\$ w3a 980

wceq 1364

wcel 2167

cun 3155

csn 3623 class class class wbr 4034

copab 4094

cxp 4662

cr 7895

cltrr 7900

cpnf 8075

cmnf 8076

cxr 8077

clt 8078

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-pr 4243

This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ral 2480 df-rex 2481 df-v 2765 df-un 3161 df-in 3163 df-ss 3170 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-br 4035 df-opab 4096 df-xp 4670 df-ltxr 8083

This theorem is referenced by: xrltnr 9871 ltpnf 9872 mnflt 9875 mnfltpnf 9877 pnfnlt 9879 nltmnf 9880

W3C validator