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

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ 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 sseldi ⊢ ( ( 𝐹 ∈ 𝐷 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑥 ∈ 𝐷 )
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 sseldi ⊢ ( ( 𝐹 ∈ 𝐷 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐹 ∘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 sseldi ⊢ ( ( 𝐹 ∈ 𝐷 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐹 ∘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→ 𝑆 )