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		simpr	$$⊢\left(F\in D\wedge X\in S\right)\to X\in S$$
5		breq1	$$⊢y=X\to \left(y{\le }_{f}F\leftrightarrow X{\le }_{f}F\right)$$
6	5 2	elrab2	$$⊢X\in S\leftrightarrow \left(X\in D\wedge X{\le }_{f}F\right)$$
7	4 6	sylib	$$⊢\left(F\in D\wedge X\in S\right)\to \left(X\in D\wedge X{\le }_{f}F\right)$$
8	7	simpld	$$⊢\left(F\in D\wedge X\in S\right)\to X\in D$$
9	1	psrbagf	$$⊢X\in D\to X:I⟶{\mathbb{N}}_0$$
10	8 9	syl	$$⊢\left(F\in D\wedge X\in S\right)\to X:I⟶{\mathbb{N}}_0$$
11	7	simprd	$$⊢\left(F\in D\wedge X\in S\right)\to X{\le }_{f}F$$
12	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)$$
13	3 10 11 12	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)$$
14		breq1	$$⊢y=F{-}_{f}X\to \left(y{\le }_{f}F\leftrightarrow \left(F{-}_{f}X\right){\le }_{f}F\right)$$
15	14 2	elrab2	$$⊢F{-}_{f}X\in S\leftrightarrow \left(F{-}_{f}X\in D\wedge \left(F{-}_{f}X\right){\le }_{f}F\right)$$
16	13 15	sylibr	$$⊢\left(F\in D\wedge X\in S\right)\to F{-}_{f}X\in S$$