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 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
psrbagconf1o.s 𝑆 = { 𝑦𝐷𝑦r𝐹 }
Assertion psrbagconf1oOLD ( ( 𝐼𝑉𝐹𝐷 ) → ( 𝑥𝑆 ↦ ( 𝐹f𝑥 ) ) : 𝑆1-1-onto𝑆 )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.s 𝑆 = { 𝑦𝐷𝑦r𝐹 }
3 eqid ( 𝑥𝑆 ↦ ( 𝐹f𝑥 ) ) = ( 𝑥𝑆 ↦ ( 𝐹f𝑥 ) )
4 simpll ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → 𝐼𝑉 )
5 simplr ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → 𝐹𝐷 )
6 simpr ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → 𝑥𝑆 )
7 breq1 ( 𝑦 = 𝑥 → ( 𝑦r𝐹𝑥r𝐹 ) )
8 7 2 elrab2 ( 𝑥𝑆 ↔ ( 𝑥𝐷𝑥r𝐹 ) )
9 6 8 sylib ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → ( 𝑥𝐷𝑥r𝐹 ) )
10 9 simpld ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → 𝑥𝐷 )
11 1 psrbagfOLD ( ( 𝐼𝑉𝑥𝐷 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
12 4 10 11 syl2anc ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
13 9 simprd ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → 𝑥r𝐹 )
14 1 psrbagconOLD ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝑥 : 𝐼 ⟶ ℕ0𝑥r𝐹 ) ) → ( ( 𝐹f𝑥 ) ∈ 𝐷 ∧ ( 𝐹f𝑥 ) ∘r𝐹 ) )
15 4 5 12 13 14 syl13anc ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → ( ( 𝐹f𝑥 ) ∈ 𝐷 ∧ ( 𝐹f𝑥 ) ∘r𝐹 ) )
16 breq1 ( 𝑦 = ( 𝐹f𝑥 ) → ( 𝑦r𝐹 ↔ ( 𝐹f𝑥 ) ∘r𝐹 ) )
17 16 2 elrab2 ( ( 𝐹f𝑥 ) ∈ 𝑆 ↔ ( ( 𝐹f𝑥 ) ∈ 𝐷 ∧ ( 𝐹f𝑥 ) ∘r𝐹 ) )
18 15 17 sylibr ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑥𝑆 ) → ( 𝐹f𝑥 ) ∈ 𝑆 )
19 18 ralrimiva ( ( 𝐼𝑉𝐹𝐷 ) → ∀ 𝑥𝑆 ( 𝐹f𝑥 ) ∈ 𝑆 )
20 oveq2 ( 𝑥 = 𝑧 → ( 𝐹f𝑥 ) = ( 𝐹f𝑧 ) )
21 20 eleq1d ( 𝑥 = 𝑧 → ( ( 𝐹f𝑥 ) ∈ 𝑆 ↔ ( 𝐹f𝑧 ) ∈ 𝑆 ) )
22 21 rspccva ( ( ∀ 𝑥𝑆 ( 𝐹f𝑥 ) ∈ 𝑆𝑧𝑆 ) → ( 𝐹f𝑧 ) ∈ 𝑆 )
23 19 22 sylan ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ 𝑧𝑆 ) → ( 𝐹f𝑧 ) ∈ 𝑆 )
24 1 psrbagfOLD ( ( 𝐼𝑉𝐹𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
25 24 adantr ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝐹 : 𝐼 ⟶ ℕ0 )
26 25 ffvelrnda ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝐹𝑛 ) ∈ ℕ0 )
27 simpll ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝐼𝑉 )
28 2 ssrab3 𝑆𝐷
29 simprr ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑧𝑆 )
30 28 29 sselid ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑧𝐷 )
31 1 psrbagfOLD ( ( 𝐼𝑉𝑧𝐷 ) → 𝑧 : 𝐼 ⟶ ℕ0 )
32 27 30 31 syl2anc ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑧 : 𝐼 ⟶ ℕ0 )
33 32 ffvelrnda ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝑧𝑛 ) ∈ ℕ0 )
34 12 adantrr ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑥 : 𝐼 ⟶ ℕ0 )
35 34 ffvelrnda ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝑥𝑛 ) ∈ ℕ0 )
36 nn0cn ( ( 𝐹𝑛 ) ∈ ℕ0 → ( 𝐹𝑛 ) ∈ ℂ )
37 nn0cn ( ( 𝑧𝑛 ) ∈ ℕ0 → ( 𝑧𝑛 ) ∈ ℂ )
38 nn0cn ( ( 𝑥𝑛 ) ∈ ℕ0 → ( 𝑥𝑛 ) ∈ ℂ )
39 subsub23 ( ( ( 𝐹𝑛 ) ∈ ℂ ∧ ( 𝑧𝑛 ) ∈ ℂ ∧ ( 𝑥𝑛 ) ∈ ℂ ) → ( ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) = ( 𝑥𝑛 ) ↔ ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) = ( 𝑧𝑛 ) ) )
40 36 37 38 39 syl3an ( ( ( 𝐹𝑛 ) ∈ ℕ0 ∧ ( 𝑧𝑛 ) ∈ ℕ0 ∧ ( 𝑥𝑛 ) ∈ ℕ0 ) → ( ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) = ( 𝑥𝑛 ) ↔ ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) = ( 𝑧𝑛 ) ) )
41 26 33 35 40 syl3anc ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) = ( 𝑥𝑛 ) ↔ ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) = ( 𝑧𝑛 ) ) )
42 eqcom ( ( 𝑥𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) ↔ ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) = ( 𝑥𝑛 ) )
43 eqcom ( ( 𝑧𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) ↔ ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) = ( 𝑧𝑛 ) )
44 41 42 43 3bitr4g ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝑥𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) ↔ ( 𝑧𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) ) )
45 25 ffnd ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝐹 Fn 𝐼 )
46 32 ffnd ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑧 Fn 𝐼 )
47 inidm ( 𝐼𝐼 ) = 𝐼
48 eqidd ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝐹𝑛 ) = ( 𝐹𝑛 ) )
49 eqidd ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝑧𝑛 ) = ( 𝑧𝑛 ) )
50 45 46 27 27 47 48 49 ofval ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝐹f𝑧 ) ‘ 𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) )
51 50 eqeq2d ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ↔ ( 𝑥𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) ) )
52 34 ffnd ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑥 Fn 𝐼 )
53 eqidd ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝑥𝑛 ) = ( 𝑥𝑛 ) )
54 45 52 27 27 47 48 53 ofval ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝐹f𝑥 ) ‘ 𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) )
55 54 eqeq2d ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ↔ ( 𝑧𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) ) )
56 44 51 55 3bitr4d ( ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ↔ ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ) )
57 56 ralbidva ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( ∀ 𝑛𝐼 ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ↔ ∀ 𝑛𝐼 ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ) )
58 23 adantrl ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑧 ) ∈ 𝑆 )
59 28 58 sselid ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑧 ) ∈ 𝐷 )
60 1 psrbagfOLD ( ( 𝐼𝑉 ∧ ( 𝐹f𝑧 ) ∈ 𝐷 ) → ( 𝐹f𝑧 ) : 𝐼 ⟶ ℕ0 )
61 27 59 60 syl2anc ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑧 ) : 𝐼 ⟶ ℕ0 )
62 61 ffnd ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑧 ) Fn 𝐼 )
63 eqfnfv ( ( 𝑥 Fn 𝐼 ∧ ( 𝐹f𝑧 ) Fn 𝐼 ) → ( 𝑥 = ( 𝐹f𝑧 ) ↔ ∀ 𝑛𝐼 ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ) )
64 52 62 63 syl2anc ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝑥 = ( 𝐹f𝑧 ) ↔ ∀ 𝑛𝐼 ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ) )
65 18 adantrr ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑥 ) ∈ 𝑆 )
66 28 65 sselid ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑥 ) ∈ 𝐷 )
67 1 psrbagfOLD ( ( 𝐼𝑉 ∧ ( 𝐹f𝑥 ) ∈ 𝐷 ) → ( 𝐹f𝑥 ) : 𝐼 ⟶ ℕ0 )
68 27 66 67 syl2anc ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑥 ) : 𝐼 ⟶ ℕ0 )
69 68 ffnd ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑥 ) Fn 𝐼 )
70 eqfnfv ( ( 𝑧 Fn 𝐼 ∧ ( 𝐹f𝑥 ) Fn 𝐼 ) → ( 𝑧 = ( 𝐹f𝑥 ) ↔ ∀ 𝑛𝐼 ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ) )
71 46 69 70 syl2anc ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝑧 = ( 𝐹f𝑥 ) ↔ ∀ 𝑛𝐼 ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ) )
72 57 64 71 3bitr4d ( ( ( 𝐼𝑉𝐹𝐷 ) ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝑥 = ( 𝐹f𝑧 ) ↔ 𝑧 = ( 𝐹f𝑥 ) ) )
73 3 18 23 72 f1o2d ( ( 𝐼𝑉𝐹𝐷 ) → ( 𝑥𝑆 ↦ ( 𝐹f𝑥 ) ) : 𝑆1-1-onto𝑆 )