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	⊢ ( 𝐴 ∈ ( N × N ) → 𝐴 ~_Q ( [Q] ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐴 )
2		nqerf	⊢ [Q] : ( N × N ) ⟶ Q
3		ffn	⊢ ( [Q] : ( N × N ) ⟶ Q → [Q] Fn ( N × N ) )
4	2 3	ax-mp	⊢ [Q] Fn ( N × N )
5		fnbrfvb	⊢ ( ( [Q] Fn ( N × N ) ∧ 𝐴 ∈ ( N × N ) ) → ( ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐴 ) ↔ 𝐴 [Q] ( [Q] ‘ 𝐴 ) ) )
6	4 5	mpan	⊢ ( 𝐴 ∈ ( N × N ) → ( ( [Q] ‘ 𝐴 ) = ( [Q] ‘ 𝐴 ) ↔ 𝐴 [Q] ( [Q] ‘ 𝐴 ) ) )
7	1 6	mpbii	⊢ ( 𝐴 ∈ ( N × N ) → 𝐴 [Q] ( [Q] ‘ 𝐴 ) )
8		df-erq	⊢ [Q] = ( ~_Q ∩ ( ( N × N ) × Q ) )
9		inss1	⊢ ( ~_Q ∩ ( ( N × N ) × Q ) ) ⊆ ~_Q
10	8 9	eqsstri	⊢ [Q] ⊆ ~_Q
11	10	ssbri	⊢ ( 𝐴 [Q] ( [Q] ‘ 𝐴 ) → 𝐴 ~_Q ( [Q] ‘ 𝐴 ) )
12	7 11	syl	⊢ ( 𝐴 ∈ ( N × N ) → 𝐴 ~_Q ( [Q] ‘ 𝐴 ) )