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

Metamath Proof Explorer

Theorem fncnvimaeqv

Description: The inverse images of the universal class _V under functions on the universal class _V are the universal class _V itself. (Proposed by Mario Carneiro, 7-Mar-2020.) (Contributed by AV, 7-Mar-2020)

Ref Expression
Assertion fncnvimaeqv ( 𝐹 Fn V → ( ◡ 𝐹 “ V ) = V )

Proof

Step Hyp Ref Expression
1 fncnvima2 ⊢ ( 𝐹 Fn V → ( ◡ 𝐹 “ V ) = { 𝑦 ∈ V ∣ ( 𝐹 ‘ 𝑦 ) ∈ V } )
2 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
3 2 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ∈ V ↔ ( 𝐹 ‘ 𝑥 ) ∈ V ) )
4 3 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ V ∣ ( 𝐹 ‘ 𝑦 ) ∈ V } ↔ ( 𝑥 ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ∈ V ) )
5 fvexd ⊢ ( 𝐹 Fn V → ( 𝐹 ‘ 𝑥 ) ∈ V )
6 5 biantrud ⊢ ( 𝐹 Fn V → ( 𝑥 ∈ V ↔ ( 𝑥 ∈ V ∧ ( 𝐹 ‘ 𝑥 ) ∈ V ) ) )
7 4 6 bitr4id ⊢ ( 𝐹 Fn V → ( 𝑥 ∈ { 𝑦 ∈ V ∣ ( 𝐹 ‘ 𝑦 ) ∈ V } ↔ 𝑥 ∈ V ) )
8 7 eqrdv ⊢ ( 𝐹 Fn V → { 𝑦 ∈ V ∣ ( 𝐹 ‘ 𝑦 ) ∈ V } = V )
9 1 8 eqtrd ⊢ ( 𝐹 Fn V → ( ◡ 𝐹 “ V ) = V )