Theorem gt-lth

Description: Relationship between < and > using hypotheses. (Contributed by David A. Wheeler, 19-Apr-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	gt-lth.1	$$⊢A\in \mathrm{V}$$
	gt-lth.2	$$⊢B\in \mathrm{V}$$
Assertion	gt-lth	$$⊢A>B\leftrightarrow B<A$$

Proof

Step	Hyp	Ref	Expression
1		gt-lth.1	$$⊢A\in \mathrm{V}$$
2		gt-lth.2	$$⊢B\in \mathrm{V}$$
3		df-gt	$$⊢>={<}^{-1}$$
4	3	breqi	$$⊢A>B\leftrightarrow A{<}^{-1}B$$
5	1 2	brcnv	$$⊢A{<}^{-1}B\leftrightarrow B<A$$
6	4 5	bitri	$$⊢A>B\leftrightarrow B<A$$