ltxr - Intuitionistic Logic Explorer

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

Theorem ltxr 9455

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 3900	. . . . 5 $/\$
2		df-3an 947	. . . . . 6 $/\$ $/\$ $/\$ $/\$
3	2	opabbii 3955	. . . . 5 $/\$ $/\$ $/\$ $/\$
4	1, 3	brab2ga 4574	. . . 4 $/\$ $/\$ $/\$ $/\$
5	4	a1i 9	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
6		brun 3941	. . . 4 $\/$
7		brxp 4530	. . . . . . 7 $/\$
8		elun 3183	. . . . . . . . . . 11 $\/$
9		orcom 700	. . . . . . . . . . 11 $\/$ $\/$
10	8, 9	bitri 183	. . . . . . . . . 10 $\/$
11		elsng 3508	. . . . . . . . . . 11
12	11	orbi1d 763	. . . . . . . . . 10 $\/$ $\/$
13	10, 12	syl5bb 191	. . . . . . . . 9 $\/$
14		elsng 3508	. . . . . . . . 9
15	13, 14	bi2anan9 578	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$
16		andir 791	. . . . . . . 8 $\/$ $/\$ $/\$ $\/$ $/\$
17	15, 16	syl6bb 195	. . . . . . 7 $/\$ $/\$ $/\$ $\/$ $/\$
18	7, 17	syl5bb 191	. . . . . 6 $/\$ $/\$ $\/$ $/\$
19		brxp 4530	. . . . . . 7 $/\$
20	11	anbi1d 458	. . . . . . . 8 $/\$ $/\$
21	20	adantr 272	. . . . . . 7 $/\$ $/\$ $/\$
22	19, 21	syl5bb 191	. . . . . 6 $/\$ $/\$
23	18, 22	orbi12d 765	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
24		orass 739	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
25	23, 24	syl6bb 195	. . . 4 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	6, 25	syl5bb 191	. . 3 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
27	5, 26	orbi12d 765	. 2 $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
28		df-ltxr 7729	. . . 4 $/\$ $/\$
29	28	breqi 3901	. . 3 $/\$ $/\$
30		brun 3941	. . 3 $/\$ $/\$ $/\$ $/\$ $\/$
31	29, 30	bitri 183	. 2 $/\$ $/\$ $\/$
32		orass 739	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
33	27, 31, 32	3bitr4g 222	1 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 680 $/\$ w3a 945

wceq 1314

wcel 1463

cun 3035

csn 3493 class class class wbr 3895

copab 3948

cxp 4497

cr 7546

cltrr 7551

cpnf 7721

cmnf 7722

cxr 7723

clt 7724

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-14 1475 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 ax-sep 4006 ax-pow 4058 ax-pr 4091

This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-eu 1978 df-mo 1979 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-ral 2395 df-rex 2396 df-v 2659 df-un 3041 df-in 3043 df-ss 3050 df-pw 3478 df-sn 3499 df-pr 3500 df-op 3502 df-br 3896 df-opab 3950 df-xp 4505 df-ltxr 7729

This theorem is referenced by: xrltnr 9459 ltpnf 9460 mnflt 9462 mnfltpnf 9464 pnfnlt 9466 nltmnf 9467

W3C validator