Metamath Proof Explorer

Theorem fsetexb

Description: The class of all functions from a class A into a class B is a set iff B is a set or A is not a set or A is empty. (Contributed by AV, 15-Sep-2024)

Ref Expression
Assertion fsetexb ⊢ f | f : A ⟶ B ∈ V ↔ A ∉ V ∨ A = ∅ ∨ B ∈ V

Proof

Step Hyp Ref Expression
1 ioran ⊢ ¬ A ∉ V ∨ A = ∅ ∨ B ∈ V ↔ ¬ A ∉ V ∨ A = ∅ ∧ ¬ B ∈ V
2 df-nel ⊢ B ∉ V ↔ ¬ B ∈ V
3 ioran ⊢ ¬ A ∉ V ∨ A = ∅ ↔ ¬ A ∉ V ∧ ¬ A = ∅
4 nnel ⊢ ¬ A ∉ V ↔ A ∈ V
5 df-ne ⊢ A ≠ ∅ ↔ ¬ A = ∅
6 5 bicomi ⊢ ¬ A = ∅ ↔ A ≠ ∅
7 4 6 anbi12i ⊢ ¬ A ∉ V ∧ ¬ A = ∅ ↔ A ∈ V ∧ A ≠ ∅
8 3 7 bitri ⊢ ¬ A ∉ V ∨ A = ∅ ↔ A ∈ V ∧ A ≠ ∅
9 fsetprcnex ⊢ A ∈ V ∧ A ≠ ∅ ∧ B ∉ V → f | f : A ⟶ B ∉ V
10 9 ex ⊢ A ∈ V ∧ A ≠ ∅ → B ∉ V → f | f : A ⟶ B ∉ V
11 8 10 sylbi ⊢ ¬ A ∉ V ∨ A = ∅ → B ∉ V → f | f : A ⟶ B ∉ V
12 2 11 biimtrrid ⊢ ¬ A ∉ V ∨ A = ∅ → ¬ B ∈ V → f | f : A ⟶ B ∉ V
13 12 imp ⊢ ¬ A ∉ V ∨ A = ∅ ∧ ¬ B ∈ V → f | f : A ⟶ B ∉ V
14 1 13 sylbi ⊢ ¬ A ∉ V ∨ A = ∅ ∨ B ∈ V → f | f : A ⟶ B ∉ V
15 df-nel ⊢ f | f : A ⟶ B ∉ V ↔ ¬ f | f : A ⟶ B ∈ V
16 14 15 sylib ⊢ ¬ A ∉ V ∨ A = ∅ ∨ B ∈ V → ¬ f | f : A ⟶ B ∈ V
17 16 con4i ⊢ f | f : A ⟶ B ∈ V → A ∉ V ∨ A = ∅ ∨ B ∈ V
18 df-3or ⊢ A ∉ V ∨ A = ∅ ∨ B ∈ V ↔ A ∉ V ∨ A = ∅ ∨ B ∈ V
19 17 18 sylibr ⊢ f | f : A ⟶ B ∈ V → A ∉ V ∨ A = ∅ ∨ B ∈ V
20 fsetdmprc0 ⊢ A ∉ V → f | f Fn A = ∅
21 ffn ⊢ f : A ⟶ B → f Fn A
22 21 ss2abi ⊢ f | f : A ⟶ B ⊆ f | f Fn A
23 sseq0 ⊢ f | f : A ⟶ B ⊆ f | f Fn A ∧ f | f Fn A = ∅ → f | f : A ⟶ B = ∅
24 22 23 mpan ⊢ f | f Fn A = ∅ → f | f : A ⟶ B = ∅
25 0ex ⊢ ∅ ∈ V
26 24 25 eqeltrdi ⊢ f | f Fn A = ∅ → f | f : A ⟶ B ∈ V
27 20 26 syl ⊢ A ∉ V → f | f : A ⟶ B ∈ V
28 feq2 ⊢ A = ∅ → f : A ⟶ B ↔ f : ∅ ⟶ B
29 28 abbidv ⊢ A = ∅ → f | f : A ⟶ B = f | f : ∅ ⟶ B
30 fset0 ⊢ f | f : ∅ ⟶ B = ∅
31 29 30 eqtrdi ⊢ A = ∅ → f | f : A ⟶ B = ∅
32 p0ex ⊢ ∅ ∈ V
33 31 32 eqeltrdi ⊢ A = ∅ → f | f : A ⟶ B ∈ V
34 fsetex ⊢ B ∈ V → f | f : A ⟶ B ∈ V
35 27 33 34 3jaoi ⊢ A ∉ V ∨ A = ∅ ∨ B ∈ V → f | f : A ⟶ B ∈ V
36 19 35 impbii ⊢ f | f : A ⟶ B ∈ V ↔ A ∉ V ∨ A = ∅ ∨ B ∈ V