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

Metamath Proof Explorer

Theorem suppssfv

Description: Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 28-May-2019)

Ref Expression
Hypotheses suppssfv.a ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
suppssfv.f ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = 𝑍 )
suppssfv.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 )
suppssfv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion suppssfv ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 )

Proof

Step Hyp Ref Expression
1 suppssfv.a ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
2 suppssfv.f ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = 𝑍 )
3 suppssfv.v ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ 𝑉 )
4 suppssfv.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
5 eldifsni ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( V ∖ { 𝑍 } ) → ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 )
6 3 elexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) → 𝐴 ∈ V )
7 6 ad4ant23 ⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐴 ∈ V )
8 fveqeq2 ⊢ ( 𝐴 = 𝑌 → ( ( 𝐹 ‘ 𝐴 ) = 𝑍 ↔ ( 𝐹 ‘ 𝑌 ) = 𝑍 ) )
9 2 8 syl5ibrcom ⊢ ( 𝜑 → ( 𝐴 = 𝑌 → ( 𝐹 ‘ 𝐴 ) = 𝑍 ) )
10 9 necon3d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 → 𝐴 ≠ 𝑌 ) )
11 10 ad2antlr ⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 → 𝐴 ≠ 𝑌 ) )
12 11 imp ⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐴 ≠ 𝑌 )
13 eldifsn ⊢ ( 𝐴 ∈ ( V ∖ { 𝑌 } ) ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ 𝑌 ) )
14 7 12 13 sylanbrc ⊢ ( ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) )
15 14 ex ⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) ≠ 𝑍 → 𝐴 ∈ ( V ∖ { 𝑌 } ) ) )
16 5 15 syl5 ⊢ ( ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑥 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( V ∖ { 𝑍 } ) → 𝐴 ∈ ( V ∖ { 𝑌 } ) ) )
17 16 ss2rabdv ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝐴 ) ∈ ( V ∖ { 𝑍 } ) } ⊆ { 𝑥 ∈ 𝐷 ∣ 𝐴 ∈ ( V ∖ { 𝑌 } ) } )
18 eqid ⊢ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) )
19 simpll ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐷 ∈ V )
20 simplr ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑍 ∈ V )
21 18 19 20 mptsuppdifd ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) = { 𝑥 ∈ 𝐷 ∣ ( 𝐹 ‘ 𝐴 ) ∈ ( V ∖ { 𝑍 } ) } )
22 eqid ⊢ ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) = ( 𝑥 ∈ 𝐷 ↦ 𝐴 )
23 4 adantl ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑌 ∈ 𝑈 )
24 22 19 23 mptsuppdifd ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) = { 𝑥 ∈ 𝐷 ∣ 𝐴 ∈ ( V ∖ { 𝑌 } ) } )
25 17 21 24 3sstr4d ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) )
26 1 adantl ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ 𝐴 ) supp 𝑌 ) ⊆ 𝐿 )
27 25 26 sstrd ⊢ ( ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 )
28 27 ex ⊢ ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 ) )
29 mptexg ⊢ ( 𝐷 ∈ V → ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V )
30 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
31 30 rgenw ⊢ ∀ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝐴 ) ∈ V
32 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐷 ( 𝐹 ‘ 𝐴 ) ∈ V → dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) = 𝐷 )
33 31 32 ax-mp ⊢ dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) = 𝐷
34 dmexg ⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V → dom ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V )
35 33 34 eqeltrrid ⊢ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V → 𝐷 ∈ V )
36 29 35 impbii ⊢ ( 𝐷 ∈ V ↔ ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V )
37 36 anbi1i ⊢ ( ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) ↔ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V ∧ 𝑍 ∈ V ) )
38 supp0prc ⊢ ( ¬ ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) = ∅ )
39 37 38 sylnbi ⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) = ∅ )
40 0ss ⊢ ∅ ⊆ 𝐿
41 39 40 eqsstrdi ⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 )
42 41 a1d ⊢ ( ¬ ( 𝐷 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 ) )
43 28 42 pm2.61i ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝐴 ) ) supp 𝑍 ) ⊆ 𝐿 )