Metamath Proof Explorer

Theorem psrbagconf1o

Description: Bag complementation is a bijection on the set of bags dominated by a given bag F . (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Hypotheses psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrbagconf1o.1 
|- S = { y e. D | y oR <_ F }
Assertion psrbagconf1o 
|- ( ( I e. V /\ F e. D ) -> ( x e. S |-> ( F oF - x ) ) : S -1-1-onto-> S )

Proof

Step Hyp Ref Expression
1 psrbag.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
2 psrbagconf1o.1 
 |-  S = { y e. D | y oR <_ F }
3 eqid 
 |-  ( x e. S |-> ( F oF - x ) ) = ( x e. S |-> ( F oF - x ) )
4 simpll 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> I e. V )
5 simplr 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> F e. D )
6 simpr 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> x e. S )
7 breq1 
 |-  ( y = x -> ( y oR <_ F <-> x oR <_ F ) )
8 7 2 elrab2 
 |-  ( x e. S <-> ( x e. D /\ x oR <_ F ) )
9 6 8 sylib 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> ( x e. D /\ x oR <_ F ) )
10 9 simpld 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> x e. D )
11 1 psrbagf 
 |-  ( ( I e. V /\ x e. D ) -> x : I --> NN0 )
12 4 10 11 syl2anc 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> x : I --> NN0 )
13 9 simprd 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> x oR <_ F )
14 1 psrbagcon 
 |-  ( ( I e. V /\ ( F e. D /\ x : I --> NN0 /\ x oR <_ F ) ) -> ( ( F oF - x ) e. D /\ ( F oF - x ) oR <_ F ) )
15 4 5 12 13 14 syl13anc 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> ( ( F oF - x ) e. D /\ ( F oF - x ) oR <_ F ) )
16 breq1 
 |-  ( y = ( F oF - x ) -> ( y oR <_ F <-> ( F oF - x ) oR <_ F ) )
17 16 2 elrab2 
 |-  ( ( F oF - x ) e. S <-> ( ( F oF - x ) e. D /\ ( F oF - x ) oR <_ F ) )
18 15 17 sylibr 
 |-  ( ( ( I e. V /\ F e. D ) /\ x e. S ) -> ( F oF - x ) e. S )
19 18 ralrimiva 
 |-  ( ( I e. V /\ F e. D ) -> A. x e. S ( F oF - x ) e. S )
20 oveq2 
 |-  ( x = z -> ( F oF - x ) = ( F oF - z ) )
21 20 eleq1d 
 |-  ( x = z -> ( ( F oF - x ) e. S <-> ( F oF - z ) e. S ) )
22 21 rspccva 
 |-  ( ( A. x e. S ( F oF - x ) e. S /\ z e. S ) -> ( F oF - z ) e. S )
23 19 22 sylan 
 |-  ( ( ( I e. V /\ F e. D ) /\ z e. S ) -> ( F oF - z ) e. S )
24 1 psrbagf 
 |-  ( ( I e. V /\ F e. D ) -> F : I --> NN0 )
25 24 adantr 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> F : I --> NN0 )
26 25 ffvelrnda 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( F ` n ) e. NN0 )
27 simpll 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> I e. V )
28 2 ssrab3 
 |-  S C_ D
29 simprr 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> z e. S )
30 28 29 sseldi 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> z e. D )
31 1 psrbagf 
 |-  ( ( I e. V /\ z e. D ) -> z : I --> NN0 )
32 27 30 31 syl2anc 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> z : I --> NN0 )
33 32 ffvelrnda 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( z ` n ) e. NN0 )
34 12 adantrr 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> x : I --> NN0 )
35 34 ffvelrnda 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( x ` n ) e. NN0 )
36 nn0cn 
 |-  ( ( F ` n ) e. NN0 -> ( F ` n ) e. CC )
37 nn0cn 
 |-  ( ( z ` n ) e. NN0 -> ( z ` n ) e. CC )
38 nn0cn 
 |-  ( ( x ` n ) e. NN0 -> ( x ` n ) e. CC )
39 subsub23 
 |-  ( ( ( F ` n ) e. CC /\ ( z ` n ) e. CC /\ ( x ` n ) e. CC ) -> ( ( ( F ` n ) - ( z ` n ) ) = ( x ` n ) <-> ( ( F ` n ) - ( x ` n ) ) = ( z ` n ) ) )
