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

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 } e. _V <-> ( A e/ _V \/ A = (/) \/ B e. _V ) )

Proof

Step Hyp Ref Expression
1 ioran 
 |-  ( -. ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) <-> ( -. ( A e/ _V \/ A = (/) ) /\ -. B e. _V ) )
2 df-nel 
 |-  ( B e/ _V <-> -. B e. _V )
3 ioran 
 |-  ( -. ( A e/ _V \/ A = (/) ) <-> ( -. A e/ _V /\ -. A = (/) ) )
4 nnel 
 |-  ( -. A e/ _V <-> A e. _V )
5 df-ne 
 |-  ( A =/= (/) <-> -. A = (/) )
6 5 bicomi 
 |-  ( -. A = (/) <-> A =/= (/) )
7 4 6 anbi12i 
 |-  ( ( -. A e/ _V /\ -. A = (/) ) <-> ( A e. _V /\ A =/= (/) ) )
8 3 7 bitri 
 |-  ( -. ( A e/ _V \/ A = (/) ) <-> ( A e. _V /\ A =/= (/) ) )
9 fsetprcnex 
 |-  ( ( ( A e. _V /\ A =/= (/) ) /\ B e/ _V ) -> { f | f : A --> B } e/ _V )
10 9 ex 
 |-  ( ( A e. _V /\ A =/= (/) ) -> ( B e/ _V -> { f | f : A --> B } e/ _V ) )
11 8 10 sylbi 
 |-  ( -. ( A e/ _V \/ A = (/) ) -> ( B e/ _V -> { f | f : A --> B } e/ _V ) )
12 2 11 biimtrrid 
 |-  ( -. ( A e/ _V \/ A = (/) ) -> ( -. B e. _V -> { f | f : A --> B } e/ _V ) )
13 12 imp 
 |-  ( ( -. ( A e/ _V \/ A = (/) ) /\ -. B e. _V ) -> { f | f : A --> B } e/ _V )
14 1 13 sylbi 
 |-  ( -. ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) -> { f | f : A --> B } e/ _V )
15 df-nel 
 |-  ( { f | f : A --> B } e/ _V <-> -. { f | f : A --> B } e. _V )
16 14 15 sylib 
 |-  ( -. ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) -> -. { f | f : A --> B } e. _V )
17 16 con4i 
 |-  ( { f | f : A --> B } e. _V -> ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) )
18 df-3or 
 |-  ( ( A e/ _V \/ A = (/) \/ B e. _V ) <-> ( ( A e/ _V \/ A = (/) ) \/ B e. _V ) )
19 17 18 sylibr 
 |-  ( { f | f : A --> B } e. _V -> ( A e/ _V \/ A = (/) \/ B e. _V ) )
20 fsetdmprc0 
 |-  ( A e/ _V -> { f | f Fn A } = (/) )
21 ffn 
 |-  ( f : A --> B -> f Fn A )
22 21 ss2abi 
 |-  { f | f : A --> B } C_ { f | f Fn A }
23 sseq0 
 |-  ( ( { f | f : A --> B } C_ { 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 
 |-  (/) e. _V
26 24 25 eqeltrdi 
 |-  ( { f | f Fn A } = (/) -> { f | f : A --> B } e. _V )
27 20 26 syl 
 |-  ( A e/ _V -> { f | f : A --> B } e. _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 
 |-  { (/) } e. _V
33 31 32 eqeltrdi 
 |-  ( A = (/) -> { f | f : A --> B } e. _V )
34 fsetex 
 |-  ( B e. _V -> { f | f : A --> B } e. _V )
35 27 33 34 3jaoi 
 |-  ( ( A e/ _V \/ A = (/) \/ B e. _V ) -> { f | f : A --> B } e. _V )
36 19 35 impbii 
 |-  ( { f | f : A --> B } e. _V <-> ( A e/ _V \/ A = (/) \/ B e. _V ) )