This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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] ‘ 𝐴 ) = 𝐴 )