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) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024)

Ref Expression
Hypotheses psrbag.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
psrbagconf1o.s 
|- S = { y e. D | y oR <_ F }
Assertion psrbagconf1o 
|- ( 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.s 
 |-  S = { y e. D | y oR <_ F }
3 eqid 
 |-  ( x e. S |-> ( F oF - x ) ) = ( x e. S |-> ( F oF - x ) )
4 1 2 psrbagconcl 
 |-  ( ( F e. D /\ x e. S ) -> ( F oF - x ) e. S )
5 1 2 psrbagconcl 
 |-  ( ( F e. D /\ z e. S ) -> ( F oF - z ) e. S )
6 1 psrbagf 
 |-  ( F e. D -> F : I --> NN0 )
7 6 adantr 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> F : I --> NN0 )
8 7 ffvelcdmda 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( F ` n ) e. NN0 )
9 2 ssrab3 
 |-  S C_ D
10 9 sseli 
 |-  ( z e. S -> z e. D )
11 10 adantl 
 |-  ( ( F e. D /\ z e. S ) -> z e. D )
12 1 psrbagf 
 |-  ( z e. D -> z : I --> NN0 )
13 11 12 syl 
 |-  ( ( F e. D /\ z e. S ) -> z : I --> NN0 )
14 13 adantrl 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> z : I --> NN0 )
15 14 ffvelcdmda 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( z ` n ) e. NN0 )
16 simprl 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> x e. S )
17 9 16 sselid 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> x e. D )
18 1 psrbagf 
 |-  ( x e. D -> x : I --> NN0 )
19 17 18 syl 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> x : I --> NN0 )
20 19 ffvelcdmda 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( x ` n ) e. NN0 )
21 nn0cn 
 |-  ( ( F ` n ) e. NN0 -> ( F ` n ) e. CC )
22 nn0cn 
 |-  ( ( z ` n ) e. NN0 -> ( z ` n ) e. CC )
23 nn0cn 
 |-  ( ( x ` n ) e. NN0 -> ( x ` n ) e. CC )
24 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 ) ) )
25 21 22 23 24 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 ) ) )
26 8 15 20 25 syl3anc 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( ( F ` n ) - ( z ` n ) ) = ( x ` n ) <-> ( ( F ` n ) - ( x ` n ) ) = ( z ` n ) ) )
27 eqcom 
 |-  ( ( x ` n ) = ( ( F ` n ) - ( z ` n ) ) <-> ( ( F ` n ) - ( z ` n ) ) = ( x ` n ) )
28 eqcom 
 |-  ( ( z ` n ) = ( ( F ` n ) - ( x ` n ) ) <-> ( ( F ` n ) - ( x ` n ) ) = ( z ` n ) )
29 26 27 28 3bitr4g 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( x ` n ) = ( ( F ` n ) - ( z ` n ) ) <-> ( z ` n ) = ( ( F ` n ) - ( x ` n ) ) ) )
30 6 ffnd 
 |-  ( F e. D -> F Fn I )
31 30 adantr 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> F Fn I )
32 13 ffnd 
 |-  ( ( F e. D /\ z e. S ) -> z Fn I )
33 32 adantrl 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> z Fn I )
34 19 ffnd 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> x Fn I )
35 16 34 fndmexd 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> I e. _V )
36 inidm 
 |-  ( I i^i I ) = I
37 eqidd 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( F ` n ) = ( F ` n ) )
38 eqidd 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( z ` n ) = ( z ` n ) )
39 31 33 35 35 36 37 38 ofval 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( F oF - z ) ` n ) = ( ( F ` n ) - ( z ` n ) ) )
40 39 eqeq2d 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( x ` n ) = ( ( F oF - z ) ` n ) <-> ( x ` n ) = ( ( F ` n ) - ( z ` n ) ) ) )
41 eqidd 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( x ` n ) = ( x ` n ) )
42 31 34 35 35 36 37 41 ofval 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( F oF - x ) ` n ) = ( ( F ` n ) - ( x ` n ) ) )
43 42 eqeq2d 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( z ` n ) = ( ( F oF - x ) ` n ) <-> ( z ` n ) = ( ( F ` n ) - ( x ` n ) ) ) )
44 29 40 43 3bitr4d 
 |-  ( ( ( F e. D /\ ( x e. S /\ z e. S ) ) /\ n e. I ) -> ( ( x ` n ) = ( ( F oF - z ) ` n ) <-> ( z ` n ) = ( ( F oF - x ) ` n ) ) )
45 44 ralbidva 
 |-  ( ( 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 ) ) )
46 5 adantrl 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> ( F oF - z ) e. S )
47 9 46 sselid 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> ( F oF - z ) e. D )
48 1 psrbagf 
 |-  ( ( F oF - z ) e. D -> ( F oF - z ) : I --> NN0 )
49 47 48 syl 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> ( F oF - z ) : I --> NN0 )
50 49 ffnd 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> ( F oF - z ) Fn I )
51 eqfnfv 
 |-  ( ( x Fn I /\ ( F oF - z ) Fn I ) -> ( x = ( F oF - z ) <-> A. n e. I ( x ` n ) = ( ( F oF - z ) ` n ) ) )
52 34 50 51 syl2anc 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> ( x = ( F oF - z ) <-> A. n e. I ( x ` n ) = ( ( F oF - z ) ` n ) ) )
53 9 4 sselid 
 |-  ( ( F e. D /\ x e. S ) -> ( F oF - x ) e. D )
54 1 psrbagf 
 |-  ( ( F oF - x ) e. D -> ( F oF - x ) : I --> NN0 )
55 53 54 syl 
 |-  ( ( F e. D /\ x e. S ) -> ( F oF - x ) : I --> NN0 )
56 55 ffnd 
 |-  ( ( F e. D /\ x e. S ) -> ( F oF - x ) Fn I )
57 56 adantrr 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> ( F oF - x ) Fn I )
58 eqfnfv 
 |-  ( ( z Fn I /\ ( F oF - x ) Fn I ) -> ( z = ( F oF - x ) <-> A. n e. I ( z ` n ) = ( ( F oF - x ) ` n ) ) )
59 33 57 58 syl2anc 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> ( z = ( F oF - x ) <-> A. n e. I ( z ` n ) = ( ( F oF - x ) ` n ) ) )
60 45 52 59 3bitr4d 
 |-  ( ( F e. D /\ ( x e. S /\ z e. S ) ) -> ( x = ( F oF - z ) <-> z = ( F oF - x ) ) )
61 3 4 5 60 f1o2d 
 |-  ( F e. D -> ( x e. S |-> ( F oF - x ) ) : S -1-1-onto-> S )