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

Metamath Proof Explorer

Theorem f1oexrnex

Description: If the range of a 1-1 onto function is a set, the function itself is a set. (Contributed by AV, 2-Jun-2019)

Ref Expression
Assertion f1oexrnex ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐹 ∈ V )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
2 f1ocnv ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 )
3 f1of ⊢ ( ◡ 𝐹 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
4 1 2 3 3syl ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ◡ 𝐹 : 𝐵 ⟶ 𝐴 )
5 fex ⊢ ( ( ◡ 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ◡ 𝐹 ∈ V )
6 4 5 sylancom ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ◡ 𝐹 ∈ V )
7 f1orel ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝐹 )
8 7 adantr ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → Rel 𝐹 )
9 relcnvexb ⊢ ( Rel 𝐹 → ( 𝐹 ∈ V ↔ ◡ 𝐹 ∈ V ) )
10 8 9 syl ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐹 ∈ V ↔ ◡ 𝐹 ∈ V ) )
11 6 10 mpbird ⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐹 ∈ V )