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
|
syl5bir |
|- ( -. ( 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 ) ) |