40 36 37 38 39 syl3an 
 |-  ( ( ( F ` n ) e. NN0 /\ ( z ` n ) e. NN0 /\ ( x ` n ) e. NN0 ) -> ( ( ( F ` n ) - ( z ` n ) ) = ( x ` n ) <-> ( ( F ` n ) - ( x ` n ) ) = ( z ` n ) ) )
41 26 33 35 40 syl3anc 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( ( F ` n ) - ( z ` n ) ) = ( x ` n ) <-> ( ( F ` n ) - ( x ` n ) ) = ( z ` n ) ) )
42 eqcom 
 |-  ( ( x ` n ) = ( ( F ` n ) - ( z ` n ) ) <-> ( ( F ` n ) - ( z ` n ) ) = ( x ` n ) )
43 eqcom 
 |-  ( ( z ` n ) = ( ( F ` n ) - ( x ` n ) ) <-> ( ( F ` n ) - ( x ` n ) ) = ( z ` n ) )
44 41 42 43 3bitr4g 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( x ` n ) = ( ( F ` n ) - ( z ` n ) ) <-> ( z ` n ) = ( ( F ` n ) - ( x ` n ) ) ) )
45 25 ffnd 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> F Fn I )
46 32 ffnd 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> z Fn I )
47 inidm 
 |-  ( I i^i I ) = I
48 eqidd 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( F ` n ) = ( F ` n ) )
49 eqidd 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( z ` n ) = ( z ` n ) )
50 45 46 27 27 47 48 49 ofval 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( F oF - z ) ` n ) = ( ( F ` n ) - ( z ` n ) ) )
51 50 eqeq2d 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( x ` n ) = ( ( F oF - z ) ` n ) <-> ( x ` n ) = ( ( F ` n ) - ( z ` n ) ) ) )
52 34 ffnd 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> x Fn I )
53 eqidd 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( x ` n ) = ( x ` n ) )
54 45 52 27 27 47 48 53 ofval 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( F oF - x ) ` n ) = ( ( F ` n ) - ( x ` n ) ) )
55 54 eqeq2d 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( z ` n ) = ( ( F oF - x ) ` n ) <-> ( z ` n ) = ( ( F ` n ) - ( x ` n ) ) ) )
56 44 51 55 3bitr4d 
 |-  ( ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( x ` n ) = ( ( F oF - z ) ` n ) <-> ( z ` n ) = ( ( F oF - x ) ` n ) ) )
57 56 ralbidva 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( A. n e. I ( x ` n ) = ( ( F oF - z ) ` n ) <-> A. n e. I ( z ` n ) = ( ( F oF - x ) ` n ) ) )
58 23 adantrl 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( F oF - z ) e. S )
59 28 58 sseldi 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( F oF - z ) e. D )
60 1 psrbagf 
 |-  ( ( I e. V /\ ( F oF - z ) e. D ) -> ( F oF - z ) : I --> NN0 )
61 27 59 60 syl2anc 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( F oF - z ) : I --> NN0 )
62 61 ffnd 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( F oF - z ) Fn I )
63 eqfnfv 
 |-  ( ( x Fn I /\ ( F oF - z ) Fn I ) -> ( x = ( F oF - z ) <-> A. n e. I ( x ` n ) = ( ( F oF - z ) ` n ) ) )
64 52 62 63 syl2anc 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( x = ( F oF - z ) <-> A. n e. I ( x ` n ) = ( ( F oF - z ) ` n ) ) )
65 18 adantrr 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( F oF - x ) e. S )
66 28 65 sseldi 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( F oF - x ) e. D )
67 1 psrbagf 
 |-  ( ( I e. V /\ ( F oF - x ) e. D ) -> ( F oF - x ) : I --> NN0 )
68 27 66 67 syl2anc 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( F oF - x ) : I --> NN0 )
69 68 ffnd 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( F oF - x ) Fn I )
70 eqfnfv 
 |-  ( ( z Fn I /\ ( F oF - x ) Fn I ) -> ( z = ( F oF - x ) <-> A. n e. I ( z ` n ) = ( ( F oF - x ) ` n ) ) )
71 46 69 70 syl2anc 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( z = ( F oF - x ) <-> A. n e. I ( z ` n ) = ( ( F oF - x ) ` n ) ) )
72 57 64 71 3bitr4d 
 |-  ( ( ( I e. V /\ F e. D ) /\ ( x e. S /\ z e. S ) ) -> ( x = ( F oF - z ) <-> z = ( F oF - x ) ) )
73 3 18 23 72 f1o2d 
 |-  ( ( I e. V /\ F e. D ) -> ( x e. S |-> ( F oF - x ) ) : S -1-1-onto-> S )