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	⊢ dom *Q = Q

Proof

Step	Hyp	Ref	Expression
1		df-rq	⊢ *Q = ( ◡ ·Q “ { 1Q } )
2		cnvimass	⊢ ( ◡ ·Q “ { 1Q } ) ⊆ dom ·Q
3	1 2	eqsstri	⊢ *Q ⊆ dom ·Q
4		mulnqf	⊢ ·Q : ( Q × Q ) ⟶ Q
5	4	fdmi	⊢ dom ·Q = ( Q × Q )
6	3 5	sseqtri	⊢ *Q ⊆ ( Q × Q )
7		dmss	⊢ ( *Q ⊆ ( Q × Q ) → dom *Q ⊆ dom ( Q × Q ) )
8	6 7	ax-mp	⊢ dom *Q ⊆ dom ( Q × Q )
9		dmxpid	⊢ dom ( Q × Q ) = Q
10	8 9	sseqtri	⊢ dom *Q ⊆ Q
11		recclnq	⊢ ( 𝑥 ∈ Q → ( *Q ‘ 𝑥 ) ∈ Q )
12		opelxpi	⊢ ( ( 𝑥 ∈ Q ∧ ( *Q ‘ 𝑥 ) ∈ Q ) → ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ ( Q × Q ) )
13	11 12	mpdan	⊢ ( 𝑥 ∈ Q → ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ ( Q × Q ) )
14		df-ov	⊢ ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) = ( ·Q ‘ ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ )
15		recidnq	⊢ ( 𝑥 ∈ Q → ( 𝑥 ·Q ( *Q ‘ 𝑥 ) ) = 1Q )
16	14 15	eqtr3id	⊢ ( 𝑥 ∈ Q → ( ·Q ‘ ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ) = 1Q )
17		ffn	⊢ ( ·Q : ( Q × Q ) ⟶ Q → ·Q Fn ( Q × Q ) )
18		fniniseg	⊢ ( ·Q Fn ( Q × Q ) → ( ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ ( ◡ ·Q “ { 1Q } ) ↔ ( ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ ( Q × Q ) ∧ ( ·Q ‘ ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ) = 1Q ) ) )
19	4 17 18	mp2b	⊢ ( ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ ( ◡ ·Q “ { 1Q } ) ↔ ( ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ ( Q × Q ) ∧ ( ·Q ‘ ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ) = 1Q ) )
20	13 16 19	sylanbrc	⊢ ( 𝑥 ∈ Q → ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ ( ◡ ·Q “ { 1Q } ) )
21	20 1	eleqtrrdi	⊢ ( 𝑥 ∈ Q → ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ *Q )
22		df-br	⊢ ( 𝑥 *Q ( *Q ‘ 𝑥 ) ↔ ⟨ 𝑥 , ( *Q ‘ 𝑥 ) ⟩ ∈ *Q )
23	21 22	sylibr	⊢ ( 𝑥 ∈ Q → 𝑥 *Q ( *Q ‘ 𝑥 ) )
24		vex	⊢ 𝑥 ∈ V
25		fvex	⊢ ( *Q ‘ 𝑥 ) ∈ V
26	24 25	breldm	⊢ ( 𝑥 *Q ( *Q ‘ 𝑥 ) → 𝑥 ∈ dom *Q )
27	23 26	syl	⊢ ( 𝑥 ∈ Q → 𝑥 ∈ dom *Q )
28	27	ssriv	⊢ Q ⊆ dom *Q
29	10 28	eqssi	⊢ dom *Q = Q