Metamath Proof Explorer


Theorem psrbagconf1oOLD

Description: Obsolete version of psrbagconf1o as of 6-Aug-2024. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses psrbag.d D = f 0 I | f -1 Fin
psrbagconf1o.s S = y D | y f F
Assertion psrbagconf1oOLD I V F D x S F f x : S 1-1 onto S

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 psrbagconf1o.s S = y D | y f F
3 eqid x S F f x = x S F f x
4 simpll I V F D x S I V
5 simplr I V F D x S F D
6 simpr I V F D x S x S
7 breq1 y = x y f F x f F
8 7 2 elrab2 x S x D x f F
9 6 8 sylib I V F D x S x D x f F
10 9 simpld I V F D x S x D
11 1 psrbagfOLD I V x D x : I 0
12 4 10 11 syl2anc I V F D x S x : I 0
13 9 simprd I V F D x S x f F
14 1 psrbagconOLD I V F D x : I 0 x f F F f x D F f x f F
15 4 5 12 13 14 syl13anc I V F D x S F f x D F f x f F
16 breq1 y = F f x y f F F f x f F
17 16 2 elrab2 F f x S F f x D F f x f F
18 15 17 sylibr I V F D x S F f x S
19 18 ralrimiva I V F D x S F f x S
20 oveq2 x = z F f x = F f z
21 20 eleq1d x = z F f x S F f z S
22 21 rspccva x S F f x S z S F f z S
23 19 22 sylan I V F D z S F f z S
24 1 psrbagfOLD I V F D F : I 0
25 24 adantr I V F D x S z S F : I 0
26 25 ffvelrnda I V F D x S z S n I F n 0
27 simpll I V F D x S z S I V
28 2 ssrab3 S D
29 simprr I V F D x S z S z S
30 28 29 sselid I V F D x S z S z D
31 1 psrbagfOLD I V z D z : I 0
32 27 30 31 syl2anc I V F D x S z S z : I 0
33 32 ffvelrnda I V F D x S z S n I z n 0
34 12 adantrr I V F D x S z S x : I 0
35 34 ffvelrnda I V F D x S z S n I x n 0
36 nn0cn F n 0 F n
37 nn0cn z n 0 z n
38 nn0cn x n 0 x n
39 subsub23 F n z n x n F n z n = x n F n x n = z n
40 36 37 38 39 syl3an F n 0 z n 0 x n 0 F n z n = x n F n x n = z n
41 26 33 35 40 syl3anc I V F D x S z S n 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 V F D x S z S n I x n = F n z n z n = F n x n
45 25 ffnd I V F D x S z S F Fn I
46 32 ffnd I V F D x S z S z Fn I
47 inidm I I = I
48 eqidd I V F D x S z S n I F n = F n
49 eqidd I V F D x S z S n I z n = z n
50 45 46 27 27 47 48 49 ofval I V F D x S z S n I F f z n = F n z n
51 50 eqeq2d I V F D x S z S n I x n = F f z n x n = F n z n
52 34 ffnd I V F D x S z S x Fn I
53 eqidd I V F D x S z S n I x n = x n
54 45 52 27 27 47 48 53 ofval I V F D x S z S n I F f x n = F n x n
55 54 eqeq2d I V F D x S z S n I z n = F f x n z n = F n x n
56 44 51 55 3bitr4d I V F D x S z S n I x n = F f z n z n = F f x n
57 56 ralbidva I V F D x S z S n I x n = F f z n n I z n = F f x n
58 23 adantrl I V F D x S z S F f z S
59 28 58 sselid I V F D x S z S F f z D
60 1 psrbagfOLD I V F f z D F f z : I 0
61 27 59 60 syl2anc I V F D x S z S F f z : I 0
62 61 ffnd I V F D x S z S F f z Fn I
63 eqfnfv x Fn I F f z Fn I x = F f z n I x n = F f z n
64 52 62 63 syl2anc I V F D x S z S x = F f z n I x n = F f z n
65 18 adantrr I V F D x S z S F f x S
66 28 65 sselid I V F D x S z S F f x D
67 1 psrbagfOLD I V F f x D F f x : I 0
68 27 66 67 syl2anc I V F D x S z S F f x : I 0
69 68 ffnd I V F D x S z S F f x Fn I
70 eqfnfv z Fn I F f x Fn I z = F f x n I z n = F f x n
71 46 69 70 syl2anc I V F D x S z S z = F f x n I z n = F f x n
72 57 64 71 3bitr4d I V F D x S z S x = F f z z = F f x
73 3 18 23 72 f1o2d I V F D x S F f x : S 1-1 onto S