Theorem psrbagconcl

Description: The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024)

	Ref	Expression
Hypotheses	psrbag.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrbagconf1o.s	$$⊢S=\left\{y\in D|y{\le }_{f}F\right\}$$
Assertion	psrbagconcl	$$⊢\left(F\in D\wedge X\in S\right)\to F{-}_{f}X\in S$$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		psrbagconf1o.s	$$⊢S=\left\{y\in D|y{\le }_{f}F\right\}$$
3		simpl	$$⊢\left(F\in D\wedge X\in S\right)\to F\in D$$
4		breq1	$$⊢y=X\to \left(y{\le }_{f}F\leftrightarrow X{\le }_{f}F\right)$$
5	4 2	elrab2	$$⊢X\in S\leftrightarrow \left(X\in D\wedge X{\le }_{f}F\right)$$
6	5	bilani	$$⊢\left(F\in D\wedge X\in S\right)\to \left(X\in D\wedge X{\le }_{f}F\right)$$
7	6	simpld	$$⊢\left(F\in D\wedge X\in S\right)\to X\in D$$
8	1	psrbagf	$$⊢X\in D\to X:I⟶{\mathbb{N}}_0$$
9	7 8	syl	$$⊢\left(F\in D\wedge X\in S\right)\to X:I⟶{\mathbb{N}}_0$$
10	6	simprd	$$⊢\left(F\in D\wedge X\in S\right)\to X{\le }_{f}F$$
11	1	psrbagcon	$$⊢\left(F\in D\wedge X:I⟶{\mathbb{N}}_0\wedge X{\le }_{f}F\right)\to \left(F{-}_{f}X\in D\wedge \left(F{-}_{f}X\right){\le }_{f}F\right)$$
12	3 9 10 11	syl3anc	$$⊢\left(F\in D\wedge X\in S\right)\to \left(F{-}_{f}X\in D\wedge \left(F{-}_{f}X\right){\le }_{f}F\right)$$
13		breq1	$$⊢y=F{-}_{f}X\to \left(y{\le }_{f}F\leftrightarrow \left(F{-}_{f}X\right){\le }_{f}F\right)$$
14	13 2	elrab2	$$⊢F{-}_{f}X\in S\leftrightarrow \left(F{-}_{f}X\in D\wedge \left(F{-}_{f}X\right){\le }_{f}F\right)$$
15	12 14	sylibr	$$⊢\left(F\in D\wedge X\in S\right)\to F{-}_{f}X\in S$$