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

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.s 𝑆 = { 𝑦𝐷𝑦r𝐹 }
3 eqid ( 𝑥𝑆 ↦ ( 𝐹f𝑥 ) ) = ( 𝑥𝑆 ↦ ( 𝐹f𝑥 ) )
4 1 2 psrbagconcl ( ( 𝐹𝐷𝑥𝑆 ) → ( 𝐹f𝑥 ) ∈ 𝑆 )
5 1 2 psrbagconcl ( ( 𝐹𝐷𝑧𝑆 ) → ( 𝐹f𝑧 ) ∈ 𝑆 )
6 1 psrbagf ( 𝐹𝐷𝐹 : 𝐼 ⟶ ℕ0 )
7 6 adantr ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝐹 : 𝐼 ⟶ ℕ0 )
8 7 ffvelrnda ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝐹𝑛 ) ∈ ℕ0 )
9 2 ssrab3 𝑆𝐷
10 9 sseli ( 𝑧𝑆𝑧𝐷 )
11 10 adantl ( ( 𝐹𝐷𝑧𝑆 ) → 𝑧𝐷 )
12 1 psrbagf ( 𝑧𝐷𝑧 : 𝐼 ⟶ ℕ0 )
13 11 12 syl ( ( 𝐹𝐷𝑧𝑆 ) → 𝑧 : 𝐼 ⟶ ℕ0 )
14 13 adantrl ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑧 : 𝐼 ⟶ ℕ0 )
15 14 ffvelrnda ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝑧𝑛 ) ∈ ℕ0 )
16 simprl ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑥𝑆 )
17 9 16 sselid ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑥𝐷 )
18 1 psrbagf ( 𝑥𝐷𝑥 : 𝐼 ⟶ ℕ0 )
19 17 18 syl ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑥 : 𝐼 ⟶ ℕ0 )
20 19 ffvelrnda ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝑥𝑛 ) ∈ ℕ0 )
21 nn0cn ( ( 𝐹𝑛 ) ∈ ℕ0 → ( 𝐹𝑛 ) ∈ ℂ )
22 nn0cn ( ( 𝑧𝑛 ) ∈ ℕ0 → ( 𝑧𝑛 ) ∈ ℂ )
23 nn0cn ( ( 𝑥𝑛 ) ∈ ℕ0 → ( 𝑥𝑛 ) ∈ ℂ )
24 subsub23 ( ( ( 𝐹𝑛 ) ∈ ℂ ∧ ( 𝑧𝑛 ) ∈ ℂ ∧ ( 𝑥𝑛 ) ∈ ℂ ) → ( ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) = ( 𝑥𝑛 ) ↔ ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) = ( 𝑧𝑛 ) ) )
25 21 22 23 24 syl3an ( ( ( 𝐹𝑛 ) ∈ ℕ0 ∧ ( 𝑧𝑛 ) ∈ ℕ0 ∧ ( 𝑥𝑛 ) ∈ ℕ0 ) → ( ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) = ( 𝑥𝑛 ) ↔ ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) = ( 𝑧𝑛 ) ) )
26 8 15 20 25 syl3anc ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) = ( 𝑥𝑛 ) ↔ ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) = ( 𝑧𝑛 ) ) )
27 eqcom ( ( 𝑥𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) ↔ ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) = ( 𝑥𝑛 ) )
28 eqcom ( ( 𝑧𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) ↔ ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) = ( 𝑧𝑛 ) )
29 26 27 28 3bitr4g ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝑥𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) ↔ ( 𝑧𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) ) )
30 6 ffnd ( 𝐹𝐷𝐹 Fn 𝐼 )
31 30 adantr ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝐹 Fn 𝐼 )
32 13 ffnd ( ( 𝐹𝐷𝑧𝑆 ) → 𝑧 Fn 𝐼 )
33 32 adantrl ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑧 Fn 𝐼 )
34 19 ffnd ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝑥 Fn 𝐼 )
35 16 34 fndmexd ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → 𝐼 ∈ V )
36 inidm ( 𝐼𝐼 ) = 𝐼
37 eqidd ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝐹𝑛 ) = ( 𝐹𝑛 ) )
38 eqidd ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝑧𝑛 ) = ( 𝑧𝑛 ) )
39 31 33 35 35 36 37 38 ofval ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝐹f𝑧 ) ‘ 𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) )
40 39 eqeq2d ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ↔ ( 𝑥𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑧𝑛 ) ) ) )
41 eqidd ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( 𝑥𝑛 ) = ( 𝑥𝑛 ) )
42 31 34 35 35 36 37 41 ofval ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝐹f𝑥 ) ‘ 𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) )
43 42 eqeq2d ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ↔ ( 𝑧𝑛 ) = ( ( 𝐹𝑛 ) − ( 𝑥𝑛 ) ) ) )
44 29 40 43 3bitr4d ( ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) ∧ 𝑛𝐼 ) → ( ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ↔ ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ) )
45 44 ralbidva ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( ∀ 𝑛𝐼 ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ↔ ∀ 𝑛𝐼 ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ) )
46 5 adantrl ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑧 ) ∈ 𝑆 )
47 9 46 sselid ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑧 ) ∈ 𝐷 )
48 1 psrbagf ( ( 𝐹f𝑧 ) ∈ 𝐷 → ( 𝐹f𝑧 ) : 𝐼 ⟶ ℕ0 )
49 47 48 syl ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑧 ) : 𝐼 ⟶ ℕ0 )
50 49 ffnd ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑧 ) Fn 𝐼 )
51 eqfnfv ( ( 𝑥 Fn 𝐼 ∧ ( 𝐹f𝑧 ) Fn 𝐼 ) → ( 𝑥 = ( 𝐹f𝑧 ) ↔ ∀ 𝑛𝐼 ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ) )
52 34 50 51 syl2anc ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝑥 = ( 𝐹f𝑧 ) ↔ ∀ 𝑛𝐼 ( 𝑥𝑛 ) = ( ( 𝐹f𝑧 ) ‘ 𝑛 ) ) )
53 9 4 sselid ( ( 𝐹𝐷𝑥𝑆 ) → ( 𝐹f𝑥 ) ∈ 𝐷 )
54 1 psrbagf ( ( 𝐹f𝑥 ) ∈ 𝐷 → ( 𝐹f𝑥 ) : 𝐼 ⟶ ℕ0 )
55 53 54 syl ( ( 𝐹𝐷𝑥𝑆 ) → ( 𝐹f𝑥 ) : 𝐼 ⟶ ℕ0 )
56 55 ffnd ( ( 𝐹𝐷𝑥𝑆 ) → ( 𝐹f𝑥 ) Fn 𝐼 )
57 56 adantrr ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝐹f𝑥 ) Fn 𝐼 )
58 eqfnfv ( ( 𝑧 Fn 𝐼 ∧ ( 𝐹f𝑥 ) Fn 𝐼 ) → ( 𝑧 = ( 𝐹f𝑥 ) ↔ ∀ 𝑛𝐼 ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ) )
59 33 57 58 syl2anc ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝑧 = ( 𝐹f𝑥 ) ↔ ∀ 𝑛𝐼 ( 𝑧𝑛 ) = ( ( 𝐹f𝑥 ) ‘ 𝑛 ) ) )
60 45 52 59 3bitr4d ( ( 𝐹𝐷 ∧ ( 𝑥𝑆𝑧𝑆 ) ) → ( 𝑥 = ( 𝐹f𝑧 ) ↔ 𝑧 = ( 𝐹f𝑥 ) ) )
61 3 4 5 60 f1o2d ( 𝐹𝐷 → ( 𝑥𝑆 ↦ ( 𝐹f𝑥 ) ) : 𝑆1-1-onto𝑆 )