Step |
Hyp |
Ref |
Expression |
1 |
|
setsn0fun.s |
|- ( ph -> S Struct X ) |
2 |
|
setsn0fun.i |
|- ( ph -> I e. U ) |
3 |
|
setsn0fun.e |
|- ( ph -> E e. W ) |
4 |
|
structn0fun |
|- ( S Struct X -> Fun ( S \ { (/) } ) ) |
5 |
|
structex |
|- ( S Struct X -> S e. _V ) |
6 |
|
setsfun0 |
|- ( ( ( S e. _V /\ Fun ( S \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) ) |
7 |
5 6
|
sylanl1 |
|- ( ( ( S Struct X /\ Fun ( S \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) ) |
8 |
7
|
expcom |
|- ( ( I e. U /\ E e. W ) -> ( ( S Struct X /\ Fun ( S \ { (/) } ) ) -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) ) ) |
9 |
2 3 8
|
syl2anc |
|- ( ph -> ( ( S Struct X /\ Fun ( S \ { (/) } ) ) -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) ) ) |
10 |
9
|
com12 |
|- ( ( S Struct X /\ Fun ( S \ { (/) } ) ) -> ( ph -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) ) ) |
11 |
4 10
|
mpdan |
|- ( S Struct X -> ( ph -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) ) ) |
12 |
1 11
|
mpcom |
|- ( ph -> Fun ( ( S sSet <. I , E >. ) \ { (/) } ) ) |