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 V Fun G I U 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 V Fun G Fun G V dom I E
3 2 adantr G V Fun G I U E W Fun G V dom I E
4 funsng I U E W Fun I E
5 4 adantl G V Fun G I U E W Fun I E
6 dmres dom G V dom I E = V dom I E dom G
7 6 ineq1i dom G V dom I E dom I E = V dom I E dom G dom I E
8 in32 V dom I E dom G dom I E = V dom I E dom I E dom G
9 disjdifr V dom I E dom I E =
10 9 ineq1i V dom I E dom I E dom G = dom G
11 0in dom G =
12 8 10 11 3eqtri V dom I E dom G dom I E =
13 7 12 eqtri dom G V dom I E dom I E =
14 13 a1i G V Fun G I U E W dom G V dom I E dom I E =
15 funun Fun G V dom I E Fun I E dom G V dom I E dom I E = Fun G V dom I E I E
16 3 5 14 15 syl21anc G V Fun G I U E W Fun G V dom I E I E
17 difundir G V dom I E I E = G V dom I E I E
18 resdifcom G V dom I E = G V dom I E
19 18 a1i G V Fun G I U E W G V dom I E = G V dom I E
20 elex I U I V
21 elex E W E V
22 20 21 anim12i I U E W I V E V
23 opnz I E I V E V
24 22 23 sylibr I U E W I E
25 24 adantl G V Fun G I U E W I E
26 disjsn2 I E I E =
27 disjdif2 I E = I E = I E
28 25 26 27 3syl G V Fun G I U E W I E = I E
29 19 28 uneq12d G V Fun G I U E W G V dom I E I E = G V dom I E I E
30 17 29 eqtrid G V Fun G I U E W G V dom I E I E = G V dom I E I E
31 30 funeqd G V Fun G I U E W Fun G V dom I E I E Fun G V dom I E I E
32 16 31 mpbird G V Fun G I U E W Fun G V dom I E I E
33 opex I E V
34 33 a1i Fun G I E V
35 setsvalg G V I E V G sSet I E = G V dom I E I E
36 34 35 sylan2 G V Fun G G sSet I E = G V dom I E I E
37 36 difeq1d G V Fun G G sSet I E = G V dom I E I E
38 37 funeqd G V Fun G Fun G sSet I E Fun G V dom I E I E
39 38 adantr G V Fun G I U E W Fun G sSet I E Fun G V dom I E I E
40 32 39 mpbird G V Fun G I U E W Fun G sSet I E