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 ( ( ( 𝐺 ∈ 𝑉 ∧ 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 opex ⊢ ⟨ 𝐼 , 𝐸 ⟩ ∈ V
20 19 a1i ⊢ ( Fun 𝐺 → ⟨ 𝐼 , 𝐸 ⟩ ∈ V )
21 setsvalg ⊢ ( ( 𝐺 ∈ 𝑉 ∧ ⟨ 𝐼 , 𝐸 ⟩ ∈ V ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
22 20 21 sylan2 ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) → ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) )
23 22 funeqd ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) → ( Fun ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ↔ Fun ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
24 23 adantr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → ( Fun ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ↔ Fun ( ( 𝐺 ↾ ( V ∖ dom { ⟨ 𝐼 , 𝐸 ⟩ } ) ) ∪ { ⟨ 𝐼 , 𝐸 ⟩ } ) ) )
25 18 24 mpbird ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ ( 𝐼 ∈ 𝑈 ∧ 𝐸 ∈ 𝑊 ) ) → Fun ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )