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