Proof of Theorem diophrw
Step | Hyp | Ref
| Expression |
1 | | simpr 479 |
. . . . . . . . 9
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) → 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) |
2 | | nn0ex 11649 |
. . . . . . . . . 10
⊢
ℕ0 ∈ V |
3 | | simp1 1127 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V) |
4 | 3 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) → 𝑆 ∈ V) |
5 | | elmapg 8153 |
. . . . . . . . . 10
⊢
((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0
↑𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0)) |
6 | 2, 4, 5 | sylancr 581 |
. . . . . . . . 9
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) → (𝑏 ∈ (ℕ0
↑𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0)) |
7 | 1, 6 | mpbid 224 |
. . . . . . . 8
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) → 𝑏:𝑆⟶ℕ0) |
8 | 7 | adantr 474 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0) |
9 | | simp2 1128 |
. . . . . . . . 9
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇–1-1→𝑆) |
10 | | f1f 6351 |
. . . . . . . . 9
⊢ (𝑀:𝑇–1-1→𝑆 → 𝑀:𝑇⟶𝑆) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇⟶𝑆) |
12 | 11 | ad2antrr 716 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑀:𝑇⟶𝑆) |
13 | | fco 6308 |
. . . . . . 7
⊢ ((𝑏:𝑆⟶ℕ0 ∧ 𝑀:𝑇⟶𝑆) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0) |
14 | 8, 12, 13 | syl2anc 579 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0) |
15 | | f1dmex 7415 |
. . . . . . . . 9
⊢ ((𝑀:𝑇–1-1→𝑆 ∧ 𝑆 ∈ V) → 𝑇 ∈ V) |
16 | 9, 3, 15 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V) |
17 | 16 | ad2antrr 716 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V) |
18 | | elmapg 8153 |
. . . . . . 7
⊢
((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏 ∘ 𝑀) ∈ (ℕ0
↑𝑚 𝑇) ↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0)) |
19 | 2, 17, 18 | sylancr 581 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ∈ (ℕ0
↑𝑚 𝑇) ↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0)) |
20 | 14, 19 | mpbird 249 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀) ∈ (ℕ0
↑𝑚 𝑇)) |
21 | | simprl 761 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏 ↾ 𝑂)) |
22 | | resco 5893 |
. . . . . . 7
⊢ ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀 ↾ 𝑂)) |
23 | | simpll3 1230 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) |
24 | 23 | coeq2d 5530 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ∘ ( I ↾ 𝑂))) |
25 | | coires1 5907 |
. . . . . . . 8
⊢ (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏 ↾ 𝑂) |
26 | 24, 25 | syl6eq 2830 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ↾ 𝑂)) |
27 | 22, 26 | syl5eq 2826 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ↾ 𝑂)) |
28 | 21, 27 | eqtr4d 2817 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂)) |
29 | | simpll1 1226 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V) |
30 | | oveq2 6930 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑆 → (ℕ0
↑𝑚 𝑎) = (ℕ0
↑𝑚 𝑆)) |
31 | | oveq2 6930 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑆 → (ℤ ↑𝑚
𝑎) = (ℤ
↑𝑚 𝑆)) |
32 | 30, 31 | sseq12d 3853 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑆 → ((ℕ0
↑𝑚 𝑎) ⊆ (ℤ ↑𝑚
𝑎) ↔
(ℕ0 ↑𝑚 𝑆) ⊆ (ℤ
↑𝑚 𝑆))) |
33 | | zex 11737 |
. . . . . . . . . . 11
⊢ ℤ
∈ V |
34 | | nn0ssz 11750 |
. . . . . . . . . . 11
⊢
ℕ0 ⊆ ℤ |
35 | | mapss 8186 |
. . . . . . . . . . 11
⊢ ((ℤ
∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0
↑𝑚 𝑎) ⊆ (ℤ ↑𝑚
𝑎)) |
36 | 33, 34, 35 | mp2an 682 |
. . . . . . . . . 10
⊢
(ℕ0 ↑𝑚 𝑎) ⊆ (ℤ ↑𝑚
𝑎) |
37 | 32, 36 | vtoclg 3467 |
. . . . . . . . 9
⊢ (𝑆 ∈ V →
(ℕ0 ↑𝑚 𝑆) ⊆ (ℤ
↑𝑚 𝑆)) |
38 | 29, 37 | syl 17 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (ℕ0
↑𝑚 𝑆) ⊆ (ℤ
↑𝑚 𝑆)) |
39 | | simplr 759 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) |
40 | 38, 39 | sseldd 3822 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑𝑚
𝑆)) |
41 | | coeq1 5525 |
. . . . . . . . 9
⊢ (𝑑 = 𝑏 → (𝑑 ∘ 𝑀) = (𝑏 ∘ 𝑀)) |
42 | 41 | fveq2d 6450 |
. . . . . . . 8
⊢ (𝑑 = 𝑏 → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(𝑏 ∘ 𝑀))) |
43 | | eqid 2778 |
. . . . . . . 8
⊢ (𝑑 ∈ (ℤ
↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀))) = (𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀))) |
44 | | fvex 6459 |
. . . . . . . 8
⊢ (𝑃‘(𝑏 ∘ 𝑀)) ∈ V |
45 | 42, 43, 44 | fvmpt 6542 |
. . . . . . 7
⊢ (𝑏 ∈ (ℤ
↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀))) |
46 | 40, 45 | syl 17 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀))) |
47 | | simprr 763 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) |
48 | 46, 47 | eqtr3d 2816 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏 ∘ 𝑀)) = 0) |
49 | | reseq1 5636 |
. . . . . . . 8
⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑐 ↾ 𝑂) = ((𝑏 ∘ 𝑀) ↾ 𝑂)) |
50 | 49 | eqeq2d 2788 |
. . . . . . 7
⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑎 = (𝑐 ↾ 𝑂) ↔ 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂))) |
51 | | fveqeq2 6455 |
. . . . . . 7
⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑃‘𝑐) = 0 ↔ (𝑃‘(𝑏 ∘ 𝑀)) = 0)) |
52 | 50, 51 | anbi12d 624 |
. . . . . 6
⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) ↔ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0))) |
53 | 52 | rspcev 3511 |
. . . . 5
⊢ (((𝑏 ∘ 𝑀) ∈ (ℕ0
↑𝑚 𝑇) ∧ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0
↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) |
54 | 20, 28, 48, 53 | syl12anc 827 |
. . . 4
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0
↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) |
55 | 54 | rexlimdva2 3216 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0
↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0
↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))) |
56 | | simpr 479 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) |
57 | 16 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → 𝑇 ∈ V) |
58 | | elmapg 8153 |
. . . . . . . . . . . 12
⊢
((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0
↑𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0)) |
59 | 2, 57, 58 | sylancr 581 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑐 ∈ (ℕ0
↑𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0)) |
60 | 56, 59 | mpbid 224 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → 𝑐:𝑇⟶ℕ0) |
61 | 60 | adantr 474 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℕ0) |
62 | 9 | ad2antrr 716 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑀:𝑇–1-1→𝑆) |
63 | | f1cnv 6414 |
. . . . . . . . . 10
⊢ (𝑀:𝑇–1-1→𝑆 → ◡𝑀:ran 𝑀–1-1-onto→𝑇) |
64 | | f1of 6391 |
. . . . . . . . . 10
⊢ (◡𝑀:ran 𝑀–1-1-onto→𝑇 → ◡𝑀:ran 𝑀⟶𝑇) |
65 | 62, 63, 64 | 3syl 18 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ◡𝑀:ran 𝑀⟶𝑇) |
66 | | fco 6308 |
. . . . . . . . 9
⊢ ((𝑐:𝑇⟶ℕ0 ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0) |
67 | 61, 65, 66 | syl2anc 579 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0) |
68 | | c0ex 10370 |
. . . . . . . . . 10
⊢ 0 ∈
V |
69 | 68 | fconst 6341 |
. . . . . . . . 9
⊢ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0} |
70 | 69 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) |
71 | | disjdif 4264 |
. . . . . . . . 9
⊢ (ran
𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅ |
72 | 71 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) |
73 | | fun 6316 |
. . . . . . . 8
⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪
{0})) |
74 | 67, 70, 72, 73 | syl21anc 828 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪
{0})) |
75 | | frn 6297 |
. . . . . . . . . . 11
⊢ (𝑀:𝑇⟶𝑆 → ran 𝑀 ⊆ 𝑆) |
76 | 9, 10, 75 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → ran 𝑀 ⊆ 𝑆) |
77 | 76 | ad2antrr 716 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ran 𝑀 ⊆ 𝑆) |
78 | | undif 4273 |
. . . . . . . . 9
⊢ (ran
𝑀 ⊆ 𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆) |
79 | 77, 78 | sylib 210 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆) |
80 | | 0nn0 11659 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
81 | | snssi 4570 |
. . . . . . . . . . 11
⊢ (0 ∈
ℕ0 → {0} ⊆ ℕ0) |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . . 10
⊢ {0}
⊆ ℕ0 |
83 | | ssequn2 4009 |
. . . . . . . . . 10
⊢ ({0}
⊆ ℕ0 ↔ (ℕ0 ∪ {0}) =
ℕ0) |
84 | 82, 83 | mpbi 222 |
. . . . . . . . 9
⊢
(ℕ0 ∪ {0}) = ℕ0 |
85 | 84 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℕ0 ∪
{0}) = ℕ0) |
86 | 79, 85 | feq23d 6286 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0})
↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)) |
87 | 74, 86 | mpbid 224 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0) |
88 | | elmapg 8153 |
. . . . . . . 8
⊢
((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)) |
89 | 2, 3, 88 | sylancr 581 |
. . . . . . 7
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)) |
90 | 89 | ad2antrr 716 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)) |
91 | 87, 90 | mpbird 249 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑𝑚 𝑆)) |
92 | | simprl 761 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (𝑐 ↾ 𝑂)) |
93 | | resundir 5661 |
. . . . . . . . 9
⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) |
94 | | resco 5893 |
. . . . . . . . . . 11
⊢ ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ∘ (◡𝑀 ↾ 𝑂)) |
95 | | cnvresid 6213 |
. . . . . . . . . . . . . 14
⊢ ◡( I ↾ 𝑂) = ( I ↾ 𝑂) |
96 | | simpl2 1201 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → 𝑀:𝑇–1-1→𝑆) |
97 | | df-f1 6140 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀:𝑇–1-1→𝑆 ↔ (𝑀:𝑇⟶𝑆 ∧ Fun ◡𝑀)) |
98 | 97 | simprbi 492 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀:𝑇–1-1→𝑆 → Fun ◡𝑀) |
99 | | funcnvres 6212 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡𝑀 → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂))) |
100 | 96, 98, 99 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂))) |
101 | | simpl3 1203 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) |
102 | 101 | cnveqd 5543 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → ◡(𝑀 ↾ 𝑂) = ◡( I ↾ 𝑂)) |
103 | | df-ima 5368 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 “ 𝑂) = ran (𝑀 ↾ 𝑂) |
104 | 101 | rneqd 5598 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) = ran ( I ↾ 𝑂)) |
105 | | rnresi 5733 |
. . . . . . . . . . . . . . . . . 18
⊢ ran ( I
↾ 𝑂) = 𝑂 |
106 | 104, 105 | syl6eq 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) = 𝑂) |
107 | 103, 106 | syl5eq 2826 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑀 “ 𝑂) = 𝑂) |
108 | 107 | reseq2d 5642 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (◡𝑀 ↾ (𝑀 “ 𝑂)) = (◡𝑀 ↾ 𝑂)) |
109 | 100, 102,
108 | 3eqtr3d 2822 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → ◡( I ↾ 𝑂) = (◡𝑀 ↾ 𝑂)) |
110 | 95, 109 | syl5reqr 2829 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (◡𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) |
111 | 110 | coeq2d 5530 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ∘ ( I ↾ 𝑂))) |
112 | | coires1 5907 |
. . . . . . . . . . . 12
⊢ (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐 ↾ 𝑂) |
113 | 111, 112 | syl6eq 2830 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ↾ 𝑂)) |
114 | 94, 113 | syl5eq 2826 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ↾ 𝑂)) |
115 | | dmres 5668 |
. . . . . . . . . . . 12
⊢ dom
(((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) |
116 | 68 | snnz 4542 |
. . . . . . . . . . . . . . 15
⊢ {0} ≠
∅ |
117 | | dmxp 5589 |
. . . . . . . . . . . . . . 15
⊢ ({0} ≠
∅ → dom ((𝑆
∖ ran 𝑀) × {0})
= (𝑆 ∖ ran 𝑀)) |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom
((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀) |
119 | 118 | ineq2i 4034 |
. . . . . . . . . . . . 13
⊢ (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀)) |
120 | | inss1 4053 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 ∩ 𝑆) ⊆ 𝑂 |
121 | 104, 105 | syl6req 2831 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → 𝑂 = ran (𝑀 ↾ 𝑂)) |
122 | | resss 5671 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ↾ 𝑂) ⊆ 𝑀 |
123 | | rnss 5599 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ↾ 𝑂) ⊆ 𝑀 → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀) |
124 | 122, 123 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀) |
125 | 121, 124 | eqsstrd 3858 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → 𝑂 ⊆ ran 𝑀) |
126 | 120, 125 | syl5ss 3832 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑂 ∩ 𝑆) ⊆ ran 𝑀) |
127 | | inssdif0 4178 |
. . . . . . . . . . . . . 14
⊢ ((𝑂 ∩ 𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅) |
128 | 126, 127 | sylib 210 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅) |
129 | 119, 128 | syl5eq 2826 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅) |
130 | 115, 129 | syl5eq 2826 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅) |
131 | | relres 5675 |
. . . . . . . . . . . 12
⊢ Rel
(((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) |
132 | | reldm0 5588 |
. . . . . . . . . . . 12
⊢ (Rel
(((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) → ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)) |
133 | 131, 132 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅) |
134 | 130, 133 | sylibr 226 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅) |
135 | 114, 134 | uneq12d 3991 |
. . . . . . . . 9
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐 ↾ 𝑂) ∪ ∅)) |
136 | 93, 135 | syl5eq 2826 |
. . . . . . . 8
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐 ↾ 𝑂) ∪ ∅)) |
137 | | un0 4193 |
. . . . . . . 8
⊢ ((𝑐 ↾ 𝑂) ∪ ∅) = (𝑐 ↾ 𝑂) |
138 | 136, 137 | syl6req 2831 |
. . . . . . 7
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)) |
139 | 138 | adantr 474 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)) |
140 | 92, 139 | eqtrd 2814 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)) |
141 | | fss 6304 |
. . . . . . . . . . . . 13
⊢ ((𝑐:𝑇⟶ℕ0 ∧
ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ) |
142 | 60, 34, 141 | sylancl 580 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) → 𝑐:𝑇⟶ℤ) |
143 | 142 | adantr 474 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℤ) |
144 | | fco 6308 |
. . . . . . . . . . 11
⊢ ((𝑐:𝑇⟶ℤ ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ) |
145 | 143, 65, 144 | syl2anc 579 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ) |
146 | | fun 6316 |
. . . . . . . . . 10
⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪
{0})) |
147 | 145, 70, 72, 146 | syl21anc 828 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪
{0})) |
148 | | 0z 11739 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
149 | | snssi 4570 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → {0} ⊆ ℤ) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ {0}
⊆ ℤ |
151 | | ssequn2 4009 |
. . . . . . . . . . . 12
⊢ ({0}
⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ) |
152 | 150, 151 | mpbi 222 |
. . . . . . . . . . 11
⊢ (ℤ
∪ {0}) = ℤ |
153 | 152 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℤ ∪ {0}) =
ℤ) |
154 | 79, 153 | feq23d 6286 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)) |
155 | 147, 154 | mpbid 224 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ) |
156 | | elmapg 8153 |
. . . . . . . . . 10
⊢ ((ℤ
∈ V ∧ 𝑆 ∈ V)
→ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)) |
157 | 33, 3, 156 | sylancr 581 |
. . . . . . . . 9
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)) |
158 | 157 | ad2antrr 716 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)) |
159 | 155, 158 | mpbird 249 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑𝑚 𝑆)) |
160 | | coeq1 5525 |
. . . . . . . . 9
⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑 ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) |
161 | 160 | fveq2d 6450 |
. . . . . . . 8
⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))) |
162 | | fvex 6459 |
. . . . . . . 8
⊢ (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V |
163 | 161, 43, 162 | fvmpt 6542 |
. . . . . . 7
⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))) |
164 | 159, 163 | syl 17 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))) |
165 | | coundir 5891 |
. . . . . . . 8
⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) |
166 | | coass 5908 |
. . . . . . . . . . 11
⊢ ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ (◡𝑀 ∘ 𝑀)) |
167 | | f1cocnv1 6420 |
. . . . . . . . . . . . 13
⊢ (𝑀:𝑇–1-1→𝑆 → (◡𝑀 ∘ 𝑀) = ( I ↾ 𝑇)) |
168 | 167 | coeq2d 5530 |
. . . . . . . . . . . 12
⊢ (𝑀:𝑇–1-1→𝑆 → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇))) |
169 | 62, 168 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇))) |
170 | 166, 169 | syl5eq 2826 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇))) |
171 | 118 | ineq1i 4033 |
. . . . . . . . . . . . 13
⊢ (dom
((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) |
172 | | incom 4028 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) |
173 | 171, 172,
71 | 3eqtri 2806 |
. . . . . . . . . . . 12
⊢ (dom
((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅ |
174 | | coeq0 5898 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ ↔ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅) |
175 | 173, 174 | mpbir 223 |
. . . . . . . . . . 11
⊢ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ |
176 | 175 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅) |
177 | 170, 176 | uneq12d 3991 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅)) |
178 | | un0 4193 |
. . . . . . . . . 10
⊢ ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇)) |
179 | | fcoi1 6328 |
. . . . . . . . . . 11
⊢ (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐) |
180 | 61, 179 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐) |
181 | 178, 180 | syl5eq 2826 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐) |
182 | 177, 181 | eqtrd 2814 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐) |
183 | 165, 182 | syl5eq 2826 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐) |
184 | 183 | fveq2d 6450 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃‘𝑐)) |
185 | | simprr 763 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘𝑐) = 0) |
186 | 164, 184,
185 | 3eqtrd 2818 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0) |
187 | | reseq1 5636 |
. . . . . . . 8
⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)) |
188 | 187 | eqeq2d 2788 |
. . . . . . 7
⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏 ↾ 𝑂) ↔ 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))) |
189 | | fveqeq2 6455 |
. . . . . . 7
⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) |
190 | 188, 189 | anbi12d 624 |
. . . . . 6
⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))) |
191 | 190 | rspcev 3511 |
. . . . 5
⊢ ((((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑𝑚 𝑆) ∧ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0
↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) |
192 | 91, 140, 186, 191 | syl12anc 827 |
. . . 4
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ∃𝑏 ∈ (ℕ0
↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) |
193 | 192 | rexlimdva2 3216 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0
↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) → ∃𝑏 ∈ (ℕ0
↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0))) |
194 | 55, 193 | impbid 204 |
. 2
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0
↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0
↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))) |
195 | 194 | abbidv 2906 |
1
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚
𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0
↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)}) |