Metamath Proof Explorer

Definition df-risc

Description: Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion df-risc 
|- ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 crisc 
 |-  ~=R
1 vr 
 |-  r
2 vs 
 |-  s
3 1 cv 
 |-  r
4 crngo 
 |-  RingOps
5 3 4 wcel 
 |-  r e. RingOps
6 2 cv 
 |-  s
7 6 4 wcel 
 |-  s e. RingOps
8 5 7 wa 
 |-  ( r e. RingOps /\ s e. RingOps )
9 vf 
 |-  f
10 9 cv 
 |-  f
11 crngoiso 
 |-  RingOpsIso
12 3 6 11 co 
 |-  ( r RingOpsIso s )
13 10 12 wcel 
 |-  f e. ( r RingOpsIso s )
14 13 9 wex 
 |-  E. f f e. ( r RingOpsIso s )
15 8 14 wa 
 |-  ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) )
16 15 1 2 copab 
 |-  { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) }
17 0 16 wceq 
 |-  ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) }