Metamath Proof Explorer

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 = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
		psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
	Assertion	psrbagconcl	$⊢ (F \in D \land X \in S) \to F -_{f} X \in S$

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
2		psrbagconf1o.s	$⊢ S = \{y \in D \| y \leq_{f} F\}$
3		simpl	$⊢ (F \in D \land X \in S) \to F \in D$
4		simpr	$⊢ (F \in D \land X \in S) \to X \in S$
5		breq1	$⊢ y = X \to (y \leq_{f} F \leftrightarrow X \leq_{f} F)$
6	5 2	elrab2	$⊢ X \in S \leftrightarrow (X \in D \land X \leq_{f} F)$
7	4 6	sylib	$⊢ (F \in D \land X \in S) \to (X \in D \land X \leq_{f} F)$
8	7	simpld	$⊢ (F \in D \land X \in S) \to X \in D$
9	1	psrbagf	$⊢ X \in D \to X : I ⟶ ℕ_{0}$
10	8 9	syl	$⊢ (F \in D \land X \in S) \to X : I ⟶ ℕ_{0}$
11	7	simprd	$⊢ (F \in D \land X \in S) \to X \leq_{f} F$
12	1	psrbagcon	$⊢ (F \in D \land X : I ⟶ ℕ_{0} \land X \leq_{f} F) \to (F -_{f} X \in D \land (F -_{f} X) \leq_{f} F)$
13	3 10 11 12	syl3anc	$⊢ (F \in D \land X \in S) \to (F -_{f} X \in D \land (F -_{f} X) \leq_{f} F)$
14		breq1	$⊢ y = F -_{f} X \to (y \leq_{f} F \leftrightarrow (F -_{f} X) \leq_{f} F)$
15	14 2	elrab2	$⊢ F -_{f} X \in S \leftrightarrow (F -_{f} X \in D \land (F -_{f} X) \leq_{f} F)$
16	13 15	sylibr	$⊢ (F \in D \land X \in S) \to F -_{f} X \in S$