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 ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) )

Proof

Step Hyp Ref Expression
1 funres ⊢ ( Fun ( 𝐺 ∖ { ∅ } ) → Fun ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
2 1 adantl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → Fun ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
3 2 adantr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
4 funsng ⊢ ( ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → Fun { ⟨ 𝐼 , 𝐸 ⟩ } )
5 4 adantl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun { ⟨ 𝐼 , 𝐸 ⟩ } )
6 dmres ⊢ dom ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) = ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) )
7 6 ineq1i ⊢ ( dom ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ( ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } )
8 in32 ⊢ ( ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ( ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) )
9 incom ⊢ ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ( dom { ⟨ 𝐼 , 𝐸 ⟩ } ∩ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) )
10 disjdif ⊢ ( dom { ⟨ 𝐼 , 𝐸 ⟩ } ∩ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) = ∅
11 9 10 eqtri ⊢ ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅
12 11 ineq1i ⊢ ( ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) = ( ∅ ∩ dom ( 𝐺 ∖ { ∅ } ) )
13 0in ⊢ ( ∅ ∩ dom ( 𝐺 ∖ { ∅ } ) ) = ∅
14 8 12 13 3eqtri ⊢ ( ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅
15 7 14 eqtri ⊢ ( dom ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅
16 15 a1i ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( dom ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅ )
17 funun ⊢ ( ( ( Fun ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∧ Fun { ⟨ 𝐼 , 𝐸 ⟩ } ) ∧ ( dom ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅ ) → Fun ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
18 3 5 16 17 syl21anc ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
19 difundir ⊢ ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) = ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∖ { ∅ } ) ∪ ( { ⟨ 𝐼 , 𝐸 ⟩ } ∖ { ∅ } ) )
20 resdifcom ⊢ ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∖ { ∅ } ) = ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) )
21 20 a1i ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∖ { ∅ } ) = ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
22 elex ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ V )
23 elex ⊢ ( 𝐸 ∈ 𝑊 → 𝐸 ∈ V )
24 22 23 anim12i ⊢ ( ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( 𝐼 ∈ V ∧ 𝐸 ∈ V ) )
25 opnz ⊢ ( ⟨ 𝐼 , 𝐸 ⟩ ≠ ∅ ↔ ( 𝐼 ∈ V ∧ 𝐸 ∈ V ) )
26 24 25 sylibr ⊢ ( ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ⟨ 𝐼 , 𝐸 ⟩ ≠ ∅ )
27 26 adantl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ⟨ 𝐼 , 𝐸 ⟩ ≠ ∅ )
28 disjsn2 ⊢ ( ⟨ 𝐼 , 𝐸 ⟩ ≠ ∅ → ( { ⟨ 𝐼 , 𝐸 ⟩ } ∩ { ∅ } ) = ∅ )
29 disjdif2 ⊢ ( ( { ⟨ 𝐼 , 𝐸 ⟩ } ∩ { ∅ } ) = ∅ → ( { ⟨ 𝐼 , 𝐸 ⟩ } ∖ { ∅ } ) = { ⟨ 𝐼 , 𝐸 ⟩ } )
30 27 28 29 3syl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( { ⟨ 𝐼 , 𝐸 ⟩ } ∖ { ∅ } ) = { ⟨ 𝐼 , 𝐸 ⟩ } )
31 21 30 uneq12d ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∖ { ∅ } ) ∪ ( { ⟨ 𝐼 , 𝐸 ⟩ } ∖ { ∅ } ) ) = ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
32 19 31 syl5eq ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) = ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
33 32 funeqd ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) ↔ Fun ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
34 18 33 mpbird ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) )
35 opex ⊢ ⟨ 𝐼 , 𝐸 ⟩ ∈ V
36 35 a1i ⊢ ( Fun ( 𝐺 ∖ { ∅ } ) → ⟨ 𝐼 , 𝐸 ⟩ ∈ V )
37 setsvalg ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ⟨ 𝐼 , 𝐸 ⟩ ∈ V ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
38 36 37 sylan2 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
39 38 difeq1d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) = ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) )
40 39 funeqd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ↔ Fun ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) ) )
41 40 adantr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ↔ Fun ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) ) )
42 34 41 mpbird ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) )