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 )