ltxr - Intuitionistic Logic Explorer

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

Theorem ltxr 10009

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 4093	. . . . 5 $/\$
2		df-3an 1006	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 4156	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4801	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 9	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 4140	. . . 4 $\/$
7		brxp 4756	. . . . . . 7 $/\$
8		elun 3348	. . . . . . . . . . 11 $\/$
9		orcom 735	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 184	. . . . . . . . . 10 $\/$
11		elsng 3684	. . . . . . . . . . 11
12	11	orbi1d 798	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	bitrid 192	. . . . . . . . 9 $\/$
14		elsng 3684	. . . . . . . . 9
15	13, 14	bi2anan9 610	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 826	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	bitrdi 196	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	bitrid 192	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 4756	. . . . . . 7 $/\$
20	11	anbi1d 465	. . . . . . . 8 $/\$ $/\$
21	20	adantr 276	. . . . . . 7 $/\$ $/\$ $/\$
22	19, 21	bitrid 192	. . . . . 6 $/\$ $/\$
23	18, 22	orbi12d 800	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		orass 774	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
25	23, 24	bitrdi 196	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	6, 25	bitrid 192	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
27	5, 26	orbi12d 800	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
28		df-ltxr 8218	. . . 4 $/\$ $/\$
29	28	breqi 4094	. . 3 $/\$ $/\$
30		brun 4140	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
31	29, 30	bitri 184	. 2 $/\$ $/\$ $\/$
32		orass 774	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33	27, 31, 32	3bitr4g 223	1 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 715 $/\$ w3a 1004

wceq 1397

wcel 2202

cun 3198

csn 3669 class class class wbr 4088

copab 4149

cxp 4723

cr 8030

cltrr 8035

cpnf 8210

cmnf 8211

cxr 8212

clt 8213

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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-v 2804 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-br 4089 df-opab 4151 df-xp 4731 df-ltxr 8218

This theorem is referenced by: xrltnr 10013 ltpnf 10014 mnflt 10017 mnfltpnf 10019 pnfnlt 10021 nltmnf 10022

W3C validator