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 𝑍 ) )