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 e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
	psrbagconf1o.s	|- S = { y e. D | y oR <_ F }
Assertion	psrbagconcl	|- ( ( F e. D /\ X e. S ) -> ( F oF - X ) e. S )

Proof

Step	Hyp	Ref	Expression
1		psrbag.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2		psrbagconf1o.s	|- S = { y e. D | y oR <_ F }
3		simpl	|- ( ( F e. D /\ X e. S ) -> F e. D )
4		simpr	|- ( ( F e. D /\ X e. S ) -> X e. S )
5		breq1	|- ( y = X -> ( y oR <_ F <-> X oR <_ F ) )
6	5 2	elrab2	|- ( X e. S <-> ( X e. D /\ X oR <_ F ) )
7	4 6	sylib	|- ( ( F e. D /\ X e. S ) -> ( X e. D /\ X oR <_ F ) )
8	7	simpld	|- ( ( F e. D /\ X e. S ) -> X e. D )
9	1	psrbagf	|- ( X e. D -> X : I --> NN0 )
10	8 9	syl	|- ( ( F e. D /\ X e. S ) -> X : I --> NN0 )
11	7	simprd	|- ( ( F e. D /\ X e. S ) -> X oR <_ F )
12	1	psrbagcon	|- ( ( F e. D /\ X : I --> NN0 /\ X oR <_ F ) -> ( ( F oF - X ) e. D /\ ( F oF - X ) oR <_ F ) )
13	3 10 11 12	syl3anc	|- ( ( F e. D /\ X e. S ) -> ( ( F oF - X ) e. D /\ ( F oF - X ) oR <_ F ) )
14		breq1	|- ( y = ( F oF - X ) -> ( y oR <_ F <-> ( F oF - X ) oR <_ F ) )
15	14 2	elrab2	|- ( ( F oF - X ) e. S <-> ( ( F oF - X ) e. D /\ ( F oF - X ) oR <_ F ) )
16	13 15	sylibr	|- ( ( F e. D /\ X e. S ) -> ( F oF - X ) e. S )