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

Metamath Proof Explorer

Theorem nqerrel

Description: Any member of ( N. X. N. ) relates to the representative of its equivalence class. (Contributed by Mario Carneiro, 6-May-2013) (New usage is discouraged.)

Ref Expression
Assertion nqerrel ⊢ A ∈ 𝑵 × 𝑵 → A ~ 𝑸 / 𝑸 ⁡ A

Proof

Step Hyp Ref Expression
1 eqid ⊢ / 𝑸 ⁡ A = / 𝑸 ⁡ A
2 nqerf ⊢ / 𝑸 : 𝑵 × 𝑵 ⟶ 𝑸
3 ffn ⊢ / 𝑸 : 𝑵 × 𝑵 ⟶ 𝑸 → / 𝑸 Fn 𝑵 × 𝑵
4 2 3 ax-mp ⊢ / 𝑸 Fn 𝑵 × 𝑵
5 fnbrfvb ⊢ / 𝑸 Fn 𝑵 × 𝑵 ∧ A ∈ 𝑵 × 𝑵 → / 𝑸 ⁡ A = / 𝑸 ⁡ A ↔ A / 𝑸 / 𝑸 ⁡ A
6 4 5 mpan ⊢ A ∈ 𝑵 × 𝑵 → / 𝑸 ⁡ A = / 𝑸 ⁡ A ↔ A / 𝑸 / 𝑸 ⁡ A
7 1 6 mpbii ⊢ A ∈ 𝑵 × 𝑵 → A / 𝑸 / 𝑸 ⁡ A
8 df-erq ⊢ / 𝑸 = ~ 𝑸 ∩ 𝑵 × 𝑵 × 𝑸
9 inss1 ⊢ ~ 𝑸 ∩ 𝑵 × 𝑵 × 𝑸 ⊆ ~ 𝑸
10 8 9 eqsstri ⊢ / 𝑸 ⊆ ~ 𝑸
11 10 ssbri ⊢ A / 𝑸 / 𝑸 ⁡ A → A ~ 𝑸 / 𝑸 ⁡ A
12 7 11 syl ⊢ A ∈ 𝑵 × 𝑵 → A ~ 𝑸 / 𝑸 ⁡ A