| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢ (𝐴 ↑m (0..^𝑆)) = (𝐴 ↑m (0..^𝑆)) |
| 2 | | eqid 2737 |
. . . . 5
⊢ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) = (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) |
| 3 | | ovexd 7466 |
. . . . 5
⊢ (𝜑 → (0..^𝑆) ∈ V) |
| 4 | | nnex 12272 |
. . . . . . 7
⊢ ℕ
∈ V |
| 5 | 4 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℕ ∈
V) |
| 6 | | reprpmtf1o.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
| 7 | 5, 6 | ssexd 5324 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ V) |
| 8 | | reprpmtf1o.x |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ (0..^𝑆)) |
| 9 | | reprpmtf1o.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ ℕ) |
| 10 | | lbfzo0 13739 |
. . . . . . 7
⊢ (0 ∈
(0..^𝑆) ↔ 𝑆 ∈
ℕ) |
| 11 | 9, 10 | sylibr 234 |
. . . . . 6
⊢ (𝜑 → 0 ∈ (0..^𝑆)) |
| 12 | | reprpmtf1o.t |
. . . . . 6
⊢ 𝑇 = if(𝑋 = 0, ( I ↾ (0..^𝑆)), ((pmTrsp‘(0..^𝑆))‘{𝑋, 0})) |
| 13 | 3, 8, 11, 12 | pmtridf1o 33114 |
. . . . 5
⊢ (𝜑 → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆)) |
| 14 | 1, 1, 2, 3, 3, 7, 13 | fmptco1f1o 32643 |
. . . 4
⊢ (𝜑 → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1-onto→(𝐴 ↑m (0..^𝑆))) |
| 15 | | f1of1 6847 |
. . . 4
⊢ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1-onto→(𝐴 ↑m (0..^𝑆)) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1→(𝐴 ↑m (0..^𝑆))) |
| 16 | 14, 15 | syl 17 |
. . 3
⊢ (𝜑 → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1→(𝐴 ↑m (0..^𝑆))) |
| 17 | | ssrab2 4080 |
. . . . . 6
⊢ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} ⊆ (𝐴 ↑m (0..^𝑆)) |
| 18 | | reprpmtf1o.p |
. . . . . . . . . 10
⊢ 𝑃 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘𝑋) ∈ 𝐵} |
| 19 | 18 | ssrab3 4082 |
. . . . . . . . 9
⊢ 𝑃 ⊆ (𝐴(repr‘𝑆)𝑀) |
| 20 | 19 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑃 ⊆ (𝐴(repr‘𝑆)𝑀)) |
| 21 | | reprpmtf1o.m |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 22 | 9 | nnnn0d 12587 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
| 23 | 6, 21, 22 | reprval 34625 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 24 | 20, 23 | sseqtrd 4020 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ⊆ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 25 | 24 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 26 | 17, 25 | sselid 3981 |
. . . . 5
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) |
| 27 | 26 | ex 412 |
. . . 4
⊢ (𝜑 → (𝑐 ∈ 𝑃 → 𝑐 ∈ (𝐴 ↑m (0..^𝑆)))) |
| 28 | 27 | ssrdv 3989 |
. . 3
⊢ (𝜑 → 𝑃 ⊆ (𝐴 ↑m (0..^𝑆))) |
| 29 | | f1ores 6862 |
. . 3
⊢ (((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1→(𝐴 ↑m (0..^𝑆)) ∧ 𝑃 ⊆ (𝐴 ↑m (0..^𝑆))) → ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) ↾ 𝑃):𝑃–1-1-onto→((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) “ 𝑃)) |
| 30 | 16, 28, 29 | syl2anc 584 |
. 2
⊢ (𝜑 → ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) ↾ 𝑃):𝑃–1-1-onto→((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) “ 𝑃)) |
| 31 | | resmpt 6055 |
. . . . 5
⊢ (𝑃 ⊆ (𝐴 ↑m (0..^𝑆)) → ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) ↾ 𝑃) = (𝑐 ∈ 𝑃 ↦ (𝑐 ∘ 𝑇))) |
| 32 | 28, 31 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) ↾ 𝑃) = (𝑐 ∈ 𝑃 ↦ (𝑐 ∘ 𝑇))) |
| 33 | | reprpmtf1o.f |
. . . 4
⊢ 𝐹 = (𝑐 ∈ 𝑃 ↦ (𝑐 ∘ 𝑇)) |
| 34 | 32, 33 | eqtr4di 2795 |
. . 3
⊢ (𝜑 → ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) ↾ 𝑃) = 𝐹) |
| 35 | | eqidd 2738 |
. . 3
⊢ (𝜑 → 𝑃 = 𝑃) |
| 36 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑑 ∈ V |
| 37 | 36 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝑑 ∈ V) |
| 38 | 2, 37, 28 | elimampt 6061 |
. . . . . . 7
⊢ (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) “ 𝑃) ↔ ∃𝑐 ∈ 𝑃 𝑑 = (𝑐 ∘ 𝑇))) |
| 39 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → 𝑑 = (𝑐 ∘ 𝑇)) |
| 40 | | f1of 6848 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))–1-1-onto→(𝐴 ↑m (0..^𝑆)) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))⟶(𝐴 ↑m (0..^𝑆))) |
| 41 | 14, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))⟶(𝐴 ↑m (0..^𝑆))) |
| 42 | 41 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))⟶(𝐴 ↑m (0..^𝑆))) |
| 43 | 2 | fmpt 7130 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑐 ∈
(𝐴 ↑m
(0..^𝑆))(𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)):(𝐴 ↑m (0..^𝑆))⟶(𝐴 ↑m (0..^𝑆))) |
| 44 | 42, 43 | sylibr 234 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → ∀𝑐 ∈ (𝐴 ↑m (0..^𝑆))(𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆))) |
| 45 | 26 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) |
| 46 | | rspa 3248 |
. . . . . . . . . . . . . 14
⊢
((∀𝑐 ∈
(𝐴 ↑m
(0..^𝑆))(𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ∧ 𝑐 ∈ (𝐴 ↑m (0..^𝑆))) → (𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆))) |
| 47 | 44, 45, 46 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → (𝑐 ∘ 𝑇) ∈ (𝐴 ↑m (0..^𝑆))) |
| 48 | 39, 47 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → 𝑑 ∈ (𝐴 ↑m (0..^𝑆))) |
| 49 | 39 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑑 = (𝑐 ∘ 𝑇)) |
| 50 | 49 | fveq1d 6908 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑‘𝑎) = ((𝑐 ∘ 𝑇)‘𝑎)) |
| 51 | | f1ofun 6850 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun 𝑇) |
| 52 | 13, 51 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → Fun 𝑇) |
| 53 | 52 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → Fun 𝑇) |
| 54 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
| 55 | | f1odm 6852 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom 𝑇 = (0..^𝑆)) |
| 56 | 13, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → dom 𝑇 = (0..^𝑆)) |
| 57 | 56 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → dom 𝑇 = (0..^𝑆)) |
| 58 | 54, 57 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom 𝑇) |
| 59 | | fvco 7007 |
. . . . . . . . . . . . . . . . 17
⊢ ((Fun
𝑇 ∧ 𝑎 ∈ dom 𝑇) → ((𝑐 ∘ 𝑇)‘𝑎) = (𝑐‘(𝑇‘𝑎))) |
| 60 | 53, 58, 59 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∘ 𝑇)‘𝑎) = (𝑐‘(𝑇‘𝑎))) |
| 61 | 60 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑐 ∘ 𝑇)‘𝑎) = (𝑐‘(𝑇‘𝑎))) |
| 62 | 50, 61 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑑‘𝑎) = (𝑐‘(𝑇‘𝑎))) |
| 63 | 62 | sumeq2dv 15738 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇‘𝑎))) |
| 64 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑇‘𝑎) → (𝑐‘𝑏) = (𝑐‘(𝑇‘𝑎))) |
| 65 | | fzofi 14015 |
. . . . . . . . . . . . . . . 16
⊢
(0..^𝑆) ∈
Fin |
| 66 | 65 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → (0..^𝑆) ∈ Fin) |
| 67 | 13 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆)) |
| 68 | | eqidd 2738 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑇‘𝑎) = (𝑇‘𝑎)) |
| 69 | 6 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ) |
| 70 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝐴 ⊆ ℕ) |
| 71 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑀 ∈ ℤ) |
| 72 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑆 ∈
ℕ0) |
| 73 | 20 | sselda 3983 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑐 ∈ (𝐴(repr‘𝑆)𝑀)) |
| 74 | 70, 71, 72, 73 | reprf 34627 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑐:(0..^𝑆)⟶𝐴) |
| 75 | 74 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐‘𝑏) ∈ 𝐴) |
| 76 | 69, 75 | sseldd 3984 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐‘𝑏) ∈ ℕ) |
| 77 | 76 | nncnd 12282 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑐‘𝑏) ∈ ℂ) |
| 78 | 64, 66, 67, 68, 77 | fsumf1o 15759 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐‘𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇‘𝑎))) |
| 79 | 78 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐‘𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑐‘(𝑇‘𝑎))) |
| 80 | 70, 71, 72, 73 | reprsum 34628 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → Σ𝑏 ∈ (0..^𝑆)(𝑐‘𝑏) = 𝑀) |
| 81 | 80 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → Σ𝑏 ∈ (0..^𝑆)(𝑐‘𝑏) = 𝑀) |
| 82 | 63, 79, 81 | 3eqtr2d 2783 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = 𝑀) |
| 83 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑑 → (𝑐‘𝑎) = (𝑑‘𝑎)) |
| 84 | 83 | sumeq2sdv 15739 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑑 → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎)) |
| 85 | 84 | eqeq1d 2739 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑑 → (Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = 𝑀)) |
| 86 | 85 | elrab 3692 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} ↔ (𝑑 ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)(𝑑‘𝑎) = 𝑀)) |
| 87 | 48, 82, 86 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → 𝑑 ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 88 | 23 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 89 | 87, 88 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) |
| 90 | 39 | fveq1d 6908 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → (𝑑‘0) = ((𝑐 ∘ 𝑇)‘0)) |
| 91 | 52 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → Fun 𝑇) |
| 92 | 11, 56 | eleqtrrd 2844 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 0 ∈ dom 𝑇) |
| 93 | 92 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → 0 ∈ dom 𝑇) |
| 94 | | fvco 7007 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝑇 ∧ 0 ∈ dom 𝑇) → ((𝑐 ∘ 𝑇)‘0) = (𝑐‘(𝑇‘0))) |
| 95 | 91, 93, 94 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → ((𝑐 ∘ 𝑇)‘0) = (𝑐‘(𝑇‘0))) |
| 96 | 3, 8, 11, 12 | pmtridfv2 33116 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇‘0) = 𝑋) |
| 97 | 96 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → (𝑇‘0) = 𝑋) |
| 98 | 97 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → (𝑐‘(𝑇‘0)) = (𝑐‘𝑋)) |
| 99 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑐 ∈ 𝑃) |
| 100 | 99, 18 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → 𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘𝑋) ∈ 𝐵}) |
| 101 | | rabid 3458 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘𝑋) ∈ 𝐵} ↔ (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐‘𝑋) ∈ 𝐵)) |
| 102 | 100, 101 | sylib 218 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → (𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑐‘𝑋) ∈ 𝐵)) |
| 103 | 102 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝑃) → ¬ (𝑐‘𝑋) ∈ 𝐵) |
| 104 | 103 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → ¬ (𝑐‘𝑋) ∈ 𝐵) |
| 105 | 98, 104 | eqneltrd 2861 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → ¬ (𝑐‘(𝑇‘0)) ∈ 𝐵) |
| 106 | 95, 105 | eqneltrd 2861 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → ¬ ((𝑐 ∘ 𝑇)‘0) ∈ 𝐵) |
| 107 | 90, 106 | eqneltrd 2861 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → ¬ (𝑑‘0) ∈ 𝐵) |
| 108 | 89, 107 | jca 511 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ 𝑃) ∧ 𝑑 = (𝑐 ∘ 𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) |
| 109 | 108 | r19.29an 3158 |
. . . . . . . 8
⊢ ((𝜑 ∧ ∃𝑐 ∈ 𝑃 𝑑 = (𝑐 ∘ 𝑇)) → (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) |
| 110 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝐴 ⊆ ℕ) |
| 111 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑀 ∈ ℤ) |
| 112 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑆 ∈
ℕ0) |
| 113 | | simpr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) |
| 114 | 110, 111,
112, 113 | reprf 34627 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → 𝑑:(0..^𝑆)⟶𝐴) |
| 115 | | f1ocnv 6860 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → ◡𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆)) |
| 116 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → ◡𝑇:(0..^𝑆)⟶(0..^𝑆)) |
| 117 | 13, 115, 116 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ◡𝑇:(0..^𝑆)⟶(0..^𝑆)) |
| 118 | 117 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → ◡𝑇:(0..^𝑆)⟶(0..^𝑆)) |
| 119 | | fco 6760 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑑:(0..^𝑆)⟶𝐴 ∧ ◡𝑇:(0..^𝑆)⟶(0..^𝑆)) → (𝑑 ∘ ◡𝑇):(0..^𝑆)⟶𝐴) |
| 120 | 114, 118,
119 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑 ∘ ◡𝑇):(0..^𝑆)⟶𝐴) |
| 121 | | elmapg 8879 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈ V ∧ (0..^𝑆) ∈ V) → ((𝑑 ∘ ◡𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑑 ∘ ◡𝑇):(0..^𝑆)⟶𝐴)) |
| 122 | 7, 3, 121 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑑 ∘ ◡𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑑 ∘ ◡𝑇):(0..^𝑆)⟶𝐴)) |
| 123 | 122 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → ((𝑑 ∘ ◡𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ↔ (𝑑 ∘ ◡𝑇):(0..^𝑆)⟶𝐴)) |
| 124 | 120, 123 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (𝑑 ∘ ◡𝑇) ∈ (𝐴 ↑m (0..^𝑆))) |
| 125 | 124 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑 ∘ ◡𝑇) ∈ (𝐴 ↑m (0..^𝑆))) |
| 126 | | f1ofun 6850 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (◡𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → Fun ◡𝑇) |
| 127 | 13, 115, 126 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Fun ◡𝑇) |
| 128 | 127 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → Fun ◡𝑇) |
| 129 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆)) |
| 130 | | f1odm 6852 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (◡𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → dom ◡𝑇 = (0..^𝑆)) |
| 131 | 13, 115, 130 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom ◡𝑇 = (0..^𝑆)) |
| 132 | 131 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → dom ◡𝑇 = (0..^𝑆)) |
| 133 | 129, 132 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom ◡𝑇) |
| 134 | 133 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ dom ◡𝑇) |
| 135 | | fvco 7007 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Fun
◡𝑇 ∧ 𝑎 ∈ dom ◡𝑇) → ((𝑑 ∘ ◡𝑇)‘𝑎) = (𝑑‘(◡𝑇‘𝑎))) |
| 136 | 128, 134,
135 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑑 ∘ ◡𝑇)‘𝑎) = (𝑑‘(◡𝑇‘𝑎))) |
| 137 | 136 | sumeq2dv 15738 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑 ∘ ◡𝑇)‘𝑎) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(◡𝑇‘𝑎))) |
| 138 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (◡𝑇‘𝑎) → (𝑑‘𝑏) = (𝑑‘(◡𝑇‘𝑎))) |
| 139 | 65 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → (0..^𝑆) ∈ Fin) |
| 140 | 13, 115 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ◡𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆)) |
| 141 | 140 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → ◡𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆)) |
| 142 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑎 ∈ (0..^𝑆)) → (◡𝑇‘𝑎) = (◡𝑇‘𝑎)) |
| 143 | 110 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ) |
| 144 | 114 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑‘𝑏) ∈ 𝐴) |
| 145 | 143, 144 | sseldd 3984 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑‘𝑏) ∈ ℕ) |
| 146 | 145 | nncnd 12282 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ 𝑏 ∈ (0..^𝑆)) → (𝑑‘𝑏) ∈ ℂ) |
| 147 | 138, 139,
141, 142, 146 | fsumf1o 15759 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑‘𝑏) = Σ𝑎 ∈ (0..^𝑆)(𝑑‘(◡𝑇‘𝑎))) |
| 148 | 110, 111,
112, 113 | reprsum 34628 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑏 ∈ (0..^𝑆)(𝑑‘𝑏) = 𝑀) |
| 149 | 137, 147,
148 | 3eqtr2d 2783 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) → Σ𝑎 ∈ (0..^𝑆)((𝑑 ∘ ◡𝑇)‘𝑎) = 𝑀) |
| 150 | 149 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Σ𝑎 ∈ (0..^𝑆)((𝑑 ∘ ◡𝑇)‘𝑎) = 𝑀) |
| 151 | | fveq1 6905 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑐 = (𝑑 ∘ ◡𝑇) → (𝑐‘𝑎) = ((𝑑 ∘ ◡𝑇)‘𝑎)) |
| 152 | 151 | sumeq2sdv 15739 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = (𝑑 ∘ ◡𝑇) → Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = Σ𝑎 ∈ (0..^𝑆)((𝑑 ∘ ◡𝑇)‘𝑎)) |
| 153 | 152 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑑 ∘ ◡𝑇) → (Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀 ↔ Σ𝑎 ∈ (0..^𝑆)((𝑑 ∘ ◡𝑇)‘𝑎) = 𝑀)) |
| 154 | 153 | elrab 3692 |
. . . . . . . . . . . . . 14
⊢ ((𝑑 ∘ ◡𝑇) ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀} ↔ ((𝑑 ∘ ◡𝑇) ∈ (𝐴 ↑m (0..^𝑆)) ∧ Σ𝑎 ∈ (0..^𝑆)((𝑑 ∘ ◡𝑇)‘𝑎) = 𝑀)) |
| 155 | 125, 150,
154 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑 ∘ ◡𝑇) ∈ {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 156 | 23 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝐴(repr‘𝑆)𝑀) = {𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐‘𝑎) = 𝑀}) |
| 157 | 155, 156 | eleqtrrd 2844 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑 ∘ ◡𝑇) ∈ (𝐴(repr‘𝑆)𝑀)) |
| 158 | 127 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → Fun ◡𝑇) |
| 159 | 8, 131 | eleqtrrd 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 ∈ dom ◡𝑇) |
| 160 | 159 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → 𝑋 ∈ dom ◡𝑇) |
| 161 | | fvco 7007 |
. . . . . . . . . . . . . 14
⊢ ((Fun
◡𝑇 ∧ 𝑋 ∈ dom ◡𝑇) → ((𝑑 ∘ ◡𝑇)‘𝑋) = (𝑑‘(◡𝑇‘𝑋))) |
| 162 | 158, 160,
161 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ((𝑑 ∘ ◡𝑇)‘𝑋) = (𝑑‘(◡𝑇‘𝑋))) |
| 163 | | f1ocnvfv 7298 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) → ((𝑇‘0) = 𝑋 → (◡𝑇‘𝑋) = 0)) |
| 164 | 163 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) ∧ 0 ∈ (0..^𝑆)) ∧ (𝑇‘0) = 𝑋) → (◡𝑇‘𝑋) = 0) |
| 165 | 13, 11, 96, 164 | syl21anc 838 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝑇‘𝑋) = 0) |
| 166 | 165 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (◡𝑇‘𝑋) = 0) |
| 167 | 166 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑‘(◡𝑇‘𝑋)) = (𝑑‘0)) |
| 168 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘0) ∈ 𝐵) |
| 169 | 167, 168 | eqneltrd 2861 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ (𝑑‘(◡𝑇‘𝑋)) ∈ 𝐵) |
| 170 | 162, 169 | eqneltrd 2861 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → ¬ ((𝑑 ∘ ◡𝑇)‘𝑋) ∈ 𝐵) |
| 171 | | fveq1 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = (𝑑 ∘ ◡𝑇) → (𝑐‘𝑋) = ((𝑑 ∘ ◡𝑇)‘𝑋)) |
| 172 | 171 | eleq1d 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑑 ∘ ◡𝑇) → ((𝑐‘𝑋) ∈ 𝐵 ↔ ((𝑑 ∘ ◡𝑇)‘𝑋) ∈ 𝐵)) |
| 173 | 172 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝑑 ∘ ◡𝑇) → (¬ (𝑐‘𝑋) ∈ 𝐵 ↔ ¬ ((𝑑 ∘ ◡𝑇)‘𝑋) ∈ 𝐵)) |
| 174 | 173 | elrab 3692 |
. . . . . . . . . . . 12
⊢ ((𝑑 ∘ ◡𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘𝑋) ∈ 𝐵} ↔ ((𝑑 ∘ ◡𝑇) ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ ((𝑑 ∘ ◡𝑇)‘𝑋) ∈ 𝐵)) |
| 175 | 157, 170,
174 | sylanbrc 583 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑 ∘ ◡𝑇) ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘𝑋) ∈ 𝐵}) |
| 176 | 175, 18 | eleqtrrdi 2852 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑑 ∈ (𝐴(repr‘𝑆)𝑀)) ∧ ¬ (𝑑‘0) ∈ 𝐵) → (𝑑 ∘ ◡𝑇) ∈ 𝑃) |
| 177 | 176 | anasss 466 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ ◡𝑇) ∈ 𝑃) |
| 178 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑 ∘ ◡𝑇)) → 𝑐 = (𝑑 ∘ ◡𝑇)) |
| 179 | 178 | coeq1d 5872 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑 ∘ ◡𝑇)) → (𝑐 ∘ 𝑇) = ((𝑑 ∘ ◡𝑇) ∘ 𝑇)) |
| 180 | 179 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) ∧ 𝑐 = (𝑑 ∘ ◡𝑇)) → (𝑑 = (𝑐 ∘ 𝑇) ↔ 𝑑 = ((𝑑 ∘ ◡𝑇) ∘ 𝑇))) |
| 181 | | f1ococnv1 6877 |
. . . . . . . . . . . . . 14
⊢ (𝑇:(0..^𝑆)–1-1-onto→(0..^𝑆) → (◡𝑇 ∘ 𝑇) = ( I ↾ (0..^𝑆))) |
| 182 | 13, 181 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑇 ∘ 𝑇) = ( I ↾ (0..^𝑆))) |
| 183 | 182 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (◡𝑇 ∘ 𝑇) = ( I ↾ (0..^𝑆))) |
| 184 | 183 | coeq2d 5873 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ (◡𝑇 ∘ 𝑇)) = (𝑑 ∘ ( I ↾ (0..^𝑆)))) |
| 185 | 114 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑:(0..^𝑆)⟶𝐴) |
| 186 | | fcoi1 6782 |
. . . . . . . . . . . 12
⊢ (𝑑:(0..^𝑆)⟶𝐴 → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑) |
| 187 | 185, 186 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → (𝑑 ∘ ( I ↾ (0..^𝑆))) = 𝑑) |
| 188 | 184, 187 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = (𝑑 ∘ (◡𝑇 ∘ 𝑇))) |
| 189 | | coass 6285 |
. . . . . . . . . 10
⊢ ((𝑑 ∘ ◡𝑇) ∘ 𝑇) = (𝑑 ∘ (◡𝑇 ∘ 𝑇)) |
| 190 | 188, 189 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → 𝑑 = ((𝑑 ∘ ◡𝑇) ∘ 𝑇)) |
| 191 | 177, 180,
190 | rspcedvd 3624 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) → ∃𝑐 ∈ 𝑃 𝑑 = (𝑐 ∘ 𝑇)) |
| 192 | 109, 191 | impbida 801 |
. . . . . . 7
⊢ (𝜑 → (∃𝑐 ∈ 𝑃 𝑑 = (𝑐 ∘ 𝑇) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))) |
| 193 | 38, 192 | bitrd 279 |
. . . . . 6
⊢ (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) “ 𝑃) ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵))) |
| 194 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑐 = 𝑑 → (𝑐‘0) = (𝑑‘0)) |
| 195 | 194 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑐 = 𝑑 → ((𝑐‘0) ∈ 𝐵 ↔ (𝑑‘0) ∈ 𝐵)) |
| 196 | 195 | notbid 318 |
. . . . . . 7
⊢ (𝑐 = 𝑑 → (¬ (𝑐‘0) ∈ 𝐵 ↔ ¬ (𝑑‘0) ∈ 𝐵)) |
| 197 | 196 | elrab 3692 |
. . . . . 6
⊢ (𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵} ↔ (𝑑 ∈ (𝐴(repr‘𝑆)𝑀) ∧ ¬ (𝑑‘0) ∈ 𝐵)) |
| 198 | 193, 197 | bitr4di 289 |
. . . . 5
⊢ (𝜑 → (𝑑 ∈ ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) “ 𝑃) ↔ 𝑑 ∈ {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵})) |
| 199 | 198 | eqrdv 2735 |
. . . 4
⊢ (𝜑 → ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) “ 𝑃) = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵}) |
| 200 | | reprpmtf1o.o |
. . . 4
⊢ 𝑂 = {𝑐 ∈ (𝐴(repr‘𝑆)𝑀) ∣ ¬ (𝑐‘0) ∈ 𝐵} |
| 201 | 199, 200 | eqtr4di 2795 |
. . 3
⊢ (𝜑 → ((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) “ 𝑃) = 𝑂) |
| 202 | 34, 35, 201 | f1oeq123d 6842 |
. 2
⊢ (𝜑 → (((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) ↾ 𝑃):𝑃–1-1-onto→((𝑐 ∈ (𝐴 ↑m (0..^𝑆)) ↦ (𝑐 ∘ 𝑇)) “ 𝑃) ↔ 𝐹:𝑃–1-1-onto→𝑂)) |
| 203 | 30, 202 | mpbid 232 |
1
⊢ (𝜑 → 𝐹:𝑃–1-1-onto→𝑂) |