psrbaglesupp

Description: The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

		Ref	Expression
	Hypothesis	psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	Assertion	psrbaglesupp	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G^{-1} [ℕ] \subseteq F^{-1} [ℕ]$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		df-ofr	$⊢ \circ_{r} \leq = \{⟨a, b⟩ \| \forall c \in (dom a \cap dom b) a (c) \leq b (c)\}$
3	2	relopabiv	$⊢ Rel \circ_{r} \leq$
4	3	brrelex1i	$⊢ G \leq_{f} F \to G \in V$
5	4	3ad2ant3	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G \in V$
6		simp2	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G : I ⟶ ℕ_{0}$
7		fcdmnn0suppg	$⊢ (G \in V \land G : I ⟶ ℕ_{0}) \to G supp 0 = G^{-1} [ℕ]$
8	5 6 7	syl2anc	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G supp 0 = G^{-1} [ℕ]$
9		eldifi	$⊢ x \in (I ∖ F^{-1} [ℕ]) \to x \in I$
10		simp3	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G \leq_{f} F$
11	6	ffnd	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G Fn I$
12	1	psrbagf	$⊢ F \in D \to F : I ⟶ ℕ_{0}$
13	12	3ad2ant1	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F : I ⟶ ℕ_{0}$
14	13	ffnd	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F Fn I$
15		simp1	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F \in D$
16		inidm	$⊢ I \cap I = I$
17		eqidd	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to G (x) = G (x)$
18		eqidd	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to F (x) = F (x)$
19	11 14 5 15 16 17 18	ofrfvalg	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (G \leq_{f} F \leftrightarrow \forall x \in I G (x) \leq F (x))$
20	10 19	mpbid	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to \forall x \in I G (x) \leq F (x)$
21	20	r19.21bi	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to G (x) \leq F (x)$
22	9 21	sylan2	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in (I ∖ F^{-1} [ℕ])) \to G (x) \leq F (x)$
23		fcdmnn0suppg	$⊢ (F \in D \land F : I ⟶ ℕ_{0}) \to F supp 0 = F^{-1} [ℕ]$
24	15 13 23	syl2anc	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F supp 0 = F^{-1} [ℕ]$
25		eqimss	$⊢ F supp 0 = F^{-1} [ℕ] \to F supp 0 \subseteq F^{-1} [ℕ]$
26	24 25	syl	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F supp 0 \subseteq F^{-1} [ℕ]$
27		c0ex	$⊢ 0 \in V$
28	27	a1i	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to 0 \in V$
29	13 26 15 28	suppssrg	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in (I ∖ F^{-1} [ℕ])) \to F (x) = 0$
30	22 29	breqtrd	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in (I ∖ F^{-1} [ℕ])) \to G (x) \leq 0$
31		ffvelcdm	$⊢ (G : I ⟶ ℕ_{0} \land x \in I) \to G (x) \in ℕ_{0}$
32	6 9 31	syl2an	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in (I ∖ F^{-1} [ℕ])) \to G (x) \in ℕ_{0}$
33	32	nn0ge0d	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in (I ∖ F^{-1} [ℕ])) \to 0 \leq G (x)$
34	32	nn0red	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in (I ∖ F^{-1} [ℕ])) \to G (x) \in ℝ$
35		0re	$⊢ 0 \in ℝ$
36		letri3	$⊢ (G (x) \in ℝ \land 0 \in ℝ) \to (G (x) = 0 \leftrightarrow (G (x) \leq 0 \land 0 \leq G (x)))$
37	34 35 36	sylancl	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in (I ∖ F^{-1} [ℕ])) \to (G (x) = 0 \leftrightarrow (G (x) \leq 0 \land 0 \leq G (x)))$
38	30 33 37	mpbir2and	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in (I ∖ F^{-1} [ℕ])) \to G (x) = 0$
39	6 38	suppss	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G supp 0 \subseteq F^{-1} [ℕ]$
40	8 39	eqsstrrd	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G^{-1} [ℕ] \subseteq F^{-1} [ℕ]$

Metamath Proof Explorer

Theorem psrbaglesupp

Proof