Step |
Hyp |
Ref |
Expression |
1 |
|
funres |
|- ( Fun ( G \ { (/) } ) -> Fun ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) ) |
2 |
1
|
adantl |
|- ( ( G e. V /\ Fun ( G \ { (/) } ) ) -> Fun ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) ) |
3 |
2
|
adantr |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) ) |
4 |
|
funsng |
|- ( ( I e. U /\ E e. W ) -> Fun { <. I , E >. } ) |
5 |
4
|
adantl |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun { <. I , E >. } ) |
6 |
|
dmres |
|- dom ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) = ( ( _V \ dom { <. I , E >. } ) i^i dom ( G \ { (/) } ) ) |
7 |
6
|
ineq1i |
|- ( dom ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) i^i dom { <. I , E >. } ) = ( ( ( _V \ dom { <. I , E >. } ) i^i dom ( G \ { (/) } ) ) i^i dom { <. I , E >. } ) |
8 |
|
in32 |
|- ( ( ( _V \ dom { <. I , E >. } ) i^i dom ( G \ { (/) } ) ) i^i dom { <. I , E >. } ) = ( ( ( _V \ dom { <. I , E >. } ) i^i dom { <. I , E >. } ) i^i dom ( G \ { (/) } ) ) |
9 |
|
incom |
|- ( ( _V \ dom { <. I , E >. } ) i^i dom { <. I , E >. } ) = ( dom { <. I , E >. } i^i ( _V \ dom { <. I , E >. } ) ) |
10 |
|
disjdif |
|- ( dom { <. I , E >. } i^i ( _V \ dom { <. I , E >. } ) ) = (/) |
11 |
9 10
|
eqtri |
|- ( ( _V \ dom { <. I , E >. } ) i^i dom { <. I , E >. } ) = (/) |
12 |
11
|
ineq1i |
|- ( ( ( _V \ dom { <. I , E >. } ) i^i dom { <. I , E >. } ) i^i dom ( G \ { (/) } ) ) = ( (/) i^i dom ( G \ { (/) } ) ) |
13 |
|
0in |
|- ( (/) i^i dom ( G \ { (/) } ) ) = (/) |
14 |
8 12 13
|
3eqtri |
|- ( ( ( _V \ dom { <. I , E >. } ) i^i dom ( G \ { (/) } ) ) i^i dom { <. I , E >. } ) = (/) |
15 |
7 14
|
eqtri |
|- ( dom ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) i^i dom { <. I , E >. } ) = (/) |
16 |
15
|
a1i |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> ( dom ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) i^i dom { <. I , E >. } ) = (/) ) |
17 |
|
funun |
|- ( ( ( Fun ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) /\ Fun { <. I , E >. } ) /\ ( dom ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) i^i dom { <. I , E >. } ) = (/) ) -> Fun ( ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) |
18 |
3 5 16 17
|
syl21anc |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) |
19 |
|
difundir |
|- ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) \ { (/) } ) = ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) \ { (/) } ) u. ( { <. I , E >. } \ { (/) } ) ) |
20 |
|
resdifcom |
|- ( ( G |` ( _V \ dom { <. I , E >. } ) ) \ { (/) } ) = ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) |
21 |
20
|
a1i |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> ( ( G |` ( _V \ dom { <. I , E >. } ) ) \ { (/) } ) = ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) ) |
22 |
|
elex |
|- ( I e. U -> I e. _V ) |
23 |
|
elex |
|- ( E e. W -> E e. _V ) |
24 |
22 23
|
anim12i |
|- ( ( I e. U /\ E e. W ) -> ( I e. _V /\ E e. _V ) ) |
25 |
|
opnz |
|- ( <. I , E >. =/= (/) <-> ( I e. _V /\ E e. _V ) ) |
26 |
24 25
|
sylibr |
|- ( ( I e. U /\ E e. W ) -> <. I , E >. =/= (/) ) |
27 |
26
|
adantl |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> <. I , E >. =/= (/) ) |
28 |
|
disjsn2 |
|- ( <. I , E >. =/= (/) -> ( { <. I , E >. } i^i { (/) } ) = (/) ) |
29 |
|
disjdif2 |
|- ( ( { <. I , E >. } i^i { (/) } ) = (/) -> ( { <. I , E >. } \ { (/) } ) = { <. I , E >. } ) |
30 |
27 28 29
|
3syl |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> ( { <. I , E >. } \ { (/) } ) = { <. I , E >. } ) |
31 |
21 30
|
uneq12d |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) \ { (/) } ) u. ( { <. I , E >. } \ { (/) } ) ) = ( ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) |
32 |
19 31
|
syl5eq |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) \ { (/) } ) = ( ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) |
33 |
32
|
funeqd |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> ( Fun ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) \ { (/) } ) <-> Fun ( ( ( G \ { (/) } ) |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) ) |
34 |
18 33
|
mpbird |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) \ { (/) } ) ) |
35 |
|
opex |
|- <. I , E >. e. _V |
36 |
35
|
a1i |
|- ( Fun ( G \ { (/) } ) -> <. I , E >. e. _V ) |
37 |
|
setsvalg |
|- ( ( G e. V /\ <. I , E >. e. _V ) -> ( G sSet <. I , E >. ) = ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) |
38 |
36 37
|
sylan2 |
|- ( ( G e. V /\ Fun ( G \ { (/) } ) ) -> ( G sSet <. I , E >. ) = ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) |
39 |
38
|
difeq1d |
|- ( ( G e. V /\ Fun ( G \ { (/) } ) ) -> ( ( G sSet <. I , E >. ) \ { (/) } ) = ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) \ { (/) } ) ) |
40 |
39
|
funeqd |
|- ( ( G e. V /\ Fun ( G \ { (/) } ) ) -> ( Fun ( ( G sSet <. I , E >. ) \ { (/) } ) <-> Fun ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) \ { (/) } ) ) ) |
41 |
40
|
adantr |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> ( Fun ( ( G sSet <. I , E >. ) \ { (/) } ) <-> Fun ( ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) \ { (/) } ) ) ) |
42 |
34 41
|
mpbird |
|- ( ( ( G e. V /\ Fun ( G \ { (/) } ) ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( G sSet <. I , E >. ) \ { (/) } ) ) |