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 | |- ~Q Er ( N. X. N. ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-enq | |- ~Q = { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z .N u ) = ( w .N v ) ) ) } |
|
| 2 | mulcompi | |- ( x .N y ) = ( y .N x ) |
|
| 3 | mulclpi | |- ( ( x e. N. /\ y e. N. ) -> ( x .N y ) e. N. ) |
|
| 4 | mulasspi | |- ( ( x .N y ) .N z ) = ( x .N ( y .N z ) ) |
|
| 5 | mulcanpi | |- ( ( x e. N. /\ y e. N. ) -> ( ( x .N y ) = ( x .N z ) <-> y = z ) ) |
|
| 6 | 5 | biimpd | |- ( ( x e. N. /\ y e. N. ) -> ( ( x .N y ) = ( x .N z ) -> y = z ) ) |
| 7 | 1 2 3 4 6 | ecopover | |- ~Q Er ( N. X. N. ) |