Metamath Proof Explorer


Theorem suppssOLD

Description: Obsolete version of suppss as of 5-Aug-2024. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 28-May-2019) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses suppss.f ( 𝜑𝐹 : 𝐴𝐵 )
suppss.n ( ( 𝜑𝑘 ∈ ( 𝐴𝑊 ) ) → ( 𝐹𝑘 ) = 𝑍 )
Assertion suppssOLD ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )

Proof

Step Hyp Ref Expression
1 suppss.f ( 𝜑𝐹 : 𝐴𝐵 )
2 suppss.n ( ( 𝜑𝑘 ∈ ( 𝐴𝑊 ) ) → ( 𝐹𝑘 ) = 𝑍 )
3 1 ffnd ( 𝜑𝐹 Fn 𝐴 )
4 3 adantl ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐹 Fn 𝐴 )
5 fdm ( 𝐹 : 𝐴𝐵 → dom 𝐹 = 𝐴 )
6 dmexg ( 𝐹 ∈ V → dom 𝐹 ∈ V )
7 6 adantr ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → dom 𝐹 ∈ V )
8 eleq1 ( 𝐴 = dom 𝐹 → ( 𝐴 ∈ V ↔ dom 𝐹 ∈ V ) )
9 8 eqcoms ( dom 𝐹 = 𝐴 → ( 𝐴 ∈ V ↔ dom 𝐹 ∈ V ) )
10 7 9 syl5ibr ( dom 𝐹 = 𝐴 → ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → 𝐴 ∈ V ) )
11 1 5 10 3syl ( 𝜑 → ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → 𝐴 ∈ V ) )
12 11 impcom ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝐴 ∈ V )
13 simplr ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → 𝑍 ∈ V )
14 elsuppfn ( ( 𝐹 Fn 𝐴𝐴 ∈ V ∧ 𝑍 ∈ V ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑘𝐴 ∧ ( 𝐹𝑘 ) ≠ 𝑍 ) ) )
15 4 12 13 14 syl3anc ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) ↔ ( 𝑘𝐴 ∧ ( 𝐹𝑘 ) ≠ 𝑍 ) ) )
16 eldif ( 𝑘 ∈ ( 𝐴𝑊 ) ↔ ( 𝑘𝐴 ∧ ¬ 𝑘𝑊 ) )
17 2 adantll ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘 ∈ ( 𝐴𝑊 ) ) → ( 𝐹𝑘 ) = 𝑍 )
18 16 17 sylan2br ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ ( 𝑘𝐴 ∧ ¬ 𝑘𝑊 ) ) → ( 𝐹𝑘 ) = 𝑍 )
19 18 expr ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘𝐴 ) → ( ¬ 𝑘𝑊 → ( 𝐹𝑘 ) = 𝑍 ) )
20 19 necon1ad ( ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) ∧ 𝑘𝐴 ) → ( ( 𝐹𝑘 ) ≠ 𝑍𝑘𝑊 ) )
21 20 expimpd ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( ( 𝑘𝐴 ∧ ( 𝐹𝑘 ) ≠ 𝑍 ) → 𝑘𝑊 ) )
22 15 21 sylbid ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝑘 ∈ ( 𝐹 supp 𝑍 ) → 𝑘𝑊 ) )
23 22 ssrdv ( ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) ∧ 𝜑 ) → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
24 23 ex ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 ) )
25 supp0prc ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ∅ )
26 0ss ∅ ⊆ 𝑊
27 25 26 eqsstrdi ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )
28 27 a1d ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 ) )
29 24 28 pm2.61i ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ 𝑊 )