ltxr - Intuitionistic Logic Explorer

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

Theorem ltxr 9850

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 4038	. . . . 5 $/\$
2		df-3an 982	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4100	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4738	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 9	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4084	. . . 4 $\/$
7		brxp 4694	. . . . . . 7 $/\$
8		elun 3304	. . . . . . . . . . 11 $\/$
9		orcom 729	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 184	. . . . . . . . . 10 $\/$
11		elsng 3637	. . . . . . . . . . 11
12	11	orbi1d 792	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	bitrid 192	. . . . . . . . 9 $\/$
14		elsng 3637	. . . . . . . . 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 4694	. . . . . . 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 8066	. . . 4 $/\$ $/\$
29	28	breqi 4039	. . 3 $/\$ $/\$
30		brun 4084	. . 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 3622 class class class wbr 4033

copab 4093

cxp 4661

cr 7878

cltrr 7883

cpnf 8058

cmnf 8059

cxr 8060

clt 8061

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 4151 ax-pow 4207 ax-pr 4242

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 3607 df-sn 3628 df-pr 3629 df-op 3631 df-br 4034 df-opab 4095 df-xp 4669 df-ltxr 8066

This theorem is referenced by: xrltnr 9854 ltpnf 9855 mnflt 9858 mnfltpnf 9860 pnfnlt 9862 nltmnf 9863

W3C validator