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|fFnA=∅
21 ffn ⊢f:A⟶B→fFnA
22 21 ss2abi ⊢f|f:A⟶B⊆f|fFnA
23 sseq0 ⊢f|f:A⟶B⊆f|fFnA∧f|fFnA=∅→f|f:A⟶B=∅
24 22 23 mpan ⊢f|fFnA=∅→f|f:A⟶B=∅
25 0ex ⊢∅∈V
26 24 25 eqeltrdi ⊢f|fFnA=∅→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