enqer

Description: The equivalence relation for positive fractions is an equivalence relation. Proposition 9-2.1 of Gleason p. 117. (Contributed by NM, 27-Aug-1995) (Revised by Mario Carneiro, 6-Jul-2015) (New usage is discouraged.)

		Ref	Expression
	Assertion	enqer	$⊢ ~_{𝑸} Er (𝑵 \times 𝑵)$

Proof

Step	Hyp	Ref	Expression
1		df-enq	$⊢ ~_{𝑸} = \{⟨x, y⟩ \| ((x \in (𝑵 \times 𝑵) \land y \in (𝑵 \times 𝑵)) \land \exists z \exists w \exists v \exists u ((x = ⟨z, w⟩ \land y = ⟨v, u⟩) \land z \cdot_{𝑵} u = w \cdot_{𝑵} v))\}$
2		mulcompi	$⊢ x \cdot_{𝑵} y = y \cdot_{𝑵} x$
3		mulclpi	$⊢ (x \in 𝑵 \land y \in 𝑵) \to x \cdot_{𝑵} y \in 𝑵$
4		mulasspi	$⊢ (x \cdot_{𝑵} y) \cdot_{𝑵} z = x \cdot_{𝑵} (y \cdot_{𝑵} z)$
5		mulcanpi	$⊢ (x \in 𝑵 \land y \in 𝑵) \to (x \cdot_{𝑵} y = x \cdot_{𝑵} z \leftrightarrow y = z)$
6	5	biimpd	$⊢ (x \in 𝑵 \land y \in 𝑵) \to (x \cdot_{𝑵} y = x \cdot_{𝑵} z \to y = z)$
7	1 2 3 4 6	ecopover	$⊢ ~_{𝑸} Er (𝑵 \times 𝑵)$

Metamath Proof Explorer

Theorem enqer

Proof