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

Metamath Proof Explorer

Theorem fsetprcnex

Description: The class of all functions from a nonempty set A into a proper class B is not a set. If one of the preconditions is not fufilled, then { f | f : A --> B } is a set, see fsetdmprc0 for A e/V , fset0 for A = (/) , and fsetex for B e. V , see also fsetexb . (Contributed by AV, 14-Sep-2024) (Proof shortened by BJ, 15-Sep-2024)

Ref Expression
Assertion fsetprcnex ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )

Proof

Step Hyp Ref Expression
1 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑎 𝑎 ∈ 𝐴 )
2 feq1 ⊢ ( 𝑓 = 𝑚 → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑚 : 𝐴 ⟶ 𝐵 ) )
3 2 cbvabv ⊢ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = { 𝑚 ∣ 𝑚 : 𝐴 ⟶ 𝐵 }
4 fveq1 ⊢ ( 𝑔 = 𝑛 → ( 𝑔 ‘ 𝑎 ) = ( 𝑛 ‘ 𝑎 ) )
5 4 cbvmptv ⊢ ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↦ ( 𝑔 ‘ 𝑎 ) ) = ( 𝑛 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↦ ( 𝑛 ‘ 𝑎 ) )
6 3 5 fsetfocdm ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) → ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↦ ( 𝑔 ‘ 𝑎 ) ) : { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } –onto→ 𝐵 )
7 focdmex ⊢ ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V → ( ( 𝑔 ∈ { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ↦ ( 𝑔 ‘ 𝑎 ) ) : { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } –onto→ 𝐵 → 𝐵 ∈ V ) )
8 6 7 syl5com ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) → ( { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V → 𝐵 ∈ V ) )
9 8 nelcon3d ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) )
10 9 expcom ⊢ ( 𝑎 ∈ 𝐴 → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) ) )
11 10 exlimiv ⊢ ( ∃ 𝑎 𝑎 ∈ 𝐴 → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) ) )
12 1 11 sylbi ⊢ ( 𝐴 ≠ ∅ → ( 𝐴 ∈ 𝑉 → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) ) )
13 12 impcom ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) → ( 𝐵 ∉ V → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V ) )
14 13 imp ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐴 ≠ ∅ ) ∧ 𝐵 ∉ V ) → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∉ V )