Metamath Proof Explorer


Theorem psrbagleclOLD

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

Ref Expression
Hypothesis psrbag.d D = f 0 I | f -1 Fin
Assertion psrbagleclOLD I V F D G : I 0 G f F G D

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 simpr2 I V F D G : I 0 G f F G : I 0
3 simpr1 I V F D G : I 0 G f F F D
4 1 psrbag I V F D F : I 0 F -1 Fin
5 4 adantr I V F D G : I 0 G f F F D F : I 0 F -1 Fin
6 3 5 mpbid I V F D G : I 0 G f F F : I 0 F -1 Fin
7 6 simprd I V F D G : I 0 G f F F -1 Fin
8 1 psrbaglesuppOLD I V F D G : I 0 G f F G -1 F -1
9 7 8 ssfid I V F D G : I 0 G f F G -1 Fin
10 1 psrbag I V G D G : I 0 G -1 Fin
11 10 adantr I V F D G : I 0 G f F G D G : I 0 G -1 Fin
12 2 9 11 mpbir2and I V F D G : I 0 G f F G D