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 )