This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 disjdifr ⊢ ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅
10 9 ineq1i ⊢ ( ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) = ( ∅ ∩ dom ( 𝐺 ∖ { ∅ } ) )
11 0in ⊢ ( ∅ ∩ dom ( 𝐺 ∖ { ∅ } ) ) = ∅
12 8 10 11 3eqtri ⊢ ( ( ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ∩ dom ( 𝐺 ∖ { ∅ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅
13 7 12 eqtri ⊢ ( dom ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅
14 13 a1i ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( dom ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅ )
15 funun ⊢ ( ( ( Fun ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∧ Fun { ⟨ 𝐼 , 𝐸 ⟩ } ) ∧ ( dom ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∩ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) = ∅ ) → Fun ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
16 3 5 14 15 syl21anc ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
17 difundir ⊢ ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) = ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∖ { ∅ } ) ∪ ( { ⟨ 𝐼 , 𝐸 ⟩ } ∖ { ∅ } ) )
18 resdifcom ⊢ ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∖ { ∅ } ) = ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) )
19 18 a1i ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∖ { ∅ } ) = ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
20 elex ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ∈ V )
21 elex ⊢ ( 𝐸 ∈ 𝑊 → 𝐸 ∈ V )
22 20 21 anim12i ⊢ ( ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ( 𝐼 ∈ V ∧ 𝐸 ∈ V ) )
23 opnz ⊢ ( ⟨ 𝐼 , 𝐸 ⟩ ≠ ∅ ↔ ( 𝐼 ∈ V ∧ 𝐸 ∈ V ) )
24 22 23 sylibr ⊢ ( ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) → ⟨ 𝐼 , 𝐸 ⟩ ≠ ∅ )
25 24 adantl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ⟨ 𝐼 , 𝐸 ⟩ ≠ ∅ )
26 disjsn2 ⊢ ( ⟨ 𝐼 , 𝐸 ⟩ ≠ ∅ → ( { ⟨ 𝐼 , 𝐸 ⟩ } ∩ { ∅ } ) = ∅ )
27 disjdif2 ⊢ ( ( { ⟨ 𝐼 , 𝐸 ⟩ } ∩ { ∅ } ) = ∅ → ( { ⟨ 𝐼 , 𝐸 ⟩ } ∖ { ∅ } ) = { ⟨ 𝐼 , 𝐸 ⟩ } )
28 25 26 27 3syl ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( { ⟨ 𝐼 , 𝐸 ⟩ } ∖ { ∅ } ) = { ⟨ 𝐼 , 𝐸 ⟩ } )
29 19 28 uneq12d ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∖ { ∅ } ) ∪ ( { ⟨ 𝐼 , 𝐸 ⟩ } ∖ { ∅ } ) ) = ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
30 17 29 eqtrid ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) = ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
31 30 funeqd ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) ↔ Fun ( ( ( 𝐺 ∖ { ∅ } ) ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
32 16 31 mpbird ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) )
33 opex ⊢ ⟨ 𝐼 , 𝐸 ⟩ ∈ V
34 33 a1i ⊢ ( Fun ( 𝐺 ∖ { ∅ } ) → ⟨ 𝐼 , 𝐸 ⟩ ∈ V )
35 setsvalg ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ⟨ 𝐼 , 𝐸 ⟩ ∈ V ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
36 34 35 sylan2 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
37 36 difeq1d ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) = ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) )
38 37 funeqd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) → ( Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ↔ Fun ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) ) )
39 38 adantr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ↔ Fun ( ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ∖ { ∅ } ) ) )
40 32 39 mpbird ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun ( 𝐺 ∖ { ∅ } ) ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) )