Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  psrbagcon Unicode version

Theorem psrbagcon 16117
 Description: The analogue of the statement " implies " for finite bags. (Contributed by Mario Carneiro, 29-Dec-2014.)
Hypothesis
Ref Expression
psrbag.d
Assertion
Ref Expression
psrbagcon
Distinct variable groups:   ,   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem psrbagcon
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpr1 961 . . . . . . . 8
2 psrbag.d . . . . . . . . . 10
32psrbag 16112 . . . . . . . . 9
43adantr 451 . . . . . . . 8
51, 4mpbid 201 . . . . . . 7
65simpld 445 . . . . . 6
7 ffn 5389 . . . . . 6
86, 7syl 15 . . . . 5
9 simpr2 962 . . . . . 6
10 ffn 5389 . . . . . 6
119, 10syl 15 . . . . 5
12 simpl 443 . . . . 5
13 inidm 3378 . . . . 5
148, 11, 12, 12, 13offn 6089 . . . 4
15 eqidd 2284 . . . . . . 7
16 eqidd 2284 . . . . . . 7
178, 11, 12, 12, 13, 15, 16ofval 6087 . . . . . 6
18 simpr3 963 . . . . . . . . 9
1911, 8, 12, 12, 13, 16, 15ofrfval 6086 . . . . . . . . 9
2018, 19mpbid 201 . . . . . . . 8
2120r19.21bi 2641 . . . . . . 7
22 ffvelrn 5663 . . . . . . . . 9
239, 22sylan 457 . . . . . . . 8
24 ffvelrn 5663 . . . . . . . . 9
256, 24sylan 457 . . . . . . . 8
26 nn0sub 10014 . . . . . . . 8
2723, 25, 26syl2anc 642 . . . . . . 7
2821, 27mpbid 201 . . . . . 6
2917, 28eqeltrd 2357 . . . . 5
3029ralrimiva 2626 . . . 4
31 ffnfv 5685 . . . 4
3214, 30, 31sylanbrc 645 . . 3
335simprd 449 . . . 4
3423nn0ge0d 10021 . . . . . . . 8
35 nn0re 9974 . . . . . . . . . 10
36 nn0re 9974 . . . . . . . . . 10
37 subge02 9289 . . . . . . . . . 10
3835, 36, 37syl2an 463 . . . . . . . . 9
3925, 23, 38syl2anc 642 . . . . . . . 8
4034, 39mpbid 201 . . . . . . 7
4140ralrimiva 2626 . . . . . 6
4214, 8, 12, 12, 13, 17, 15ofrfval 6086 . . . . . 6
4341, 42mpbird 223 . . . . 5
442psrbaglesupp 16114 . . . . 5
4512, 1, 32, 43, 44syl13anc 1184 . . . 4
46 ssfi 7083 . . . 4
4733, 45, 46syl2anc 642 . . 3
482psrbag 16112 . . . 4