Theorem dmrecnq

Description: Domain of reciprocal on positive fractions. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 10-Jul-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	dmrecnq	$$⊢\mathrm{dom}{*}_{𝑸}=𝑸$$

Proof

Step	Hyp	Ref	Expression
1		df-rq	$$⊢{*}_{𝑸}={{\cdot }_{𝑸}}^{-1}\left[\left\{1_{𝑸}\right\}\right]$$
2		cnvimass	$$⊢{{\cdot }_{𝑸}}^{-1}\left[\left\{1_{𝑸}\right\}\right]\subseteq \mathrm{dom}{\cdot }_{𝑸}$$
3	1 2	eqsstri	$$⊢{*}_{𝑸}\subseteq \mathrm{dom}{\cdot }_{𝑸}$$
4		mulnqf	$$⊢{\cdot }_{𝑸}:𝑸\times 𝑸⟶𝑸$$
5	4	fdmi	$$⊢\mathrm{dom}{\cdot }_{𝑸}=𝑸\times 𝑸$$
6	3 5	sseqtri	$$⊢{*}_{𝑸}\subseteq 𝑸\times 𝑸$$
7		dmss	$$⊢{*}_{𝑸}\subseteq 𝑸\times 𝑸\to \mathrm{dom}{*}_{𝑸}\subseteq \mathrm{dom}\left(𝑸\times 𝑸\right)$$
8	6 7	ax-mp	$$⊢\mathrm{dom}{*}_{𝑸}\subseteq \mathrm{dom}\left(𝑸\times 𝑸\right)$$
9		dmxpid	$$⊢\mathrm{dom}\left(𝑸\times 𝑸\right)=𝑸$$
10	8 9	sseqtri	$$⊢\mathrm{dom}{*}_{𝑸}\subseteq 𝑸$$
11		recclnq	$$⊢x\in 𝑸\to {*}_{𝑸}\left(x\right)\in 𝑸$$
12		opelxpi	$$⊢\left(x\in 𝑸\wedge {*}_{𝑸}\left(x\right)\in 𝑸\right)\to ⟨x,{*}_{𝑸}\left(x\right)⟩\in \left(𝑸\times 𝑸\right)$$
13	11 12	mpdan	$$⊢x\in 𝑸\to ⟨x,{*}_{𝑸}\left(x\right)⟩\in \left(𝑸\times 𝑸\right)$$
14		df-ov	$$⊢x{\cdot }_{𝑸}{*}_{𝑸}\left(x\right)={\cdot }_{𝑸}\left(⟨x,{*}_{𝑸}\left(x\right)⟩\right)$$
15		recidnq	$$⊢x\in 𝑸\to x{\cdot }_{𝑸}{*}_{𝑸}\left(x\right)=1_{𝑸}$$
16	14 15	syl5eqr	$$⊢x\in 𝑸\to {\cdot }_{𝑸}\left(⟨x,{*}_{𝑸}\left(x\right)⟩\right)=1_{𝑸}$$
17		ffn	$$⊢{\cdot }_{𝑸}:𝑸\times 𝑸⟶𝑸\to {\cdot }_{𝑸}Fn\left(𝑸\times 𝑸\right)$$
18		fniniseg	$$⊢{\cdot }_{𝑸}Fn\left(𝑸\times 𝑸\right)\to \left(⟨x,{*}_{𝑸}\left(x\right)⟩\in {{\cdot }_{𝑸}}^{-1}\left[\left\{1_{𝑸}\right\}\right]\leftrightarrow \left(⟨x,{*}_{𝑸}\left(x\right)⟩\in \left(𝑸\times 𝑸\right)\wedge {\cdot }_{𝑸}\left(⟨x,{*}_{𝑸}\left(x\right)⟩\right)=1_{𝑸}\right)\right)$$
19	4 17 18	mp2b	$$⊢⟨x,{*}_{𝑸}\left(x\right)⟩\in {{\cdot }_{𝑸}}^{-1}\left[\left\{1_{𝑸}\right\}\right]\leftrightarrow \left(⟨x,{*}_{𝑸}\left(x\right)⟩\in \left(𝑸\times 𝑸\right)\wedge {\cdot }_{𝑸}\left(⟨x,{*}_{𝑸}\left(x\right)⟩\right)=1_{𝑸}\right)$$
20	13 16 19	sylanbrc	$$⊢x\in 𝑸\to ⟨x,{*}_{𝑸}\left(x\right)⟩\in {{\cdot }_{𝑸}}^{-1}\left[\left\{1_{𝑸}\right\}\right]$$
21	20 1	eleqtrrdi	$$⊢x\in 𝑸\to ⟨x,{*}_{𝑸}\left(x\right)⟩\in {*}_{𝑸}$$
22		df-br	$$⊢x{*}_{𝑸}{*}_{𝑸}\left(x\right)\leftrightarrow ⟨x,{*}_{𝑸}\left(x\right)⟩\in {*}_{𝑸}$$
23	21 22	sylibr	$$⊢x\in 𝑸\to x{*}_{𝑸}{*}_{𝑸}\left(x\right)$$
24		vex	$$⊢x\in \mathrm{V}$$
25		fvex	$$⊢{*}_{𝑸}\left(x\right)\in \mathrm{V}$$
26	24 25	breldm	$$⊢x{*}_{𝑸}{*}_{𝑸}\left(x\right)\to x\in \mathrm{dom}{*}_{𝑸}$$
27	23 26	syl	$$⊢x\in 𝑸\to x\in \mathrm{dom}{*}_{𝑸}$$
28	27	ssriv	$$⊢𝑸\subseteq \mathrm{dom}{*}_{𝑸}$$
29	10 28	eqssi	$$⊢\mathrm{dom}{*}_{𝑸}=𝑸$$