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

Metamath Proof Explorer

Theorem tposexg

Description: The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion tposexg ( 𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V )

Proof

Step Hyp Ref Expression
1 tposssxp ⊢ tpos 𝐹 ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 )
2 dmexg ⊢ ( 𝐹 ∈ 𝑉 → dom 𝐹 ∈ V )
3 cnvexg ⊢ ( dom 𝐹 ∈ V → ◡ dom 𝐹 ∈ V )
4 2 3 syl ⊢ ( 𝐹 ∈ 𝑉 → ◡ dom 𝐹 ∈ V )
5 p0ex ⊢ { ∅ } ∈ V
6 unexg ⊢ ( ( ◡ dom 𝐹 ∈ V ∧ { ∅ } ∈ V ) → ( ◡ dom 𝐹 ∪ { ∅ } ) ∈ V )
7 4 5 6 sylancl ⊢ ( 𝐹 ∈ 𝑉 → ( ◡ dom 𝐹 ∪ { ∅ } ) ∈ V )
8 rnexg ⊢ ( 𝐹 ∈ 𝑉 → ran 𝐹 ∈ V )
9 7 8 xpexd ⊢ ( 𝐹 ∈ 𝑉 → ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) ∈ V )
10 ssexg ⊢ ( ( tpos 𝐹 ⊆ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) ∧ ( ( ◡ dom 𝐹 ∪ { ∅ } ) × ran 𝐹 ) ∈ V ) → tpos 𝐹 ∈ V )
11 1 9 10 sylancr ⊢ ( 𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V )