Theorem qextle

Description: An extensionality-like property for extended real ordering. (Contributed by Mario Carneiro, 3-Oct-2014)

	Ref	Expression
Assertion	qextle	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \forall x\in \mathbb{Q}\left(x\le A\leftrightarrow x\le B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq2	$$⊢A=B\to \left(x\le A\leftrightarrow x\le B\right)$$
2	1	ralrimivw	$$⊢A=B\to \forall x\in \mathbb{Q}\left(x\le A\leftrightarrow x\le B\right)$$
3		xrlttri2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\ne B\leftrightarrow \left(A<B\vee B<A\right)\right)$$
4		qextltlem	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\to \exists x\in \mathbb{Q}\left(\neg \left(x<A\leftrightarrow x<B\right)\wedge \neg \left(x\le A\leftrightarrow x\le B\right)\right)\right)$$
5		simpr	$$⊢\left(\neg \left(x<A\leftrightarrow x<B\right)\wedge \neg \left(x\le A\leftrightarrow x\le B\right)\right)\to \neg \left(x\le A\leftrightarrow x\le B\right)$$
6	5	reximi	$$⊢\exists x\in \mathbb{Q}\left(\neg \left(x<A\leftrightarrow x<B\right)\wedge \neg \left(x\le A\leftrightarrow x\le B\right)\right)\to \exists x\in \mathbb{Q}\neg \left(x\le A\leftrightarrow x\le B\right)$$
7	4 6	syl6	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\to \exists x\in \mathbb{Q}\neg \left(x\le A\leftrightarrow x\le B\right)\right)$$
8		qextltlem	$$⊢\left(B\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(B<A\to \exists x\in \mathbb{Q}\left(\neg \left(x<B\leftrightarrow x<A\right)\wedge \neg \left(x\le B\leftrightarrow x\le A\right)\right)\right)$$
9		simpr	$$⊢\left(\neg \left(x<B\leftrightarrow x<A\right)\wedge \neg \left(x\le B\leftrightarrow x\le A\right)\right)\to \neg \left(x\le B\leftrightarrow x\le A\right)$$
10		bicom	$$⊢\left(x\le B\leftrightarrow x\le A\right)\leftrightarrow \left(x\le A\leftrightarrow x\le B\right)$$
11	9 10	sylnib	$$⊢\left(\neg \left(x<B\leftrightarrow x<A\right)\wedge \neg \left(x\le B\leftrightarrow x\le A\right)\right)\to \neg \left(x\le A\leftrightarrow x\le B\right)$$
12	11	reximi	$$⊢\exists x\in \mathbb{Q}\left(\neg \left(x<B\leftrightarrow x<A\right)\wedge \neg \left(x\le B\leftrightarrow x\le A\right)\right)\to \exists x\in \mathbb{Q}\neg \left(x\le A\leftrightarrow x\le B\right)$$
13	8 12	syl6	$$⊢\left(B\in {ℝ}^{*}\wedge A\in {ℝ}^{*}\right)\to \left(B<A\to \exists x\in \mathbb{Q}\neg \left(x\le A\leftrightarrow x\le B\right)\right)$$
14	13	ancoms	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(B<A\to \exists x\in \mathbb{Q}\neg \left(x\le A\leftrightarrow x\le B\right)\right)$$
15	7 14	jaod	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\left(A<B\vee B<A\right)\to \exists x\in \mathbb{Q}\neg \left(x\le A\leftrightarrow x\le B\right)\right)$$
16	3 15	sylbid	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\ne B\to \exists x\in \mathbb{Q}\neg \left(x\le A\leftrightarrow x\le B\right)\right)$$
17		rexnal	$$⊢\exists x\in \mathbb{Q}\neg \left(x\le A\leftrightarrow x\le B\right)\leftrightarrow \neg \forall x\in \mathbb{Q}\left(x\le A\leftrightarrow x\le B\right)$$
18	16 17	syl6ib	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A\ne B\to \neg \forall x\in \mathbb{Q}\left(x\le A\leftrightarrow x\le B\right)\right)$$
19	18	necon4ad	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(\forall x\in \mathbb{Q}\left(x\le A\leftrightarrow x\le B\right)\to A=B\right)$$
20	2 19	impbid2	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \forall x\in \mathbb{Q}\left(x\le A\leftrightarrow x\le B\right)\right)$$