Metamath Proof Explorer

Theorem cnvexg

Description: The converse of a set is a set. Corollary 6.8(1) of TakeutiZaring p. 26. (Contributed by NM, 17-Mar-1998)

Ref Expression
Assertion cnvexg ⊢ A ∈ V → A -1 ∈ V

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ A -1
2 relssdmrn ⊢ Rel ⁡ A -1 → A -1 ⊆ dom ⁡ A -1 × ran ⁡ A -1
3 1 2 ax-mp ⊢ A -1 ⊆ dom ⁡ A -1 × ran ⁡ A -1
4 df-rn ⊢ ran ⁡ A = dom ⁡ A -1
5 rnexg ⊢ A ∈ V → ran ⁡ A ∈ V
6 4 5 eqeltrrid ⊢ A ∈ V → dom ⁡ A -1 ∈ V
7 dfdm4 ⊢ dom ⁡ A = ran ⁡ A -1
8 dmexg ⊢ A ∈ V → dom ⁡ A ∈ V
9 7 8 eqeltrrid ⊢ A ∈ V → ran ⁡ A -1 ∈ V
10 6 9 xpexd ⊢ A ∈ V → dom ⁡ A -1 × ran ⁡ A -1 ∈ V
11 ssexg ⊢ A -1 ⊆ dom ⁡ A -1 × ran ⁡ A -1 ∧ dom ⁡ A -1 × ran ⁡ A -1 ∈ V → A -1 ∈ V
12 3 10 11 sylancr ⊢ A ∈ V → A -1 ∈ V