Metamath Proof Explorer


Theorem psrbagconclOLD

Description: Obsolete version of psrbagconcl as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (New usage is discouraged.) (Proof modification is discouraged.)

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 psrbagconclOLD
|- ( ( I e. V /\ 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 simp1
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> I e. V )
4 simp2
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> F e. D )
5 simp3
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> X e. S )
6 breq1
 |-  ( y = X -> ( y oR <_ F <-> X oR <_ F ) )
7 6 2 elrab2
 |-  ( X e. S <-> ( X e. D /\ X oR <_ F ) )
8 5 7 sylib
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> ( X e. D /\ X oR <_ F ) )
9 8 simpld
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> X e. D )
10 1 psrbagfOLD
 |-  ( ( I e. V /\ X e. D ) -> X : I --> NN0 )
11 3 9 10 syl2anc
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> X : I --> NN0 )
12 8 simprd
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> X oR <_ F )
13 1 psrbagconOLD
 |-  ( ( I e. V /\ ( F e. D /\ X : I --> NN0 /\ X oR <_ F ) ) -> ( ( F oF - X ) e. D /\ ( F oF - X ) oR <_ F ) )
14 3 4 11 12 13 syl13anc
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> ( ( F oF - X ) e. D /\ ( F oF - X ) oR <_ F ) )
15 breq1
 |-  ( y = ( F oF - X ) -> ( y oR <_ F <-> ( F oF - X ) oR <_ F ) )
16 15 2 elrab2
 |-  ( ( F oF - X ) e. S <-> ( ( F oF - X ) e. D /\ ( F oF - X ) oR <_ F ) )
17 14 16 sylibr
 |-  ( ( I e. V /\ F e. D /\ X e. S ) -> ( F oF - X ) e. S )