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 0 I | f -1 Fin
psrbagconf1o.s S = y D | y f F
Assertion psrbagconclOLD I V F D X S F f X S

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 psrbagconf1o.s S = y D | y f F
3 simp1 I V F D X S I V
4 simp2 I V F D X S F D
5 simp3 I V F D X S X S
6 breq1 y = X y f F X f F
7 6 2 elrab2 X S X D X f F
8 5 7 sylib I V F D X S X D X f F
9 8 simpld I V F D X S X D
10 1 psrbagfOLD I V X D X : I 0
11 3 9 10 syl2anc I V F D X S X : I 0
12 8 simprd I V F D X S X f F
13 1 psrbagconOLD I V F D X : I 0 X f F F f X D F f X f F
14 3 4 11 12 13 syl13anc I V F D X S F f X D F f X f F
15 breq1 y = F f X y f F F f X f F
16 15 2 elrab2 F f X S F f X D F f X f F
17 14 16 sylibr I V F D X S F f X S