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

Metamath Proof Explorer

Theorem f1oabexg

Description: The class of all 1-1-onto functions mapping one set to another is a set. (Contributed by Paul Chapman, 25-Feb-2008) (Proof shortened by AV, 9-Jun-2025)

Ref Expression
Hypothesis f1oabexg.1 ⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) }
Assertion f1oabexg ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V )

Proof

Step Hyp Ref Expression
1 f1oabexg.1 ⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) }
2 elex ⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V )
3 elex ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V )
4 f1of ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
5 4 ad2antrl ⊢ ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) ) → 𝑓 : 𝐴 ⟶ 𝐵 )
6 simpl ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐴 ∈ V )
7 simpr ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐵 ∈ V )
8 5 6 7 fabexd ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) } ∈ V )
9 1 8 eqeltrid ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝐹 ∈ V )
10 2 3 9 syl2an ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V )