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)

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

Proof

Step	Hyp	Ref	Expression
1		f1oabexg.1	⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) }
2		f1of	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
3	2	anim1i	⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) → ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) )
4	3	ss2abi	⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) } ⊆ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
5		eqid	⊢ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } = { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
6	5	fabexg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } ∈ V )
7		ssexg	⊢ ( ( { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) } ⊆ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } ∧ { 𝑓 ∣ ( 𝑓 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } ∈ V ) → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) } ∈ V )
8	4 6 7	sylancr	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) } ∈ V )
9	1 8	eqeltrid	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V )