Metamath Proof Explorer

Theorem setsfun0

Description: A structure with replacement without the empty set is a function if the original structure without the empty set is a function. This variant of setsfun is useful for proofs based on isstruct2 which requires Fun ( F \ { (/) } ) for F to be an extensible structure. (Contributed by AV, 7-Jun-2021)

Ref Expression
Assertion setsfun0 
|- ( ( ( 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 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 >. ) \ { (/) } ) )