Theorem pinq

Description: The representatives of positive integers as positive fractions. (Contributed by NM, 29-Oct-1995) (Revised by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	pinq	$$⊢A\in 𝑵\to ⟨A,1_{𝑜}⟩\in 𝑸$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢x=⟨A,1_{𝑜}⟩\to \left(x{~}_{𝑸}y\leftrightarrow ⟨A,1_{𝑜}⟩{~}_{𝑸}y\right)$$
2		fveq2	$$⊢x=⟨A,1_{𝑜}⟩\to 2^{nd}\left(x\right)=2^{nd}\left(⟨A,1_{𝑜}⟩\right)$$
3	2	breq2d	$$⊢x=⟨A,1_{𝑜}⟩\to \left(2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\leftrightarrow 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(⟨A,1_{𝑜}⟩\right)\right)$$
4	3	notbid	$$⊢x=⟨A,1_{𝑜}⟩\to \left(\neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\leftrightarrow \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(⟨A,1_{𝑜}⟩\right)\right)$$
5	1 4	imbi12d	$$⊢x=⟨A,1_{𝑜}⟩\to \left(\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)\leftrightarrow \left(⟨A,1_{𝑜}⟩{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(⟨A,1_{𝑜}⟩\right)\right)\right)$$
6	5	ralbidv	$$⊢x=⟨A,1_{𝑜}⟩\to \left(\forall y\in \left(𝑵\times 𝑵\right)\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)\leftrightarrow \forall y\in \left(𝑵\times 𝑵\right)\left(⟨A,1_{𝑜}⟩{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(⟨A,1_{𝑜}⟩\right)\right)\right)$$
7		1pi	$$⊢1_{𝑜}\in 𝑵$$
8		opelxpi	$$⊢\left(A\in 𝑵\wedge 1_{𝑜}\in 𝑵\right)\to ⟨A,1_{𝑜}⟩\in \left(𝑵\times 𝑵\right)$$
9	7 8	mpan2	$$⊢A\in 𝑵\to ⟨A,1_{𝑜}⟩\in \left(𝑵\times 𝑵\right)$$
10		nlt1pi	$$⊢\neg 2^{nd}\left(y\right){<}_{𝑵}{1}_{𝑜}$$
11		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
12		op2ndg	$$⊢\left(A\in 𝑵\wedge 1_{𝑜}\in \mathrm{V}\right)\to 2^{nd}\left(⟨A,1_{𝑜}⟩\right)=1_{𝑜}$$
13	11 12	mpan2	$$⊢A\in 𝑵\to 2^{nd}\left(⟨A,1_{𝑜}⟩\right)=1_{𝑜}$$
14	13	breq2d	$$⊢A\in 𝑵\to \left(2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(⟨A,1_{𝑜}⟩\right)\leftrightarrow 2^{nd}\left(y\right){<}_{𝑵}{1}_{𝑜}\right)$$
15	10 14	mtbiri	$$⊢A\in 𝑵\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(⟨A,1_{𝑜}⟩\right)$$
16	15	a1d	$$⊢A\in 𝑵\to \left(⟨A,1_{𝑜}⟩{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(⟨A,1_{𝑜}⟩\right)\right)$$
17	16	ralrimivw	$$⊢A\in 𝑵\to \forall y\in \left(𝑵\times 𝑵\right)\left(⟨A,1_{𝑜}⟩{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(⟨A,1_{𝑜}⟩\right)\right)$$
18	6 9 17	elrabd	$$⊢A\in 𝑵\to ⟨A,1_{𝑜}⟩\in \left\{x\in \left(𝑵\times 𝑵\right)|\forall y\in \left(𝑵\times 𝑵\right)\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)\right\}$$
19		df-nq	$$⊢𝑸=\left\{x\in \left(𝑵\times 𝑵\right)|\forall y\in \left(𝑵\times 𝑵\right)\left(x{~}_{𝑸}y\to \neg 2^{nd}\left(y\right){<}_{𝑵}{2}^{nd}\left(x\right)\right)\right\}$$
20	18 19	eleqtrrdi	$$⊢A\in 𝑵\to ⟨A,1_{𝑜}⟩\in 𝑸$$