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