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)

Ref Expression
Hypotheses psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
psrbagconf1o.1 ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹 }
Assertion psrbagconf1o ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝐹 ∘f − 𝑥 ) ) : 𝑆 –1-1-onto→ 𝑆 )

Proof

Step Hyp Ref Expression
1 psrbag.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.1 ⊢ 𝑆 = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘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 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
12 4 10 11 syl2anc ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 : 𝐼 ⟶ ℕ0 )
13 9 simprd ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∘r ≤ 𝐹 )
14 1 psrbagcon ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∈ 𝐷 ∧ 𝑥 : 𝐼 ⟶ ℕ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 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
25 24 adantr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝐹 : 𝐼 ⟶ ℕ0 )
26 25 ffvelrnda ⊢ ( ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℕ0 )
27 simpll ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝐼 ∈ 𝑉 )
28 2 ssrab3 ⊢ 𝑆 ⊆ 𝐷
29 simprr ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ 𝑆 )
30 28 29 sseldi ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → 𝑧 ∈ 𝐷 )
31 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐷 ) → 𝑧 : 𝐼 ⟶ ℕ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 sseldi ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐹 ∘f − 𝑧 ) ∈ 𝐷 )
60 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘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 sseldi ⊢ ( ( ( 𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷 ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ) → ( 𝐹 ∘f − 𝑥 ) ∈ 𝐷 )
67 1 psrbagf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝐹 ∘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→ 𝑆 )