Proof of Theorem diophrw
Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
→ 𝑏 ∈
(ℕ0 ↑m 𝑆)) |
2 | | nn0ex 12120 |
. . . . . . . . . 10
⊢
ℕ0 ∈ V |
3 | | simp1 1138 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V) |
4 | 3 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
→ 𝑆 ∈
V) |
5 | | elmapg 8541 |
. . . . . . . . . 10
⊢
((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0
↑m 𝑆)
↔ 𝑏:𝑆⟶ℕ0)) |
6 | 2, 4, 5 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
→ (𝑏 ∈
(ℕ0 ↑m 𝑆) ↔ 𝑏:𝑆⟶ℕ0)) |
7 | 1, 6 | mpbid 235 |
. . . . . . . 8
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
→ 𝑏:𝑆⟶ℕ0) |
8 | 7 | adantr 484 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0) |
9 | | simp2 1139 |
. . . . . . . . 9
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇–1-1→𝑆) |
10 | | f1f 6633 |
. . . . . . . . 9
⊢ (𝑀:𝑇–1-1→𝑆 → 𝑀:𝑇⟶𝑆) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇⟶𝑆) |
12 | 11 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑀:𝑇⟶𝑆) |
13 | | fco 6587 |
. . . . . . 7
⊢ ((𝑏:𝑆⟶ℕ0 ∧ 𝑀:𝑇⟶𝑆) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0) |
14 | 8, 12, 13 | syl2anc 587 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0) |
15 | | f1dmex 7748 |
. . . . . . . . 9
⊢ ((𝑀:𝑇–1-1→𝑆 ∧ 𝑆 ∈ V) → 𝑇 ∈ V) |
16 | 9, 3, 15 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V) |
17 | 16 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V) |
18 | | elmapg 8541 |
. . . . . . 7
⊢
((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏 ∘ 𝑀) ∈ (ℕ0
↑m 𝑇)
↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0)) |
19 | 2, 17, 18 | sylancr 590 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ∈ (ℕ0
↑m 𝑇)
↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0)) |
20 | 14, 19 | mpbird 260 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀) ∈ (ℕ0
↑m 𝑇)) |
21 | | simprl 771 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏 ↾ 𝑂)) |
22 | | resco 6128 |
. . . . . . 7
⊢ ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀 ↾ 𝑂)) |
23 | | simpll3 1216 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) |
24 | 23 | coeq2d 5745 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ∘ ( I ↾ 𝑂))) |
25 | | coires1 6142 |
. . . . . . . 8
⊢ (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏 ↾ 𝑂) |
26 | 24, 25 | eqtrdi 2795 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ↾ 𝑂)) |
27 | 22, 26 | syl5eq 2791 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ↾ 𝑂)) |
28 | 21, 27 | eqtr4d 2781 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂)) |
29 | | simpll1 1214 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V) |
30 | | oveq2 7239 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑆 → (ℕ0
↑m 𝑎) =
(ℕ0 ↑m 𝑆)) |
31 | | oveq2 7239 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑆 → (ℤ ↑m 𝑎) = (ℤ ↑m
𝑆)) |
32 | 30, 31 | sseq12d 3948 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑆 → ((ℕ0
↑m 𝑎)
⊆ (ℤ ↑m 𝑎) ↔ (ℕ0
↑m 𝑆)
⊆ (ℤ ↑m 𝑆))) |
33 | | zex 12209 |
. . . . . . . . . . 11
⊢ ℤ
∈ V |
34 | | nn0ssz 12222 |
. . . . . . . . . . 11
⊢
ℕ0 ⊆ ℤ |
35 | | mapss 8590 |
. . . . . . . . . . 11
⊢ ((ℤ
∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0
↑m 𝑎)
⊆ (ℤ ↑m 𝑎)) |
36 | 33, 34, 35 | mp2an 692 |
. . . . . . . . . 10
⊢
(ℕ0 ↑m 𝑎) ⊆ (ℤ ↑m 𝑎) |
37 | 32, 36 | vtoclg 3493 |
. . . . . . . . 9
⊢ (𝑆 ∈ V →
(ℕ0 ↑m 𝑆) ⊆ (ℤ ↑m 𝑆)) |
38 | 29, 37 | syl 17 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (ℕ0
↑m 𝑆)
⊆ (ℤ ↑m 𝑆)) |
39 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0
↑m 𝑆)) |
40 | 38, 39 | sseldd 3916 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑m 𝑆)) |
41 | | coeq1 5740 |
. . . . . . . . 9
⊢ (𝑑 = 𝑏 → (𝑑 ∘ 𝑀) = (𝑏 ∘ 𝑀)) |
42 | 41 | fveq2d 6739 |
. . . . . . . 8
⊢ (𝑑 = 𝑏 → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(𝑏 ∘ 𝑀))) |
43 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑑 ∈ (ℤ
↑m 𝑆)
↦ (𝑃‘(𝑑 ∘ 𝑀))) = (𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀))) |
44 | | fvex 6748 |
. . . . . . . 8
⊢ (𝑃‘(𝑏 ∘ 𝑀)) ∈ V |
45 | 42, 43, 44 | fvmpt 6836 |
. . . . . . 7
⊢ (𝑏 ∈ (ℤ
↑m 𝑆)
→ ((𝑑 ∈ (ℤ
↑m 𝑆)
↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀))) |
46 | 40, 45 | syl 17 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀))) |
47 | | simprr 773 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) |
48 | 46, 47 | eqtr3d 2780 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏 ∘ 𝑀)) = 0) |
49 | | reseq1 5859 |
. . . . . . . 8
⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑐 ↾ 𝑂) = ((𝑏 ∘ 𝑀) ↾ 𝑂)) |
50 | 49 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑎 = (𝑐 ↾ 𝑂) ↔ 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂))) |
51 | | fveqeq2 6744 |
. . . . . . 7
⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑃‘𝑐) = 0 ↔ (𝑃‘(𝑏 ∘ 𝑀)) = 0)) |
52 | 50, 51 | anbi12d 634 |
. . . . . 6
⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) ↔ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0))) |
53 | 52 | rspcev 3549 |
. . . . 5
⊢ (((𝑏 ∘ 𝑀) ∈ (ℕ0
↑m 𝑇) ∧
(𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0
↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) |
54 | 20, 28, 48, 53 | syl12anc 837 |
. . . 4
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0
↑m 𝑆))
∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0
↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) |
55 | 54 | rexlimdva2 3214 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0
↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0
↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))) |
56 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ 𝑐 ∈
(ℕ0 ↑m 𝑇)) |
57 | 16 | adantr 484 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ 𝑇 ∈
V) |
58 | | elmapg 8541 |
. . . . . . . . . . . 12
⊢
((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0
↑m 𝑇)
↔ 𝑐:𝑇⟶ℕ0)) |
59 | 2, 57, 58 | sylancr 590 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑐 ∈
(ℕ0 ↑m 𝑇) ↔ 𝑐:𝑇⟶ℕ0)) |
60 | 56, 59 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ 𝑐:𝑇⟶ℕ0) |
61 | 60 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℕ0) |
62 | 9 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑀:𝑇–1-1→𝑆) |
63 | | f1cnv 6702 |
. . . . . . . . . 10
⊢ (𝑀:𝑇–1-1→𝑆 → ◡𝑀:ran 𝑀–1-1-onto→𝑇) |
64 | | f1of 6679 |
. . . . . . . . . 10
⊢ (◡𝑀:ran 𝑀–1-1-onto→𝑇 → ◡𝑀:ran 𝑀⟶𝑇) |
65 | 62, 63, 64 | 3syl 18 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ◡𝑀:ran 𝑀⟶𝑇) |
66 | | fco 6587 |
. . . . . . . . 9
⊢ ((𝑐:𝑇⟶ℕ0 ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0) |
67 | 61, 65, 66 | syl2anc 587 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0) |
68 | | c0ex 10851 |
. . . . . . . . . 10
⊢ 0 ∈
V |
69 | 68 | fconst 6623 |
. . . . . . . . 9
⊢ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0} |
70 | 69 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) |
71 | | disjdif 4400 |
. . . . . . . . 9
⊢ (ran
𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅ |
72 | 71 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) |
73 | | fun 6599 |
. . . . . . . 8
⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪
{0})) |
74 | 67, 70, 72, 73 | syl21anc 838 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪
{0})) |
75 | | frn 6570 |
. . . . . . . . . . 11
⊢ (𝑀:𝑇⟶𝑆 → ran 𝑀 ⊆ 𝑆) |
76 | 9, 10, 75 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → ran 𝑀 ⊆ 𝑆) |
77 | 76 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ran 𝑀 ⊆ 𝑆) |
78 | | undif 4410 |
. . . . . . . . 9
⊢ (ran
𝑀 ⊆ 𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆) |
79 | 77, 78 | sylib 221 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆) |
80 | | 0nn0 12129 |
. . . . . . . . . . 11
⊢ 0 ∈
ℕ0 |
81 | | snssi 4735 |
. . . . . . . . . . 11
⊢ (0 ∈
ℕ0 → {0} ⊆ ℕ0) |
82 | 80, 81 | ax-mp 5 |
. . . . . . . . . 10
⊢ {0}
⊆ ℕ0 |
83 | | ssequn2 4111 |
. . . . . . . . . 10
⊢ ({0}
⊆ ℕ0 ↔ (ℕ0 ∪ {0}) =
ℕ0) |
84 | 82, 83 | mpbi 233 |
. . . . . . . . 9
⊢
(ℕ0 ∪ {0}) = ℕ0 |
85 | 84 | a1i 11 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℕ0 ∪
{0}) = ℕ0) |
86 | 79, 85 | feq23d 6558 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0})
↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)) |
87 | 74, 86 | mpbid 235 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0) |
88 | | elmapg 8541 |
. . . . . . . 8
⊢
((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑m 𝑆)
↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)) |
89 | 2, 3, 88 | sylancr 590 |
. . . . . . 7
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑m 𝑆)
↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)) |
90 | 89 | ad2antrr 726 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑m 𝑆)
↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)) |
91 | 87, 90 | mpbird 260 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑m 𝑆)) |
92 | | simprl 771 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (𝑐 ↾ 𝑂)) |
93 | | resundir 5880 |
. . . . . . . . 9
⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) |
94 | | resco 6128 |
. . . . . . . . . . 11
⊢ ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ∘ (◡𝑀 ↾ 𝑂)) |
95 | | simpl2 1194 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ 𝑀:𝑇–1-1→𝑆) |
96 | | df-f1 6402 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀:𝑇–1-1→𝑆 ↔ (𝑀:𝑇⟶𝑆 ∧ Fun ◡𝑀)) |
97 | 96 | simprbi 500 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀:𝑇–1-1→𝑆 → Fun ◡𝑀) |
98 | | funcnvres 6475 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
◡𝑀 → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂))) |
99 | 95, 97, 98 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂))) |
100 | | simpl3 1195 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) |
101 | 100 | cnveqd 5758 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ ◡(𝑀 ↾ 𝑂) = ◡( I ↾ 𝑂)) |
102 | | df-ima 5578 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 “ 𝑂) = ran (𝑀 ↾ 𝑂) |
103 | 100 | rneqd 5821 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ ran (𝑀 ↾ 𝑂) = ran ( I ↾ 𝑂)) |
104 | | rnresi 5957 |
. . . . . . . . . . . . . . . . . 18
⊢ ran ( I
↾ 𝑂) = 𝑂 |
105 | 103, 104 | eqtrdi 2795 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ ran (𝑀 ↾ 𝑂) = 𝑂) |
106 | 102, 105 | syl5eq 2791 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑀 “ 𝑂) = 𝑂) |
107 | 106 | reseq2d 5865 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (◡𝑀 ↾ (𝑀 “ 𝑂)) = (◡𝑀 ↾ 𝑂)) |
108 | 99, 101, 107 | 3eqtr3d 2786 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ ◡( I ↾ 𝑂) = (◡𝑀 ↾ 𝑂)) |
109 | | cnvresid 6476 |
. . . . . . . . . . . . . 14
⊢ ◡( I ↾ 𝑂) = ( I ↾ 𝑂) |
110 | 108, 109 | eqtr3di 2794 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (◡𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) |
111 | 110 | coeq2d 5745 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ∘ ( I ↾ 𝑂))) |
112 | | coires1 6142 |
. . . . . . . . . . . 12
⊢ (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐 ↾ 𝑂) |
113 | 111, 112 | eqtrdi 2795 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ↾ 𝑂)) |
114 | 94, 113 | syl5eq 2791 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ↾ 𝑂)) |
115 | | dmres 5887 |
. . . . . . . . . . . 12
⊢ dom
(((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) |
116 | 68 | snnz 4706 |
. . . . . . . . . . . . . . 15
⊢ {0} ≠
∅ |
117 | | dmxp 5812 |
. . . . . . . . . . . . . . 15
⊢ ({0} ≠
∅ → dom ((𝑆
∖ ran 𝑀) × {0})
= (𝑆 ∖ ran 𝑀)) |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ dom
((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀) |
119 | 118 | ineq2i 4138 |
. . . . . . . . . . . . 13
⊢ (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀)) |
120 | | inss1 4157 |
. . . . . . . . . . . . . . 15
⊢ (𝑂 ∩ 𝑆) ⊆ 𝑂 |
121 | 103, 104 | eqtr2di 2796 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ 𝑂 = ran (𝑀 ↾ 𝑂)) |
122 | | resss 5890 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ↾ 𝑂) ⊆ 𝑀 |
123 | | rnss 5822 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑀 ↾ 𝑂) ⊆ 𝑀 → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀) |
124 | 122, 123 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀) |
125 | 121, 124 | eqsstrd 3953 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ 𝑂 ⊆ ran 𝑀) |
126 | 120, 125 | sstrid 3926 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑂 ∩ 𝑆) ⊆ ran 𝑀) |
127 | | inssdif0 4298 |
. . . . . . . . . . . . . 14
⊢ ((𝑂 ∩ 𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅) |
128 | 126, 127 | sylib 221 |
. . . . . . . . . . . . 13
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅) |
129 | 119, 128 | syl5eq 2791 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅) |
130 | 115, 129 | syl5eq 2791 |
. . . . . . . . . . 11
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ dom (((𝑆 ∖ ran
𝑀) × {0}) ↾
𝑂) =
∅) |
131 | | relres 5894 |
. . . . . . . . . . . 12
⊢ Rel
(((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) |
132 | | reldm0 5811 |
. . . . . . . . . . . 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 237 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (((𝑆 ∖ ran
𝑀) × {0}) ↾
𝑂) =
∅) |
135 | 114, 134 | uneq12d 4092 |
. . . . . . . . 9
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐 ↾ 𝑂) ∪ ∅)) |
136 | 93, 135 | syl5eq 2791 |
. . . . . . . 8
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐 ↾ 𝑂) ∪ ∅)) |
137 | | un0 4319 |
. . . . . . . 8
⊢ ((𝑐 ↾ 𝑂) ∪ ∅) = (𝑐 ↾ 𝑂) |
138 | 136, 137 | eqtr2di 2796 |
. . . . . . 7
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)) |
139 | 138 | adantr 484 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)) |
140 | 92, 139 | eqtrd 2778 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)) |
141 | | fss 6580 |
. . . . . . . . . . . . 13
⊢ ((𝑐:𝑇⟶ℕ0 ∧
ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ) |
142 | 60, 34, 141 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
→ 𝑐:𝑇⟶ℤ) |
143 | 142 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℤ) |
144 | | fco 6587 |
. . . . . . . . . . 11
⊢ ((𝑐:𝑇⟶ℤ ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ) |
145 | 143, 65, 144 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ) |
146 | | fun 6599 |
. . . . . . . . . 10
⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪
{0})) |
147 | 145, 70, 72, 146 | syl21anc 838 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪
{0})) |
148 | | 0z 12211 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℤ |
149 | | snssi 4735 |
. . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → {0} ⊆ ℤ) |
150 | 148, 149 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ {0}
⊆ ℤ |
151 | | ssequn2 4111 |
. . . . . . . . . . . 12
⊢ ({0}
⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ) |
152 | 150, 151 | mpbi 233 |
. . . . . . . . . . 11
⊢ (ℤ
∪ {0}) = ℤ |
153 | 152 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℤ ∪ {0}) =
ℤ) |
154 | 79, 153 | feq23d 6558 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)) |
155 | 147, 154 | mpbid 235 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ) |
156 | | elmapg 8541 |
. . . . . . . . . 10
⊢ ((ℤ
∈ V ∧ 𝑆 ∈ V)
→ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑m 𝑆)
↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)) |
157 | 33, 3, 156 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑m 𝑆)
↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)) |
158 | 157 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑m 𝑆)
↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)) |
159 | 155, 158 | mpbird 260 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑m 𝑆)) |
160 | | coeq1 5740 |
. . . . . . . . 9
⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑 ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) |
161 | 160 | fveq2d 6739 |
. . . . . . . 8
⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))) |
162 | | fvex 6748 |
. . . . . . . 8
⊢ (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V |
163 | 161, 43, 162 | fvmpt 6836 |
. . . . . . 7
⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ
↑m 𝑆)
→ ((𝑑 ∈ (ℤ
↑m 𝑆)
↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))) |
164 | 159, 163 | syl 17 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))) |
165 | | coundir 6126 |
. . . . . . . 8
⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) |
166 | | coass 6143 |
. . . . . . . . . . 11
⊢ ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ (◡𝑀 ∘ 𝑀)) |
167 | | f1cocnv1 6708 |
. . . . . . . . . . . . 13
⊢ (𝑀:𝑇–1-1→𝑆 → (◡𝑀 ∘ 𝑀) = ( I ↾ 𝑇)) |
168 | 167 | coeq2d 5745 |
. . . . . . . . . . . 12
⊢ (𝑀:𝑇–1-1→𝑆 → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇))) |
169 | 62, 168 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇))) |
170 | 166, 169 | syl5eq 2791 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇))) |
171 | 118 | ineq1i 4137 |
. . . . . . . . . . . . 13
⊢ (dom
((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) |
172 | | incom 4129 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) |
173 | 171, 172,
71 | 3eqtri 2770 |
. . . . . . . . . . . 12
⊢ (dom
((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅ |
174 | | coeq0 6133 |
. . . . . . . . . . . 12
⊢ ((((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ ↔ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅) |
175 | 173, 174 | mpbir 234 |
. . . . . . . . . . 11
⊢ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ |
176 | 175 | a1i 11 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅) |
177 | 170, 176 | uneq12d 4092 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅)) |
178 | | un0 4319 |
. . . . . . . . . 10
⊢ ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇)) |
179 | | fcoi1 6611 |
. . . . . . . . . . 11
⊢ (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐) |
180 | 61, 179 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐) |
181 | 178, 180 | syl5eq 2791 |
. . . . . . . . 9
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐) |
182 | 177, 181 | eqtrd 2778 |
. . . . . . . 8
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐) |
183 | 165, 182 | syl5eq 2791 |
. . . . . . 7
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐) |
184 | 183 | fveq2d 6739 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃‘𝑐)) |
185 | | simprr 773 |
. . . . . 6
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘𝑐) = 0) |
186 | 164, 184,
185 | 3eqtrd 2782 |
. . . . 5
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0) |
187 | | reseq1 5859 |
. . . . . . . 8
⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)) |
188 | 187 | eqeq2d 2749 |
. . . . . . 7
⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏 ↾ 𝑂) ↔ 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))) |
189 | | fveqeq2 6744 |
. . . . . . 7
⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) |
190 | 188, 189 | anbi12d 634 |
. . . . . 6
⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))) |
191 | 190 | rspcev 3549 |
. . . . 5
⊢ ((((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0
↑m 𝑆) ∧
(𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0
↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) |
192 | 91, 140, 186, 191 | syl12anc 837 |
. . . 4
⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0
↑m 𝑇))
∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ∃𝑏 ∈ (ℕ0
↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) |
193 | 192 | rexlimdva2 3214 |
. . 3
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0
↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) → ∃𝑏 ∈ (ℕ0
↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0))) |
194 | 55, 193 | impbid 215 |
. 2
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0
↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0
↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))) |
195 | 194 | abbidv 2808 |
1
⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0
↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)}) |