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