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 \in 𝑸 \to /_{𝑸} (A) = A$

Proof

Step	Hyp	Ref	Expression
1		nqerf	$⊢ /_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸$
2		ffun	$⊢ /_{𝑸} : 𝑵 \times 𝑵 ⟶ 𝑸 \to Fun /_{𝑸}$
3	1 2	ax-mp	$⊢ Fun /_{𝑸}$
4		elpqn	$⊢ A \in 𝑸 \to A \in (𝑵 \times 𝑵)$
5		id	$⊢ A \in 𝑸 \to A \in 𝑸$
6		enqer	$⊢ ~_{𝑸} Er (𝑵 \times 𝑵)$
7	6	a1i	$⊢ A \in 𝑸 \to ~_{𝑸} Er (𝑵 \times 𝑵)$
8	7 4	erref	$⊢ A \in 𝑸 \to A ~_{𝑸} A$
9		df-erq	$⊢ /_{𝑸} = ~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)$
10	9	breqi	$⊢ A /_{𝑸} A \leftrightarrow A (~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)) A$
11		brinxp2	$⊢ A (~_{𝑸} \cap ((𝑵 \times 𝑵) \times 𝑸)) A \leftrightarrow ((A \in (𝑵 \times 𝑵) \land A \in 𝑸) \land A ~_{𝑸} A)$
12	10 11	bitri	$⊢ A /_{𝑸} A \leftrightarrow ((A \in (𝑵 \times 𝑵) \land A \in 𝑸) \land A ~_{𝑸} A)$
13	4 5 8 12	syl21anbrc	$⊢ A \in 𝑸 \to A /_{𝑸} A$
14		funbrfv	$⊢ Fun /_{𝑸} \to (A /_{𝑸} A \to /_{𝑸} (A) = A)$
15	3 13 14	mpsyl	$⊢ A \in 𝑸 \to /_{𝑸} (A) = A$