This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ 𝑉 → ◡ 𝐴 ∈ V )

Proof

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