psrbagcon

Description: The analogue of the statement " 0 <_ G <_ F implies 0 <_ F - G <_ F " for finite bags. (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	psrbagcon	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F -_{f} G \in D \land (F -_{f} G) \leq_{f} F)$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2	1	psrbagf	$⊢ F \in D \to F : I ⟶ ℕ_{0}$
3	2	ffnd	$⊢ F \in D \to F Fn I$
4	3	3ad2ant1	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F Fn I$
5		simp2	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G : I ⟶ ℕ_{0}$
6	5	ffnd	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G Fn I$
7		id	$⊢ F \in D \to F \in D$
8	7 3	fndmexd	$⊢ F \in D \to I \in V$
9	8	3ad2ant1	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to I \in V$
10		inidm	$⊢ I \cap I = I$
11	4 6 9 9 10	offn	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F -_{f} G) Fn I$
12		eqidd	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to F (x) = F (x)$
13		eqidd	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to G (x) = G (x)$
14	4 6 9 9 10 12 13	ofval	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to (F -_{f} G) (x) = F (x) - G (x)$
15		simp3	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to G \leq_{f} F$
16	6 4 9 9 10 13 12	ofrfval	$⊢ (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))$
17	15 16	mpbid	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to \forall x \in I G (x) \leq F (x)$
18	17	r19.21bi	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to G (x) \leq F (x)$
19	5	ffvelrnda	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to G (x) \in ℕ_{0}$
20	2	3ad2ant1	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F : I ⟶ ℕ_{0}$
21	20	ffvelrnda	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to F (x) \in ℕ_{0}$
22		nn0sub	$⊢ (G (x) \in ℕ_{0} \land F (x) \in ℕ_{0}) \to (G (x) \leq F (x) \leftrightarrow F (x) - G (x) \in ℕ_{0})$
23	19 21 22	syl2anc	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to (G (x) \leq F (x) \leftrightarrow F (x) - G (x) \in ℕ_{0})$
24	18 23	mpbid	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to F (x) - G (x) \in ℕ_{0}$
25	14 24	eqeltrd	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to (F -_{f} G) (x) \in ℕ_{0}$
26	25	ralrimiva	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to \forall x \in I (F -_{f} G) (x) \in ℕ_{0}$
27		ffnfv	$⊢ (F -_{f} G) : I ⟶ ℕ_{0} \leftrightarrow ((F -_{f} G) Fn I \land \forall x \in I (F -_{f} G) (x) \in ℕ_{0})$
28	11 26 27	sylanbrc	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F -_{f} G) : I ⟶ ℕ_{0}$
29		simp1	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F \in D$
30	1	psrbag	$⊢ I \in V \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
31	9 30	syl	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F \in D \leftrightarrow (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin))$
32	29 31	mpbid	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F : I ⟶ ℕ_{0} \land F^{-1} [ℕ] \in Fin)$
33	32	simprd	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F^{-1} [ℕ] \in Fin$
34	19	nn0ge0d	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to 0 \leq G (x)$
35	21	nn0red	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to F (x) \in ℝ$
36	19	nn0red	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to G (x) \in ℝ$
37	35 36	subge02d	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to (0 \leq G (x) \leftrightarrow F (x) - G (x) \leq F (x))$
38	34 37	mpbid	$⊢ ((F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \land x \in I) \to F (x) - G (x) \leq F (x)$
39	38	ralrimiva	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to \forall x \in I F (x) - G (x) \leq F (x)$
40	11 4 9 9 10 14 12	ofrfval	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to ((F -_{f} G) \leq_{f} F \leftrightarrow \forall x \in I F (x) - G (x) \leq F (x))$
41	39 40	mpbird	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F -_{f} G) \leq_{f} F$
42	1	psrbaglesupp	$⊢ (F \in D \land (F -_{f} G) : I ⟶ ℕ_{0} \land (F -_{f} G) \leq_{f} F) \to {(F -_{f} G)}^{-1} [ℕ] \subseteq F^{-1} [ℕ]$
43	29 28 41 42	syl3anc	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to {(F -_{f} G)}^{-1} [ℕ] \subseteq F^{-1} [ℕ]$
44	33 43	ssfid	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to {(F -_{f} G)}^{-1} [ℕ] \in Fin$
45	1	psrbag	$⊢ I \in V \to (F -_{f} G \in D \leftrightarrow ((F -_{f} G) : I ⟶ ℕ_{0} \land {(F -_{f} G)}^{-1} [ℕ] \in Fin))$
46	9 45	syl	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F -_{f} G \in D \leftrightarrow ((F -_{f} G) : I ⟶ ℕ_{0} \land {(F -_{f} G)}^{-1} [ℕ] \in Fin))$
47	28 44 46	mpbir2and	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to F -_{f} G \in D$
48	47 41	jca	$⊢ (F \in D \land G : I ⟶ ℕ_{0} \land G \leq_{f} F) \to (F -_{f} G \in D \land (F -_{f} G) \leq_{f} F)$

Metamath Proof Explorer

Theorem psrbagcon

Proof