Metamath Proof Explorer

Theorem funsnfsupp

Description: Finite support for a function extended by a singleton. (Contributed by Stefan O'Rear, 27-Feb-2015) (Revised by AV, 19-Jul-2019)

Ref Expression
Assertion funsnfsupp ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) )
2 1 anim2i ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) ) → ( 𝑍 ∈ V ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) )
3 2 ancomd ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ 𝑍 ∈ V ) )
4 df-3an ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V ) ↔ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ 𝑍 ∈ V ) )
5 3 4 sylibr ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V ) )
6 snopfsupp ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ V ) → { ⟨ 𝑋 , 𝑌 ⟩ } finSupp 𝑍 )
7 5 6 syl ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) ) → { ⟨ 𝑋 , 𝑌 ⟩ } finSupp 𝑍 )
8 funsng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → Fun { ⟨ 𝑋 , 𝑌 ⟩ } )
9 simpl ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) → Fun 𝐹 )
10 8 9 anim12ci ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) → ( Fun 𝐹 ∧ Fun { ⟨ 𝑋 , 𝑌 ⟩ } ) )
11 dmsnopg ⊢ ( 𝑌 ∈ 𝑊 → dom { ⟨ 𝑋 , 𝑌 ⟩ } = { 𝑋 } )
12 11 adantl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → dom { ⟨ 𝑋 , 𝑌 ⟩ } = { 𝑋 } )
13 12 ineq2d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( dom 𝐹 ∩ dom { ⟨ 𝑋 , 𝑌 ⟩ } ) = ( dom 𝐹 ∩ { 𝑋 } ) )
14 df-nel ⊢ ( 𝑋 ∉ dom 𝐹 ↔ ¬ 𝑋 ∈ dom 𝐹 )
15 disjsn ⊢ ( ( dom 𝐹 ∩ { 𝑋 } ) = ∅ ↔ ¬ 𝑋 ∈ dom 𝐹 )
16 14 15 sylbb2 ⊢ ( 𝑋 ∉ dom 𝐹 → ( dom 𝐹 ∩ { 𝑋 } ) = ∅ )
17 16 adantl ⊢ ( ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) → ( dom 𝐹 ∩ { 𝑋 } ) = ∅ )
18 13 17 sylan9eq ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) → ( dom 𝐹 ∩ dom { ⟨ 𝑋 , 𝑌 ⟩ } ) = ∅ )
19 10 18 jca ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) → ( ( Fun 𝐹 ∧ Fun { ⟨ 𝑋 , 𝑌 ⟩ } ) ∧ ( dom 𝐹 ∩ dom { ⟨ 𝑋 , 𝑌 ⟩ } ) = ∅ ) )
20 19 adantl ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) ) → ( ( Fun 𝐹 ∧ Fun { ⟨ 𝑋 , 𝑌 ⟩ } ) ∧ ( dom 𝐹 ∩ dom { ⟨ 𝑋 , 𝑌 ⟩ } ) = ∅ ) )
21 funun ⊢ ( ( ( Fun 𝐹 ∧ Fun { ⟨ 𝑋 , 𝑌 ⟩ } ) ∧ ( dom 𝐹 ∩ dom { ⟨ 𝑋 , 𝑌 ⟩ } ) = ∅ ) → Fun ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
22 20 21 syl ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) ) → Fun ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) )
23 22 fsuppunbi ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) finSupp 𝑍 ↔ ( 𝐹 finSupp 𝑍 ∧ { ⟨ 𝑋 , 𝑌 ⟩ } finSupp 𝑍 ) ) )
24 7 23 mpbiran2d ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍 ) )
25 24 ex ⊢ ( 𝑍 ∈ V → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍 ) ) )
26 relfsupp ⊢ Rel finSupp
27 26 brrelex2i ⊢ ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) finSupp 𝑍 → 𝑍 ∈ V )
28 26 brrelex2i ⊢ ( 𝐹 finSupp 𝑍 → 𝑍 ∈ V )
29 27 28 pm5.21ni ⊢ ( ¬ 𝑍 ∈ V → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍 ) )
30 29 a1d ⊢ ( ¬ 𝑍 ∈ V → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍 ) ) )
31 25 30 pm2.61i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ∧ ( Fun 𝐹 ∧ 𝑋 ∉ dom 𝐹 ) ) → ( ( 𝐹 ∪ { ⟨ 𝑋 , 𝑌 ⟩ } ) finSupp 𝑍 ↔ 𝐹 finSupp 𝑍 ) )