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

Metamath Proof Explorer

Theorem funsssuppss

Description: The support of a function which is a subset of another function is a subset of the support of this other function. (Contributed by AV, 27-Jul-2019)

Ref Expression
Assertion funsssuppss ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )

Proof

Step Hyp Ref Expression
1 funss ⊢ ( 𝐹 ⊆ 𝐺 → ( Fun 𝐺 → Fun 𝐹 ) )
2 1 impcom ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ) → Fun 𝐹 )
3 2 funfnd ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ) → 𝐹 Fn dom 𝐹 )
4 funfn ⊢ ( Fun 𝐺 ↔ 𝐺 Fn dom 𝐺 )
5 4 birani ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ) → 𝐺 Fn dom 𝐺 )
6 3 5 jca ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺 ) )
7 6 3adant3 ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺 ) )
8 7 adantr ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ 𝑍 ∈ V ) → ( 𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺 ) )
9 dmss ⊢ ( 𝐹 ⊆ 𝐺 → dom 𝐹 ⊆ dom 𝐺 )
10 9 3ad2ant2 ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → dom 𝐹 ⊆ dom 𝐺 )
11 10 adantr ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ 𝑍 ∈ V ) → dom 𝐹 ⊆ dom 𝐺 )
12 dmexg ⊢ ( 𝐺 ∈ 𝑉 → dom 𝐺 ∈ V )
13 12 3ad2ant3 ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → dom 𝐺 ∈ V )
14 13 adantr ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ 𝑍 ∈ V ) → dom 𝐺 ∈ V )
15 simpr ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ 𝑍 ∈ V ) → 𝑍 ∈ V )
16 11 14 15 3jca ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ 𝑍 ∈ V ) → ( dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V ) )
17 8 16 jca ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ 𝑍 ∈ V ) → ( ( 𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺 ) ∧ ( dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V ) ) )
18 funssfv ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
19 18 3expa ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
20 eqeq1 ⊢ ( ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑍 ↔ ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
21 20 biimpd ⊢ ( ( 𝐺 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
22 19 21 syl ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ) ∧ 𝑥 ∈ dom 𝐹 ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
23 22 ralrimiva ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ) → ∀ 𝑥 ∈ dom 𝐹 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
24 23 3adant3 ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ∀ 𝑥 ∈ dom 𝐹 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
25 24 adantr ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ 𝑍 ∈ V ) → ∀ 𝑥 ∈ dom 𝐹 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) )
26 suppfnss ⊢ ( ( ( 𝐹 Fn dom 𝐹 ∧ 𝐺 Fn dom 𝐺 ) ∧ ( dom 𝐹 ⊆ dom 𝐺 ∧ dom 𝐺 ∈ V ∧ 𝑍 ∈ V ) ) → ( ∀ 𝑥 ∈ dom 𝐹 ( ( 𝐺 ‘ 𝑥 ) = 𝑍 → ( 𝐹 ‘ 𝑥 ) = 𝑍 ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ) )
27 17 25 26 sylc ⊢ ( ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )
28 27 expcom ⊢ ( 𝑍 ∈ V → ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ) )
29 ssid ⊢ ∅ ⊆ ∅
30 simpr ⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → 𝑍 ∈ V )
31 supp0prc ⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ∅ )
32 30 31 nsyl5 ⊢ ( ¬ 𝑍 ∈ V → ( 𝐹 supp 𝑍 ) = ∅ )
33 simpr ⊢ ( ( 𝐺 ∈ V ∧ 𝑍 ∈ V ) → 𝑍 ∈ V )
34 supp0prc ⊢ ( ¬ ( 𝐺 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐺 supp 𝑍 ) = ∅ )
35 33 34 nsyl5 ⊢ ( ¬ 𝑍 ∈ V → ( 𝐺 supp 𝑍 ) = ∅ )
36 32 35 sseq12d ⊢ ( ¬ 𝑍 ∈ V → ( ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ↔ ∅ ⊆ ∅ ) )
37 29 36 mpbiri ⊢ ( ¬ 𝑍 ∈ V → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )
38 37 a1d ⊢ ( ¬ 𝑍 ∈ V → ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) ) )
39 28 38 pm2.61i ⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ∧ 𝐺 ∈ 𝑉 ) → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐺 supp 𝑍 ) )