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 ⊢ A ∈ 𝑸 → / 𝑸 ⁡ A = A

Proof

Step Hyp Ref Expression
1 nqerf ⊢ / 𝑸 : 𝑵 × 𝑵 ⟶ 𝑸
2 ffun ⊢ / 𝑸 : 𝑵 × 𝑵 ⟶ 𝑸 → Fun ⁡ / 𝑸
3 1 2 ax-mp ⊢ Fun ⁡ / 𝑸
4 elpqn ⊢ A ∈ 𝑸 → A ∈ 𝑵 × 𝑵
5 id ⊢ A ∈ 𝑸 → A ∈ 𝑸
6 enqer ⊢ ~ 𝑸 Er 𝑵 × 𝑵
7 6 a1i ⊢ A ∈ 𝑸 → ~ 𝑸 Er 𝑵 × 𝑵
8 7 4 erref ⊢ A ∈ 𝑸 → A ~ 𝑸 A
9 df-erq ⊢ / 𝑸 = ~ 𝑸 ∩ 𝑵 × 𝑵 × 𝑸
10 9 breqi ⊢ A / 𝑸 A ↔ A ~ 𝑸 ∩ 𝑵 × 𝑵 × 𝑸 A
11 brinxp2 ⊢ A ~ 𝑸 ∩ 𝑵 × 𝑵 × 𝑸 A ↔ A ∈ 𝑵 × 𝑵 ∧ A ∈ 𝑸 ∧ A ~ 𝑸 A
12 10 11 bitri ⊢ A / 𝑸 A ↔ A ∈ 𝑵 × 𝑵 ∧ A ∈ 𝑸 ∧ A ~ 𝑸 A
13 4 5 8 12 syl21anbrc ⊢ A ∈ 𝑸 → A / 𝑸 A
14 funbrfv ⊢ Fun ⁡ / 𝑸 → A / 𝑸 A → / 𝑸 ⁡ A = A
15 3 13 14 mpsyl ⊢ A ∈ 𝑸 → / 𝑸 ⁡ A = A