ltxr - Intuitionistic Logic Explorer

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

Theorem ltxr 8927

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 3798	. . . . 5 $/\$
2		df-3an 922	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 3853	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4441	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 9	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 3839	. . . 4 $\/$
7		brxp 4401	. . . . . . 7 $/\$
8		elun 3114	. . . . . . . . . . 11 $\/$
9		orcom 680	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 182	. . . . . . . . . 10 $\/$
11		elsng 3421	. . . . . . . . . . 11
12	11	orbi1d 738	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	syl5bb 190	. . . . . . . . 9 $\/$
14		elsng 3421	. . . . . . . . 9
15	13, 14	bi2anan9 571	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 766	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	syl6bb 194	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	syl5bb 190	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 4401	. . . . . . 7 $/\$
20	11	anbi1d 453	. . . . . . . 8 $/\$ $/\$
21	20	adantr 270	. . . . . . 7 $/\$ $/\$ $/\$
22	19, 21	syl5bb 190	. . . . . 6 $/\$ $/\$
23	18, 22	orbi12d 740	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		orass 717	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
25	23, 24	syl6bb 194	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	6, 25	syl5bb 190	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
27	5, 26	orbi12d 740	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
28		df-ltxr 7220	. . . 4 $/\$ $/\$
29	28	breqi 3799	. . 3 $/\$ $/\$
30		brun 3839	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
31	29, 30	bitri 182	. 2 $/\$ $/\$ $\/$
32		orass 717	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33	27, 31, 32	3bitr4g 221	1 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 102

wb 103 $\/$ wo 662 $/\$ w3a 920

wceq 1285

wcel 1434

cun 2972

csn 3406 class class class wbr 3793

copab 3846

cxp 4369

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-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-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

This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 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-ral 2354 df-rex 2355 df-v 2604 df-un 2978 df-in 2980 df-ss 2987 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-br 3794 df-opab 3848 df-xp 4377 df-ltxr 7220

This theorem is referenced by: xrltnr 8931 ltpnf 8932 mnflt 8934 mnfltpnf 8936 pnfnlt 8938 nltmnf 8939

W3C validator