| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. 2
⊢ (𝑥 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑥)) = (𝑥 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑥)) |
| 2 | | psrbag.d |
. . 3
⊢ 𝐷 = {𝑓 ∈ (ℕ0
↑m 𝐼)
∣ (◡𝑓 “ ℕ) ∈
Fin} |
| 3 | | psrbagconf1o.s |
. . 3
⊢ 𝑆 = {𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝐹} |
| 4 | 2, 3 | psrbagconcl 21947 |
. 2
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑥 ∈ 𝑆) → (𝐹 ∘f − 𝑥) ∈ 𝑆) |
| 5 | 2, 3 | psrbagconcl 21947 |
. 2
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑧 ∈ 𝑆) → (𝐹 ∘f − 𝑧) ∈ 𝑆) |
| 6 | 2 | psrbagf 21938 |
. . . . . . . . 9
⊢ (𝐹 ∈ 𝐷 → 𝐹:𝐼⟶ℕ0) |
| 7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝐹:𝐼⟶ℕ0) |
| 8 | 7 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝐹‘𝑛) ∈
ℕ0) |
| 9 | 3 | ssrab3 4082 |
. . . . . . . . . . . 12
⊢ 𝑆 ⊆ 𝐷 |
| 10 | 9 | sseli 3979 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ 𝐷) |
| 11 | 10 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝐷) |
| 12 | 2 | psrbagf 21938 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝐷 → 𝑧:𝐼⟶ℕ0) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑧 ∈ 𝑆) → 𝑧:𝐼⟶ℕ0) |
| 14 | 13 | adantrl 716 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧:𝐼⟶ℕ0) |
| 15 | 14 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝑧‘𝑛) ∈
ℕ0) |
| 16 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑥 ∈ 𝑆) |
| 17 | 9, 16 | sselid 3981 |
. . . . . . . . 9
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑥 ∈ 𝐷) |
| 18 | 2 | psrbagf 21938 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → 𝑥:𝐼⟶ℕ0) |
| 19 | 17, 18 | syl 17 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑥:𝐼⟶ℕ0) |
| 20 | 19 | ffvelcdmda 7104 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝑥‘𝑛) ∈
ℕ0) |
| 21 | | nn0cn 12536 |
. . . . . . . 8
⊢ ((𝐹‘𝑛) ∈ ℕ0 → (𝐹‘𝑛) ∈ ℂ) |
| 22 | | nn0cn 12536 |
. . . . . . . 8
⊢ ((𝑧‘𝑛) ∈ ℕ0 → (𝑧‘𝑛) ∈ ℂ) |
| 23 | | nn0cn 12536 |
. . . . . . . 8
⊢ ((𝑥‘𝑛) ∈ ℕ0 → (𝑥‘𝑛) ∈ ℂ) |
| 24 | | subsub23 11513 |
. . . . . . . 8
⊢ (((𝐹‘𝑛) ∈ ℂ ∧ (𝑧‘𝑛) ∈ ℂ ∧ (𝑥‘𝑛) ∈ ℂ) → (((𝐹‘𝑛) − (𝑧‘𝑛)) = (𝑥‘𝑛) ↔ ((𝐹‘𝑛) − (𝑥‘𝑛)) = (𝑧‘𝑛))) |
| 25 | 21, 22, 23, 24 | syl3an 1161 |
. . . . . . 7
⊢ (((𝐹‘𝑛) ∈ ℕ0 ∧ (𝑧‘𝑛) ∈ ℕ0 ∧ (𝑥‘𝑛) ∈ ℕ0) → (((𝐹‘𝑛) − (𝑧‘𝑛)) = (𝑥‘𝑛) ↔ ((𝐹‘𝑛) − (𝑥‘𝑛)) = (𝑧‘𝑛))) |
| 26 | 8, 15, 20, 25 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (((𝐹‘𝑛) − (𝑧‘𝑛)) = (𝑥‘𝑛) ↔ ((𝐹‘𝑛) − (𝑥‘𝑛)) = (𝑧‘𝑛))) |
| 27 | | eqcom 2744 |
. . . . . 6
⊢ ((𝑥‘𝑛) = ((𝐹‘𝑛) − (𝑧‘𝑛)) ↔ ((𝐹‘𝑛) − (𝑧‘𝑛)) = (𝑥‘𝑛)) |
| 28 | | eqcom 2744 |
. . . . . 6
⊢ ((𝑧‘𝑛) = ((𝐹‘𝑛) − (𝑥‘𝑛)) ↔ ((𝐹‘𝑛) − (𝑥‘𝑛)) = (𝑧‘𝑛)) |
| 29 | 26, 27, 28 | 3bitr4g 314 |
. . . . 5
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) = ((𝐹‘𝑛) − (𝑧‘𝑛)) ↔ (𝑧‘𝑛) = ((𝐹‘𝑛) − (𝑥‘𝑛)))) |
| 30 | 6 | ffnd 6737 |
. . . . . . . 8
⊢ (𝐹 ∈ 𝐷 → 𝐹 Fn 𝐼) |
| 31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝐹 Fn 𝐼) |
| 32 | 13 | ffnd 6737 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑧 ∈ 𝑆) → 𝑧 Fn 𝐼) |
| 33 | 32 | adantrl 716 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑧 Fn 𝐼) |
| 34 | 19 | ffnd 6737 |
. . . . . . . 8
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝑥 Fn 𝐼) |
| 35 | 16, 34 | fndmexd 7926 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → 𝐼 ∈ V) |
| 36 | | inidm 4227 |
. . . . . . 7
⊢ (𝐼 ∩ 𝐼) = 𝐼 |
| 37 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝐹‘𝑛) = (𝐹‘𝑛)) |
| 38 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝑧‘𝑛) = (𝑧‘𝑛)) |
| 39 | 31, 33, 35, 35, 36, 37, 38 | ofval 7708 |
. . . . . 6
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝐹 ∘f − 𝑧)‘𝑛) = ((𝐹‘𝑛) − (𝑧‘𝑛))) |
| 40 | 39 | eqeq2d 2748 |
. . . . 5
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) = ((𝐹 ∘f − 𝑧)‘𝑛) ↔ (𝑥‘𝑛) = ((𝐹‘𝑛) − (𝑧‘𝑛)))) |
| 41 | | eqidd 2738 |
. . . . . . 7
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → (𝑥‘𝑛) = (𝑥‘𝑛)) |
| 42 | 31, 34, 35, 35, 36, 37, 41 | ofval 7708 |
. . . . . 6
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝐹 ∘f − 𝑥)‘𝑛) = ((𝐹‘𝑛) − (𝑥‘𝑛))) |
| 43 | 42 | eqeq2d 2748 |
. . . . 5
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝑧‘𝑛) = ((𝐹 ∘f − 𝑥)‘𝑛) ↔ (𝑧‘𝑛) = ((𝐹‘𝑛) − (𝑥‘𝑛)))) |
| 44 | 29, 40, 43 | 3bitr4d 311 |
. . . 4
⊢ (((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) ∧ 𝑛 ∈ 𝐼) → ((𝑥‘𝑛) = ((𝐹 ∘f − 𝑧)‘𝑛) ↔ (𝑧‘𝑛) = ((𝐹 ∘f − 𝑥)‘𝑛))) |
| 45 | 44 | ralbidva 3176 |
. . 3
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (∀𝑛 ∈ 𝐼 (𝑥‘𝑛) = ((𝐹 ∘f − 𝑧)‘𝑛) ↔ ∀𝑛 ∈ 𝐼 (𝑧‘𝑛) = ((𝐹 ∘f − 𝑥)‘𝑛))) |
| 46 | 5 | adantrl 716 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘f − 𝑧) ∈ 𝑆) |
| 47 | 9, 46 | sselid 3981 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘f − 𝑧) ∈ 𝐷) |
| 48 | 2 | psrbagf 21938 |
. . . . . 6
⊢ ((𝐹 ∘f −
𝑧) ∈ 𝐷 → (𝐹 ∘f − 𝑧):𝐼⟶ℕ0) |
| 49 | 47, 48 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘f − 𝑧):𝐼⟶ℕ0) |
| 50 | 49 | ffnd 6737 |
. . . 4
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘f − 𝑧) Fn 𝐼) |
| 51 | | eqfnfv 7051 |
. . . 4
⊢ ((𝑥 Fn 𝐼 ∧ (𝐹 ∘f − 𝑧) Fn 𝐼) → (𝑥 = (𝐹 ∘f − 𝑧) ↔ ∀𝑛 ∈ 𝐼 (𝑥‘𝑛) = ((𝐹 ∘f − 𝑧)‘𝑛))) |
| 52 | 34, 50, 51 | syl2anc 584 |
. . 3
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥 = (𝐹 ∘f − 𝑧) ↔ ∀𝑛 ∈ 𝐼 (𝑥‘𝑛) = ((𝐹 ∘f − 𝑧)‘𝑛))) |
| 53 | 9, 4 | sselid 3981 |
. . . . . . 7
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑥 ∈ 𝑆) → (𝐹 ∘f − 𝑥) ∈ 𝐷) |
| 54 | 2 | psrbagf 21938 |
. . . . . . 7
⊢ ((𝐹 ∘f −
𝑥) ∈ 𝐷 → (𝐹 ∘f − 𝑥):𝐼⟶ℕ0) |
| 55 | 53, 54 | syl 17 |
. . . . . 6
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑥 ∈ 𝑆) → (𝐹 ∘f − 𝑥):𝐼⟶ℕ0) |
| 56 | 55 | ffnd 6737 |
. . . . 5
⊢ ((𝐹 ∈ 𝐷 ∧ 𝑥 ∈ 𝑆) → (𝐹 ∘f − 𝑥) Fn 𝐼) |
| 57 | 56 | adantrr 717 |
. . . 4
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝐹 ∘f − 𝑥) Fn 𝐼) |
| 58 | | eqfnfv 7051 |
. . . 4
⊢ ((𝑧 Fn 𝐼 ∧ (𝐹 ∘f − 𝑥) Fn 𝐼) → (𝑧 = (𝐹 ∘f − 𝑥) ↔ ∀𝑛 ∈ 𝐼 (𝑧‘𝑛) = ((𝐹 ∘f − 𝑥)‘𝑛))) |
| 59 | 33, 57, 58 | syl2anc 584 |
. . 3
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑧 = (𝐹 ∘f − 𝑥) ↔ ∀𝑛 ∈ 𝐼 (𝑧‘𝑛) = ((𝐹 ∘f − 𝑥)‘𝑛))) |
| 60 | 45, 52, 59 | 3bitr4d 311 |
. 2
⊢ ((𝐹 ∈ 𝐷 ∧ (𝑥 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥 = (𝐹 ∘f − 𝑧) ↔ 𝑧 = (𝐹 ∘f − 𝑥))) |
| 61 | 1, 4, 5, 60 | f1o2d 7687 |
1
⊢ (𝐹 ∈ 𝐷 → (𝑥 ∈ 𝑆 ↦ (𝐹 ∘f − 𝑥)):𝑆–1-1-onto→𝑆) |