Metamath Proof Explorer


Theorem psrbaglesupp

Description: The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 df-ofr r = a b | c dom a dom b a c b c
3 2 relopabiv Rel r
4 3 brrelex1i G f F G V
5 4 3ad2ant3 F D G : I 0 G f F G V
6 simp2 F D G : I 0 G f F G : I 0
7 frnnn0suppg G V G : I 0 G supp 0 = G -1
8 5 6 7 syl2anc F D G : I 0 G f F G supp 0 = G -1
9 eldifi x I F -1 x I
10 simp3 F D G : I 0 G f F G f F
11 6 ffnd F D G : I 0 G f F G Fn I
12 1 psrbagf F D F : I 0
13 12 3ad2ant1 F D G : I 0 G f F F : I 0
14 13 ffnd F D G : I 0 G f F F Fn I
15 simp1 F D G : I 0 G f F F D
16 inidm I I = I
17 eqidd F D G : I 0 G f F x I G x = G x
18 eqidd F D G : I 0 G f F x I F x = F x
19 11 14 5 15 16 17 18 ofrfvalg F D G : I 0 G f F G f F x I G x F x
20 10 19 mpbid F D G : I 0 G f F x I G x F x
21 20 r19.21bi F D G : I 0 G f F x I G x F x
22 9 21 sylan2 F D G : I 0 G f F x I F -1 G x F x
23 frnnn0suppg F D F : I 0 F supp 0 = F -1
24 15 13 23 syl2anc F D G : I 0 G f F F supp 0 = F -1
25 eqimss F supp 0 = F -1 F supp 0 F -1
26 24 25 syl F D G : I 0 G f F F supp 0 F -1
27 c0ex 0 V
28 27 a1i F D G : I 0 G f F 0 V
29 13 26 15 28 suppssrg F D G : I 0 G f F x I F -1 F x = 0
30 22 29 breqtrd F D G : I 0 G f F x I F -1 G x 0
31 ffvelrn G : I 0 x I G x 0
32 6 9 31 syl2an F D G : I 0 G f F x I F -1 G x 0
33 32 nn0ge0d F D G : I 0 G f F x I F -1 0 G x
34 32 nn0red F D G : I 0 G f F x I F -1 G x
35 0re 0
36 letri3 G x 0 G x = 0 G x 0 0 G x
37 34 35 36 sylancl F D G : I 0 G f F x I F -1 G x = 0 G x 0 0 G x
38 30 33 37 mpbir2and F D G : I 0 G f F x I F -1 G x = 0
39 6 38 suppss F D G : I 0 G f F G supp 0 F -1
40 8 39 eqsstrrd F D G : I 0 G f F G -1 F -1