This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union The mapping operation f1osetex
Description: The set of bijections between two classes exists. (Contributed by AV , 30-Mar-2024) (Revised by AV , 8-Aug-2024) (Proof shortened by SN , 22-Aug-2024)
Ref
Expression
Assertion
f1osetex ⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1 -onto → 𝐵 } ∈ V
Proof
Step
Hyp
Ref
Expression
1
fosetex ⊢ { 𝑓 ∣ 𝑓 : 𝐴 –onto → 𝐵 } ∈ V
2
f1ofo ⊢ ( 𝑓 : 𝐴 –1-1 -onto → 𝐵 → 𝑓 : 𝐴 –onto → 𝐵 )
3
2
ss2abi ⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1 -onto → 𝐵 } ⊆ { 𝑓 ∣ 𝑓 : 𝐴 –onto → 𝐵 }
4
1 3
ssexi ⊢ { 𝑓 ∣ 𝑓 : 𝐴 –1-1 -onto → 𝐵 } ∈ V