Metamath Proof Explorer

Theorem setsfun

Description: A structure with replacement is a function if the original structure is a function. (Contributed by AV, 7-Jun-2021)

Ref Expression
Assertion setsfun 
|- ( ( ( G e. V /\ Fun G ) /\ ( I e. U /\ E e. W ) ) -> Fun ( G sSet <. I , E >. ) )

Proof

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 disjdifr 
 |-  ( ( _V \ dom { <. I , E >. } ) i^i dom { <. I , E >. } ) = (/)
10 9 ineq1i 
 |-  ( ( ( _V \ dom { <. I , E >. } ) i^i dom { <. I , E >. } ) i^i dom G ) = ( (/) i^i dom G )
11 0in 
 |-  ( (/) i^i dom G ) = (/)
12 8 10 11 3eqtri 
 |-  ( ( ( _V \ dom { <. I , E >. } ) i^i dom G ) i^i dom { <. I , E >. } ) = (/)
13 7 12 eqtri 
 |-  ( dom ( G |` ( _V \ dom { <. I , E >. } ) ) i^i dom { <. I , E >. } ) = (/)
14 13 a1i 
 |-  ( ( ( G e. V /\ Fun G ) /\ ( I e. U /\ E e. W ) ) -> ( dom ( G |` ( _V \ dom { <. I , E >. } ) ) i^i dom { <. I , E >. } ) = (/) )
15 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 >. } ) )
16 3 5 14 15 syl21anc 
 |-  ( ( ( G e. V /\ Fun G ) /\ ( I e. U /\ E e. W ) ) -> Fun ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) )
17 opex 
 |-  <. I , E >. e. _V
18 17 a1i 
 |-  ( Fun G -> <. I , E >. e. _V )
19 setsvalg 
 |-  ( ( G e. V /\ <. I , E >. e. _V ) -> ( G sSet <. I , E >. ) = ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) )
20 18 19 sylan2 
 |-  ( ( G e. V /\ Fun G ) -> ( G sSet <. I , E >. ) = ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) )
21 20 funeqd 
 |-  ( ( G e. V /\ Fun G ) -> ( Fun ( G sSet <. I , E >. ) <-> Fun ( ( G |` ( _V \ dom { <. I , E >. } ) ) u. { <. I , E >. } ) ) )
22 21 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 >. } ) ) )
23 16 22 mpbird 
 |-  ( ( ( G e. V /\ Fun G ) /\ ( I e. U /\ E e. W ) ) -> Fun ( G sSet <. I , E >. ) )