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 |
|
opex |
|- <. I , E >. e. _V |
20 |
19
|
a1i |
|- ( Fun G -> <. I , E >. e. _V ) |
21 |
|
setsvalg |
|- ( ( G e. V /\ <. I , E >. e. _V ) -> ( G sSet <. I , E >. ) = ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) |
22 |
20 21
|
sylan2 |
|- ( ( G e. V /\ Fun G ) -> ( G sSet <. I , E >. ) = ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) |
23 |
22
|
funeqd |
|- ( ( G e. V /\ Fun G ) -> ( Fun ( G sSet <. I , E >. ) <-> Fun ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) ) |
24 |
23
|
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 >. } ) ) ) |
25 |
18 24
|
mpbird |
|- ( ( ( G e. V /\ Fun G ) /\ ( I e. U /\ E e. W ) ) -> Fun ( G sSet <. I , E >. ) ) |