Description: Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-oppg | ⊢ oppg = ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g ‘ 𝑤 ) ⟩ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | coppg | ⊢ oppg | |
| 1 | vw | ⊢ 𝑤 | |
| 2 | cvv | ⊢ V | |
| 3 | 1 | cv | ⊢ 𝑤 |
| 4 | csts | ⊢ sSet | |
| 5 | cplusg | ⊢ +g | |
| 6 | cnx | ⊢ ndx | |
| 7 | 6 5 | cfv | ⊢ ( +g ‘ ndx ) |
| 8 | 3 5 | cfv | ⊢ ( +g ‘ 𝑤 ) |
| 9 | 8 | ctpos | ⊢ tpos ( +g ‘ 𝑤 ) |
| 10 | 7 9 | cop | ⊢ ⟨ ( +g ‘ ndx ) , tpos ( +g ‘ 𝑤 ) ⟩ |
| 11 | 3 10 4 | co | ⊢ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g ‘ 𝑤 ) ⟩ ) |
| 12 | 1 2 11 | cmpt | ⊢ ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g ‘ 𝑤 ) ⟩ ) ) |
| 13 | 0 12 | wceq | ⊢ oppg = ( 𝑤 ∈ V ↦ ( 𝑤 sSet ⟨ ( +g ‘ ndx ) , tpos ( +g ‘ 𝑤 ) ⟩ ) ) |