Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. 2
⊢ (𝑥 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑥)) = (𝑥 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑥)) |
2 | | simpll 790 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → 𝐼 ∈ 𝑉) |
3 | | simplr 792 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → 𝐹 ∈ 𝐷) |
4 | | simpr 477 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
5 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝑦 ∘𝑟 ≤ 𝐹 ↔ 𝑥 ∘𝑟 ≤ 𝐹)) |
6 | | psrbagconf1o.1 |
. . . . . . . 8
⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} |
7 | 5, 6 | elrab2 3366 |
. . . . . . 7
⊢ (𝑥 ∈ 𝑆 ↔ (𝑥 ∈ 𝐷 ∧ 𝑥 ∘𝑟 ≤ 𝐹)) |
8 | 4, 7 | sylib 208 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → (𝑥 ∈ 𝐷 ∧ 𝑥 ∘𝑟 ≤ 𝐹)) |
9 | 8 | simpld 475 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐷) |
10 | | psrbag.d |
. . . . . 6
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡𝑓 “ ℕ) ∈
Fin} |
11 | 10 | psrbagf 19365 |
. . . . 5
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑥 ∈ 𝐷) → 𝑥:𝐼⟶ℕ0) |
12 | 2, 9, 11 | syl2anc 693 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → 𝑥:𝐼⟶ℕ0) |
13 | 8 | simprd 479 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∘𝑟 ≤ 𝐹) |
14 | 10 | psrbagcon 19371 |
. . . 4
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∈ 𝐷 ∧ 𝑥:𝐼⟶ℕ0 ∧ 𝑥 ∘𝑟
≤ 𝐹)) → ((𝐹 ∘𝑓
− 𝑥) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝑥) ∘𝑟
≤ 𝐹)) |
15 | 2, 3, 12, 13, 14 | syl13anc 1328 |
. . 3
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → ((𝐹 ∘𝑓 − 𝑥) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝑥) ∘𝑟
≤ 𝐹)) |
16 | | breq1 4656 |
. . . 4
⊢ (𝑦 = (𝐹 ∘𝑓 − 𝑥) → (𝑦 ∘𝑟 ≤ 𝐹 ↔ (𝐹 ∘𝑓 − 𝑥) ∘𝑟
≤ 𝐹)) |
17 | 16, 6 | elrab2 3366 |
. . 3
⊢ ((𝐹 ∘𝑓
− 𝑥) ∈ 𝑆 ↔ ((𝐹 ∘𝑓 − 𝑥) ∈ 𝐷 ∧ (𝐹 ∘𝑓 − 𝑥) ∘𝑟
≤ 𝐹)) |
18 | 15, 17 | sylibr 224 |
. 2
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑥 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑥) ∈ 𝑆) |
19 | 18 | ralrimiva 2966 |
. . 3
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → ∀𝑥 ∈ 𝑆 (𝐹 ∘𝑓 − 𝑥) ∈ 𝑆) |
20 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝑧 → (𝐹 ∘𝑓 − 𝑥) = (𝐹 ∘𝑓 − 𝑧)) |
21 | 20 | eleq1d 2686 |
. . . 4
⊢ (𝑥 = 𝑧 → ((𝐹 ∘𝑓 − 𝑥) ∈ 𝑆 ↔ (𝐹 ∘𝑓 − 𝑧) ∈ 𝑆)) |
22 | 21 | rspccva 3308 |
. . 3
⊢
((∀𝑥 ∈
𝑆 (𝐹 ∘𝑓 − 𝑥) ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑧) ∈ 𝑆) |
23 | 19, 22 | sylan 488 |
. 2
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ 𝑧 ∈ 𝑆) → (𝐹 ∘𝑓 − 𝑧) ∈ 𝑆) |
24 | 10 | psrbagf 19365 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → 𝐹:𝐼⟶ℕ0) |
25 | 24 | adantr 481 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝐹:𝐼⟶ℕ0) |
26 | 25 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝐹‘𝑛) ∈
ℕ0) |
27 | | simpll 790 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝐼 ∈ 𝑉) |
28 | | ssrab2 3687 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ 𝐷 ∣ 𝑦 ∘𝑟 ≤ 𝐹} ⊆ 𝐷 |
29 | 6, 28 | eqsstri 3635 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ 𝐷 |
30 | | simprr 796 |
. . . . . . . . . 10
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ 𝑆) |
31 | 29, 30 | sseldi 3601 |
. . . . . . . . 9
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 ∈ 𝐷) |
32 | 10 | psrbagf 19365 |
. . . . . . . . 9
⊢ ((𝐼 ∈ 𝑉 ∧ 𝑧 ∈ 𝐷) → 𝑧:𝐼⟶ℕ0) |
33 | 27, 31, 32 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧:𝐼⟶ℕ0) |
34 | 33 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝑧‘𝑛) ∈
ℕ0) |
35 | 12 | adantrr 753 |
. . . . . . . 8
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑥:𝐼⟶ℕ0) |
36 | 35 | ffvelrnda 6359 |
. . . . . . 7
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝑥‘𝑛) ∈
ℕ0) |
37 | | nn0cn 11302 |
. . . . . . . 8
⊢ ((𝐹‘𝑛) ∈ ℕ0 → (𝐹‘𝑛) ∈ ℂ) |
38 | | nn0cn 11302 |
. . . . . . . 8
⊢ ((𝑧‘𝑛) ∈ ℕ0 → (𝑧‘𝑛) ∈ ℂ) |
39 | | nn0cn 11302 |
. . . . . . . 8
⊢ ((𝑥‘𝑛) ∈ ℕ0 → (𝑥‘𝑛) ∈ ℂ) |
40 | | subsub23 10286 |
. . . . . . . 8
⊢ (((𝐹‘𝑛) ∈ ℂ ∧ (𝑧‘𝑛) ∈ ℂ ∧ (𝑥‘𝑛) ∈ ℂ) → (((𝐹‘𝑛) − (𝑧‘𝑛)) = (𝑥‘𝑛) ↔ ((𝐹‘𝑛) − (𝑥‘𝑛)) = (𝑧‘𝑛))) |
41 | 37, 38, 39, 40 | syl3an 1368 |
. . . . . . 7
⊢ (((𝐹‘𝑛) ∈ ℕ0 ∧ (𝑧‘𝑛) ∈ ℕ0 ∧ (𝑥‘𝑛) ∈ ℕ0) → (((𝐹‘𝑛) − (𝑧‘𝑛)) = (𝑥‘𝑛) ↔ ((𝐹‘𝑛) − (𝑥‘𝑛)) = (𝑧‘𝑛))) |
42 | 26, 34, 36, 41 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (((𝐹‘𝑛) − (𝑧‘𝑛)) = (𝑥‘𝑛) ↔ ((𝐹‘𝑛) − (𝑥‘𝑛)) = (𝑧‘𝑛))) |
43 | | eqcom 2629 |
. . . . . 6
⊢ ((𝑥‘𝑛) = ((𝐹‘𝑛) − (𝑧‘𝑛)) ↔ ((𝐹‘𝑛) − (𝑧‘𝑛)) = (𝑥‘𝑛)) |
44 | | eqcom 2629 |
. . . . . 6
⊢ ((𝑧‘𝑛) = ((𝐹‘𝑛) − (𝑥‘𝑛)) ↔ ((𝐹‘𝑛) − (𝑥‘𝑛)) = (𝑧‘𝑛)) |
45 | 42, 43, 44 | 3bitr4g 303 |
. . . . 5
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) = ((𝐹‘𝑛) − (𝑧‘𝑛)) ↔ (𝑧‘𝑛) = ((𝐹‘𝑛) − (𝑥‘𝑛)))) |
46 | | ffn 6045 |
. . . . . . . 8
⊢ (𝐹:𝐼⟶ℕ0 → 𝐹 Fn 𝐼) |
47 | 25, 46 | syl 17 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝐹 Fn 𝐼) |
48 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑧:𝐼⟶ℕ0 → 𝑧 Fn 𝐼) |
49 | 33, 48 | syl 17 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 Fn 𝐼) |
50 | | inidm 3822 |
. . . . . . 7
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
51 | | eqidd 2623 |
. . . . . . 7
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝐹‘𝑛) = (𝐹‘𝑛)) |
52 | | eqidd 2623 |
. . . . . . 7
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝑧‘𝑛) = (𝑧‘𝑛)) |
53 | 47, 49, 27, 27, 50, 51, 52 | ofval 6906 |
. . . . . 6
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝐹 ∘𝑓 − 𝑧)‘𝑛) = ((𝐹‘𝑛) − (𝑧‘𝑛))) |
54 | 53 | eqeq2d 2632 |
. . . . 5
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) = ((𝐹 ∘𝑓 − 𝑧)‘𝑛) ↔ (𝑥‘𝑛) = ((𝐹‘𝑛) − (𝑧‘𝑛)))) |
55 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑥:𝐼⟶ℕ0 → 𝑥 Fn 𝐼) |
56 | 35, 55 | syl 17 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑥 Fn 𝐼) |
57 | | eqidd 2623 |
. . . . . . 7
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝑥‘𝑛) = (𝑥‘𝑛)) |
58 | 47, 56, 27, 27, 50, 51, 57 | ofval 6906 |
. . . . . 6
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝐹 ∘𝑓 − 𝑥)‘𝑛) = ((𝐹‘𝑛) − (𝑥‘𝑛))) |
59 | 58 | eqeq2d 2632 |
. . . . 5
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝑧‘𝑛) = ((𝐹 ∘𝑓 − 𝑥)‘𝑛) ↔ (𝑧‘𝑛) = ((𝐹‘𝑛) − (𝑥‘𝑛)))) |
60 | 45, 54, 59 | 3bitr4d 300 |
. . . 4
⊢ ((((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) = ((𝐹 ∘𝑓 − 𝑧)‘𝑛) ↔ (𝑧‘𝑛) = ((𝐹 ∘𝑓 − 𝑥)‘𝑛))) |
61 | 60 | ralbidva 2985 |
. . 3
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (∀𝑛 ∈ 𝐼 (𝑥‘𝑛) = ((𝐹 ∘𝑓 − 𝑧)‘𝑛) ↔ ∀𝑛 ∈ 𝐼 (𝑧‘𝑛) = ((𝐹 ∘𝑓 − 𝑥)‘𝑛))) |
62 | 23 | adantrl 752 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘𝑓 − 𝑧) ∈ 𝑆) |
63 | 29, 62 | sseldi 3601 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘𝑓 − 𝑧) ∈ 𝐷) |
64 | 10 | psrbagf 19365 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘𝑓 − 𝑧) ∈ 𝐷) → (𝐹 ∘𝑓 − 𝑧):𝐼⟶ℕ0) |
65 | 27, 63, 64 | syl2anc 693 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘𝑓 − 𝑧):𝐼⟶ℕ0) |
66 | | ffn 6045 |
. . . . 5
⊢ ((𝐹 ∘𝑓
− 𝑧):𝐼⟶ℕ0
→ (𝐹
∘𝑓 − 𝑧) Fn 𝐼) |
67 | 65, 66 | syl 17 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘𝑓 − 𝑧) Fn 𝐼) |
68 | | eqfnfv 6311 |
. . . 4
⊢ ((𝑥 Fn 𝐼 ∧ (𝐹 ∘𝑓 − 𝑧) Fn 𝐼) → (𝑥 = (𝐹 ∘𝑓 − 𝑧) ↔ ∀𝑛 ∈ 𝐼 (𝑥‘𝑛) = ((𝐹 ∘𝑓 − 𝑧)‘𝑛))) |
69 | 56, 67, 68 | syl2anc 693 |
. . 3
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥 = (𝐹 ∘𝑓 − 𝑧) ↔ ∀𝑛 ∈ 𝐼 (𝑥‘𝑛) = ((𝐹 ∘𝑓 − 𝑧)‘𝑛))) |
70 | 18 | adantrr 753 |
. . . . . . 7
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘𝑓 − 𝑥) ∈ 𝑆) |
71 | 29, 70 | sseldi 3601 |
. . . . . 6
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘𝑓 − 𝑥) ∈ 𝐷) |
72 | 10 | psrbagf 19365 |
. . . . . 6
⊢ ((𝐼 ∈ 𝑉 ∧ (𝐹 ∘𝑓 − 𝑥) ∈ 𝐷) → (𝐹 ∘𝑓 − 𝑥):𝐼⟶ℕ0) |
73 | 27, 71, 72 | syl2anc 693 |
. . . . 5
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘𝑓 − 𝑥):𝐼⟶ℕ0) |
74 | | ffn 6045 |
. . . . 5
⊢ ((𝐹 ∘𝑓
− 𝑥):𝐼⟶ℕ0
→ (𝐹
∘𝑓 − 𝑥) Fn 𝐼) |
75 | 73, 74 | syl 17 |
. . . 4
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘𝑓 − 𝑥) Fn 𝐼) |
76 | | eqfnfv 6311 |
. . . 4
⊢ ((𝑧 Fn 𝐼 ∧ (𝐹 ∘𝑓 − 𝑥) Fn 𝐼) → (𝑧 = (𝐹 ∘𝑓 − 𝑥) ↔ ∀𝑛 ∈ 𝐼 (𝑧‘𝑛) = ((𝐹 ∘𝑓 − 𝑥)‘𝑛))) |
77 | 49, 75, 76 | syl2anc 693 |
. . 3
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑧 = (𝐹 ∘𝑓 − 𝑥) ↔ ∀𝑛 ∈ 𝐼 (𝑧‘𝑛) = ((𝐹 ∘𝑓 − 𝑥)‘𝑛))) |
78 | 61, 69, 77 | 3bitr4d 300 |
. 2
⊢ (((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥 = (𝐹 ∘𝑓 − 𝑧) ↔ 𝑧 = (𝐹 ∘𝑓 − 𝑥))) |
79 | 1, 18, 23, 78 | f1o2d 6887 |
1
⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝐷) → (𝑥 ∈ 𝑆 ↦ (𝐹 ∘𝑓 − 𝑥)):𝑆–1-1-onto→𝑆) |