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 syl5bir ¬ 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