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

Metamath Proof Explorer

Theorem f1oabexgOLD

Description: Obsolete version of f1oabexg as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis f1oabexg.1 ⊢ 𝐹 = { 𝑓 ∣ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝜑 ) }
Assertion f1oabexgOLD ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ 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 )