Metamath Proof Explorer


Theorem psrbagconOLD

Description: Obsolete version of psrbagcon 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 psrbagconOLD I V F D G : I 0 G f F F f G D F f G f F

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 simpr1 I V F D G : I 0 G f F F D
3 1 psrbag I V F D F : I 0 F -1 Fin
4 3 adantr I V F D G : I 0 G f F F D F : I 0 F -1 Fin
5 2 4 mpbid I V F D G : I 0 G f F F : I 0 F -1 Fin
6 5 simpld I V F D G : I 0 G f F F : I 0
7 6 ffnd I V F D G : I 0 G f F F Fn I
8 simpr2 I V F D G : I 0 G f F G : I 0
9 8 ffnd I V F D G : I 0 G f F G Fn I
10 simpl I V F D G : I 0 G f F I V
11 inidm I I = I
12 7 9 10 10 11 offn I V F D G : I 0 G f F F f G Fn I
13 eqidd I V F D G : I 0 G f F x I F x = F x
14 eqidd I V F D G : I 0 G f F x I G x = G x
15 7 9 10 10 11 13 14 ofval I V F D G : I 0 G f F x I F f G x = F x G x
16 simpr3 I V F D G : I 0 G f F G f F
17 9 7 10 10 11 14 13 ofrfval I V F D G : I 0 G f F G f F x I G x F x
18 16 17 mpbid I V F D G : I 0 G f F x I G x F x
19 18 r19.21bi I V F D G : I 0 G f F x I G x F x
20 8 ffvelrnda I V F D G : I 0 G f F x I G x 0
21 6 ffvelrnda I V F D G : I 0 G f F x I F x 0
22 nn0sub G x 0 F x 0 G x F x F x G x 0
23 20 21 22 syl2anc I V F D G : I 0 G f F x I G x F x F x G x 0
24 19 23 mpbid I V F D G : I 0 G f F x I F x G x 0
25 15 24 eqeltrd I V F D G : I 0 G f F x I F f G x 0
26 25 ralrimiva I V F D G : I 0 G f F x I F f G x 0
27 ffnfv F f G : I 0 F f G Fn I x I F f G x 0
28 12 26 27 sylanbrc I V F D G : I 0 G f F F f G : I 0
29 5 simprd I V F D G : I 0 G f F F -1 Fin
30 20 nn0ge0d I V F D G : I 0 G f F x I 0 G x
31 nn0re F x 0 F x
32 nn0re G x 0 G x
33 subge02 F x G x 0 G x F x G x F x
34 31 32 33 syl2an F x 0 G x 0 0 G x F x G x F x
35 21 20 34 syl2anc I V F D G : I 0 G f F x I 0 G x F x G x F x
36 30 35 mpbid I V F D G : I 0 G f F x I F x G x F x
37 36 ralrimiva I V F D G : I 0 G f F x I F x G x F x
38 12 7 10 10 11 15 13 ofrfval I V F D G : I 0 G f F F f G f F x I F x G x F x
39 37 38 mpbird I V F D G : I 0 G f F F f G f F
40 1 psrbaglesuppOLD I V F D F f G : I 0 F f G f F F f G -1 F -1
41 10 2 28 39 40 syl13anc I V F D G : I 0 G f F F f G -1 F -1
42 29 41 ssfid I V F D G : I 0 G f F F f G -1 Fin
43 1 psrbag I V F f G D F f G : I 0 F f G -1 Fin
44 43 adantr I V F D G : I 0 G f F F f G D F f G : I 0 F f G -1 Fin
45 28 42 44 mpbir2and I V F D G : I 0 G f F F f G D
46 45 39 jca I V F D G : I 0 G f F F f G D F f G f F