Definition df-ltnq

Description: Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. Similar to Definition 5 of Suppes p. 162. (Contributed by NM, 13-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ltnq	⊢ <Q = ( <pQ ∩ ( Q × Q ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cltq	⊢ <Q
1		cltpq	⊢ <pQ
2		cnq	⊢ Q
3	2 2	cxp	⊢ ( Q × Q )
4	1 3	cin	⊢ ( <pQ ∩ ( Q × Q ) )
5	0 4	wceq	⊢ <Q = ( <pQ ∩ ( Q × Q ) )