This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 )