![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ltrelnq | GIF version |
Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) |
Ref | Expression |
---|---|
ltrelnq | โข <Q โ (Q ร Q) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ltnqqs 7351 | . 2 โข <Q = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ Q โง ๐ฆ โ Q) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง ๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง (๐ง ยทN ๐ข) <N (๐ค ยทN ๐ฃ)))} | |
2 | opabssxp 4700 | . 2 โข {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ Q โง ๐ฆ โ Q) โง โ๐งโ๐คโ๐ฃโ๐ข((๐ฅ = [โจ๐ง, ๐คโฉ] ~Q โง ๐ฆ = [โจ๐ฃ, ๐ขโฉ] ~Q ) โง (๐ง ยทN ๐ข) <N (๐ค ยทN ๐ฃ)))} โ (Q ร Q) | |
3 | 1, 2 | eqsstri 3187 | 1 โข <Q โ (Q ร Q) |
Copyright terms: Public domain | W3C validator |