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 “ { 1_Q } )
2		cnvimass	⊢ ( ^◡ ·_Q “ { 1_Q } ) ⊆ 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 ‘ 𝑥 ) ) = 1_Q )
16	14 15	eqtr3id	⊢ ( 𝑥 ∈ Q → ( ·_Q ‘ ⟨ 𝑥 , ( *_Q ‘ 𝑥 ) ⟩ ) = 1_Q )
17		ffn	⊢ ( ·_Q : ( Q × Q ) ⟶ Q → ·_Q Fn ( Q × Q ) )
18		fniniseg	⊢ ( ·_Q Fn ( Q × Q ) → ( ⟨ 𝑥 , ( _Q ‘ 𝑥 ) ⟩ ∈ ( ^◡ ·_Q “ { 1_Q } ) ↔ ( ⟨ 𝑥 , ( _Q ‘ 𝑥 ) ⟩ ∈ ( Q × Q ) ∧ ( ·_Q ‘ ⟨ 𝑥 , ( *_Q ‘ 𝑥 ) ⟩ ) = 1_Q ) ) )
19	4 17 18	mp2b	⊢ ( ⟨ 𝑥 , ( _Q ‘ 𝑥 ) ⟩ ∈ ( ^◡ ·_Q “ { 1_Q } ) ↔ ( ⟨ 𝑥 , ( _Q ‘ 𝑥 ) ⟩ ∈ ( Q × Q ) ∧ ( ·_Q ‘ ⟨ 𝑥 , ( *_Q ‘ 𝑥 ) ⟩ ) = 1_Q ) )
20	13 16 19	sylanbrc	⊢ ( 𝑥 ∈ Q → ⟨ 𝑥 , ( *_Q ‘ 𝑥 ) ⟩ ∈ ( ^◡ ·_Q “ { 1_Q } ) )
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

Metamath Proof Explorer

Theorem dmrecnq

Proof