Theorem nqerid

Description: Corollary of nqereu : the function /Q acts as the identity on members of Q. . (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	nqerid	⊢ ( 𝐴 ∈ Q → ( [Q] ‘ 𝐴 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nqerf	⊢ [Q] : ( N × N ) ⟶ Q
2		ffun	⊢ ( [Q] : ( N × N ) ⟶ Q → Fun [Q] )
3	1 2	ax-mp	⊢ Fun [Q]
4		elpqn	⊢ ( 𝐴 ∈ Q → 𝐴 ∈ ( N × N ) )
5		id	⊢ ( 𝐴 ∈ Q → 𝐴 ∈ Q )
6		enqer	⊢ ~Q Er ( N × N )
7	6	a1i	⊢ ( 𝐴 ∈ Q → ~Q Er ( N × N ) )
8	7 4	erref	⊢ ( 𝐴 ∈ Q → 𝐴 ~Q 𝐴 )
9		df-erq	⊢ [Q] = ( ~Q ∩ ( ( N × N ) × Q ) )
10	9	breqi	⊢ ( 𝐴 [Q] 𝐴 ↔ 𝐴 ( ~Q ∩ ( ( N × N ) × Q ) ) 𝐴 )
11		brinxp2	⊢ ( 𝐴 ( ~Q ∩ ( ( N × N ) × Q ) ) 𝐴 ↔ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐴 ∈ Q ) ∧ 𝐴 ~Q 𝐴 ) )
12	10 11	bitri	⊢ ( 𝐴 [Q] 𝐴 ↔ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐴 ∈ Q ) ∧ 𝐴 ~Q 𝐴 ) )
13	4 5 8 12	syl21anbrc	⊢ ( 𝐴 ∈ Q → 𝐴 [Q] 𝐴 )
14		funbrfv	⊢ ( Fun [Q] → ( 𝐴 [Q] 𝐴 → ( [Q] ‘ 𝐴 ) = 𝐴 ) )
15	3 13 14	mpsyl	⊢ ( 𝐴 ∈ Q → ( [Q] ‘ 𝐴 ) = 𝐴 )