Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  diophrw Structured version   Visualization version   GIF version

Theorem diophrw 39346
Description: Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014.)
Assertion
Ref Expression
diophrw ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)})
Distinct variable groups:   𝑆,𝑎,𝑏,𝑐,𝑑   𝑇,𝑎,𝑏,𝑐,𝑑   𝑀,𝑎,𝑏,𝑐,𝑑   𝑂,𝑎,𝑏,𝑐,𝑑   𝑃,𝑏,𝑐,𝑑
Allowed substitution hint:   𝑃(𝑎)

Proof of Theorem diophrw
StepHypRef Expression
1 simpr 487 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) → 𝑏 ∈ (ℕ0m 𝑆))
2 nn0ex 11895 . . . . . . . . . 10 0 ∈ V
3 simp1 1130 . . . . . . . . . . 11 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V)
43adantr 483 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) → 𝑆 ∈ V)
5 elmapg 8411 . . . . . . . . . 10 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0m 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
62, 4, 5sylancr 589 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) → (𝑏 ∈ (ℕ0m 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
71, 6mpbid 234 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) → 𝑏:𝑆⟶ℕ0)
87adantr 483 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0)
9 simp2 1131 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇1-1𝑆)
10 f1f 6568 . . . . . . . . 9 (𝑀:𝑇1-1𝑆𝑀:𝑇𝑆)
119, 10syl 17 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇𝑆)
1211ad2antrr 724 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑀:𝑇𝑆)
13 fco 6524 . . . . . . 7 ((𝑏:𝑆⟶ℕ0𝑀:𝑇𝑆) → (𝑏𝑀):𝑇⟶ℕ0)
148, 12, 13syl2anc 586 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀):𝑇⟶ℕ0)
15 f1dmex 7650 . . . . . . . . 9 ((𝑀:𝑇1-1𝑆𝑆 ∈ V) → 𝑇 ∈ V)
169, 3, 15syl2anc 586 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V)
1716ad2antrr 724 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V)
18 elmapg 8411 . . . . . . 7 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏𝑀) ∈ (ℕ0m 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
192, 17, 18sylancr 589 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ∈ (ℕ0m 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
2014, 19mpbird 259 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀) ∈ (ℕ0m 𝑇))
21 simprl 769 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏𝑂))
22 resco 6096 . . . . . . 7 ((𝑏𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀𝑂))
23 simpll3 1208 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑀𝑂) = ( I ↾ 𝑂))
2423coeq2d 5726 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏 ∘ ( I ↾ 𝑂)))
25 coires1 6110 . . . . . . . 8 (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏𝑂)
2624, 25syl6eq 2870 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏𝑂))
2722, 26syl5eq 2866 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ↾ 𝑂) = (𝑏𝑂))
2821, 27eqtr4d 2857 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏𝑀) ↾ 𝑂))
29 simpll1 1206 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V)
30 oveq2 7156 . . . . . . . . . . 11 (𝑎 = 𝑆 → (ℕ0m 𝑎) = (ℕ0m 𝑆))
31 oveq2 7156 . . . . . . . . . . 11 (𝑎 = 𝑆 → (ℤ ↑m 𝑎) = (ℤ ↑m 𝑆))
3230, 31sseq12d 3998 . . . . . . . . . 10 (𝑎 = 𝑆 → ((ℕ0m 𝑎) ⊆ (ℤ ↑m 𝑎) ↔ (ℕ0m 𝑆) ⊆ (ℤ ↑m 𝑆)))
33 zex 11982 . . . . . . . . . . 11 ℤ ∈ V
34 nn0ssz 11995 . . . . . . . . . . 11 0 ⊆ ℤ
35 mapss 8445 . . . . . . . . . . 11 ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0m 𝑎) ⊆ (ℤ ↑m 𝑎))
3633, 34, 35mp2an 690 . . . . . . . . . 10 (ℕ0m 𝑎) ⊆ (ℤ ↑m 𝑎)
3732, 36vtoclg 3566 . . . . . . . . 9 (𝑆 ∈ V → (ℕ0m 𝑆) ⊆ (ℤ ↑m 𝑆))
3829, 37syl 17 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (ℕ0m 𝑆) ⊆ (ℤ ↑m 𝑆))
39 simplr 767 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0m 𝑆))
4038, 39sseldd 3966 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑m 𝑆))
41 coeq1 5721 . . . . . . . . 9 (𝑑 = 𝑏 → (𝑑𝑀) = (𝑏𝑀))
4241fveq2d 6667 . . . . . . . 8 (𝑑 = 𝑏 → (𝑃‘(𝑑𝑀)) = (𝑃‘(𝑏𝑀)))
43 eqid 2819 . . . . . . . 8 (𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀))) = (𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))
44 fvex 6676 . . . . . . . 8 (𝑃‘(𝑏𝑀)) ∈ V
4542, 43, 44fvmpt 6761 . . . . . . 7 (𝑏 ∈ (ℤ ↑m 𝑆) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = (𝑃‘(𝑏𝑀)))
4640, 45syl 17 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = (𝑃‘(𝑏𝑀)))
47 simprr 771 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)
4846, 47eqtr3d 2856 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏𝑀)) = 0)
49 reseq1 5840 . . . . . . . 8 (𝑐 = (𝑏𝑀) → (𝑐𝑂) = ((𝑏𝑀) ↾ 𝑂))
5049eqeq2d 2830 . . . . . . 7 (𝑐 = (𝑏𝑀) → (𝑎 = (𝑐𝑂) ↔ 𝑎 = ((𝑏𝑀) ↾ 𝑂)))
51 fveqeq2 6672 . . . . . . 7 (𝑐 = (𝑏𝑀) → ((𝑃𝑐) = 0 ↔ (𝑃‘(𝑏𝑀)) = 0))
5250, 51anbi12d 632 . . . . . 6 (𝑐 = (𝑏𝑀) → ((𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) ↔ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)))
5352rspcev 3621 . . . . 5 (((𝑏𝑀) ∈ (ℕ0m 𝑇) ∧ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5420, 28, 48, 53syl12anc 834 . . . 4 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5554rexlimdva2 3285 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
56 simpr 487 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑐 ∈ (ℕ0m 𝑇))
5716adantr 483 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑇 ∈ V)
58 elmapg 8411 . . . . . . . . . . . 12 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0m 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
592, 57, 58sylancr 589 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑐 ∈ (ℕ0m 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
6056, 59mpbid 234 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑐:𝑇⟶ℕ0)
6160adantr 483 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℕ0)
629ad2antrr 724 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:𝑇1-1𝑆)
63 f1cnv 6631 . . . . . . . . . 10 (𝑀:𝑇1-1𝑆𝑀:ran 𝑀1-1-onto𝑇)
64 f1of 6608 . . . . . . . . . 10 (𝑀:ran 𝑀1-1-onto𝑇𝑀:ran 𝑀𝑇)
6562, 63, 643syl 18 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:ran 𝑀𝑇)
66 fco 6524 . . . . . . . . 9 ((𝑐:𝑇⟶ℕ0𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℕ0)
6761, 65, 66syl2anc 586 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℕ0)
68 c0ex 10627 . . . . . . . . . 10 0 ∈ V
6968fconst 6558 . . . . . . . . 9 ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}
7069a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0})
71 disjdif 4419 . . . . . . . . 9 (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅
7271a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
73 fun 6533 . . . . . . . 8 ((((𝑐𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
7467, 70, 72, 73syl21anc 835 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
75 frn 6513 . . . . . . . . . . 11 (𝑀:𝑇𝑆 → ran 𝑀𝑆)
769, 10, 753syl 18 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → ran 𝑀𝑆)
7776ad2antrr 724 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ran 𝑀𝑆)
78 undif 4428 . . . . . . . . 9 (ran 𝑀𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
7977, 78sylib 220 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
80 0nn0 11904 . . . . . . . . . . 11 0 ∈ ℕ0
81 snssi 4733 . . . . . . . . . . 11 (0 ∈ ℕ0 → {0} ⊆ ℕ0)
8280, 81ax-mp 5 . . . . . . . . . 10 {0} ⊆ ℕ0
83 ssequn2 4157 . . . . . . . . . 10 ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
8482, 83mpbi 232 . . . . . . . . 9 (ℕ0 ∪ {0}) = ℕ0
8584a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ℕ0 ∪ {0}) = ℕ0)
8679, 85feq23d 6502 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
8774, 86mpbid 234 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)
88 elmapg 8411 . . . . . . . 8 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0m 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
892, 3, 88sylancr 589 . . . . . . 7 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0m 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
9089ad2antrr 724 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0m 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
9187, 90mpbird 259 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0m 𝑆))
92 simprl 769 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (𝑐𝑂))
93 resundir 5861 . . . . . . . . 9 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂))
94 resco 6096 . . . . . . . . . . 11 ((𝑐𝑀) ↾ 𝑂) = (𝑐 ∘ (𝑀𝑂))
95 cnvresid 6426 . . . . . . . . . . . . . 14 ( I ↾ 𝑂) = ( I ↾ 𝑂)
96 simpl2 1186 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑀:𝑇1-1𝑆)
97 df-f1 6353 . . . . . . . . . . . . . . . . 17 (𝑀:𝑇1-1𝑆 ↔ (𝑀:𝑇𝑆 ∧ Fun 𝑀))
9897simprbi 499 . . . . . . . . . . . . . . . 16 (𝑀:𝑇1-1𝑆 → Fun 𝑀)
99 funcnvres 6425 . . . . . . . . . . . . . . . 16 (Fun 𝑀(𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
10096, 98, 993syl 18 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
101 simpl3 1187 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
102101cnveqd 5739 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
103 df-ima 5561 . . . . . . . . . . . . . . . . 17 (𝑀𝑂) = ran (𝑀𝑂)
104101rneqd 5801 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ran (𝑀𝑂) = ran ( I ↾ 𝑂))
105 rnresi 5936 . . . . . . . . . . . . . . . . . 18 ran ( I ↾ 𝑂) = 𝑂
106104, 105syl6eq 2870 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ran (𝑀𝑂) = 𝑂)
107103, 106syl5eq 2866 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = 𝑂)
108107reseq2d 5846 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀 ↾ (𝑀𝑂)) = (𝑀𝑂))
109100, 102, 1083eqtr3d 2862 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ( I ↾ 𝑂) = (𝑀𝑂))
11095, 109syl5reqr 2869 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
111110coeq2d 5726 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐 ∘ ( I ↾ 𝑂)))
112 coires1 6110 . . . . . . . . . . . 12 (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐𝑂)
113111, 112syl6eq 2870 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐𝑂))
11494, 113syl5eq 2866 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ((𝑐𝑀) ↾ 𝑂) = (𝑐𝑂))
115 dmres 5868 . . . . . . . . . . . 12 dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0}))
11668snnz 4703 . . . . . . . . . . . . . . 15 {0} ≠ ∅
117 dmxp 5792 . . . . . . . . . . . . . . 15 ({0} ≠ ∅ → dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀))
118116, 117ax-mp 5 . . . . . . . . . . . . . 14 dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀)
119118ineq2i 4184 . . . . . . . . . . . . 13 (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀))
120 inss1 4203 . . . . . . . . . . . . . . 15 (𝑂𝑆) ⊆ 𝑂
121104, 105syl6req 2871 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑂 = ran (𝑀𝑂))
122 resss 5871 . . . . . . . . . . . . . . . . 17 (𝑀𝑂) ⊆ 𝑀
123 rnss 5802 . . . . . . . . . . . . . . . . 17 ((𝑀𝑂) ⊆ 𝑀 → ran (𝑀𝑂) ⊆ ran 𝑀)
124122, 123mp1i 13 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ran (𝑀𝑂) ⊆ ran 𝑀)
125121, 124eqsstrd 4003 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑂 ⊆ ran 𝑀)
126120, 125sstrid 3976 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑂𝑆) ⊆ ran 𝑀)
127 inssdif0 4327 . . . . . . . . . . . . . 14 ((𝑂𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
128126, 127sylib 220 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
129119, 128syl5eq 2866 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅)
130115, 129syl5eq 2866 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
131 relres 5875 . . . . . . . . . . . 12 Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)
132 reldm0 5791 . . . . . . . . . . . 12 (Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) → ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅))
133131, 132ax-mp 5 . . . . . . . . . . 11 ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
134130, 133sylibr 236 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
135114, 134uneq12d 4138 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐𝑂) ∪ ∅))
13693, 135syl5eq 2866 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐𝑂) ∪ ∅))
137 un0 4342 . . . . . . . 8 ((𝑐𝑂) ∪ ∅) = (𝑐𝑂)
138136, 137syl6req 2871 . . . . . . 7 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
139138adantr 483 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
14092, 139eqtrd 2854 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
141 fss 6520 . . . . . . . . . . . . 13 ((𝑐:𝑇⟶ℕ0 ∧ ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ)
14260, 34, 141sylancl 588 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑐:𝑇⟶ℤ)
143142adantr 483 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℤ)
144 fco 6524 . . . . . . . . . . 11 ((𝑐:𝑇⟶ℤ ∧ 𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℤ)
145143, 65, 144syl2anc 586 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℤ)
146 fun 6533 . . . . . . . . . 10 ((((𝑐𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
147145, 70, 72, 146syl21anc 835 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
148 0z 11984 . . . . . . . . . . . . 13 0 ∈ ℤ
149 snssi 4733 . . . . . . . . . . . . 13 (0 ∈ ℤ → {0} ⊆ ℤ)
150148, 149ax-mp 5 . . . . . . . . . . . 12 {0} ⊆ ℤ
151 ssequn2 4157 . . . . . . . . . . . 12 ({0} ⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ)
152150, 151mpbi 232 . . . . . . . . . . 11 (ℤ ∪ {0}) = ℤ
153152a1i 11 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ℤ ∪ {0}) = ℤ)
15479, 153feq23d 6502 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
155147, 154mpbid 234 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)
156 elmapg 8411 . . . . . . . . . 10 ((ℤ ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
15733, 3, 156sylancr 589 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
158157ad2antrr 724 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
159155, 158mpbird 259 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆))
160 coeq1 5721 . . . . . . . . 9 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑𝑀) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))
161160fveq2d 6667 . . . . . . . 8 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑𝑀)) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
162 fvex 6676 . . . . . . . 8 (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V
163161, 43, 162fvmpt 6761 . . . . . . 7 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
164159, 163syl 17 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
165 coundir 6094 . . . . . . . 8 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀))
166 coass 6111 . . . . . . . . . . 11 ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ (𝑀𝑀))
167 f1cocnv1 6637 . . . . . . . . . . . . 13 (𝑀:𝑇1-1𝑆 → (𝑀𝑀) = ( I ↾ 𝑇))
168167coeq2d 5726 . . . . . . . . . . . 12 (𝑀:𝑇1-1𝑆 → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
16962, 168syl 17 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
170166, 169syl5eq 2866 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇)))
171118ineq1i 4183 . . . . . . . . . . . . 13 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀)
172 incom 4176 . . . . . . . . . . . . 13 ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀))
173171, 172, 713eqtri 2846 . . . . . . . . . . . 12 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅
174 coeq0 6101 . . . . . . . . . . . 12 ((((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ ↔ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅)
175173, 174mpbir 233 . . . . . . . . . . 11 (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅
176175a1i 11 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅)
177170, 176uneq12d 4138 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅))
178 un0 4342 . . . . . . . . . 10 ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇))
179 fcoi1 6545 . . . . . . . . . . 11 (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
18061, 179syl 17 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
181178, 180syl5eq 2866 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐)
182177, 181eqtrd 2854 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐)
183165, 182syl5eq 2866 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐)
184183fveq2d 6667 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃𝑐))
185 simprr 771 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃𝑐) = 0)
186164, 184, 1853eqtrd 2858 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)
187 reseq1 5840 . . . . . . . 8 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
188187eqeq2d 2830 . . . . . . 7 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏𝑂) ↔ 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)))
189 fveqeq2 6672 . . . . . . 7 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))
190188, 189anbi12d 632 . . . . . 6 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)))
191190rspcev 3621 . . . . 5 ((((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0m 𝑆) ∧ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
19291, 140, 186, 191syl12anc 834 . . . 4 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
193192rexlimdva2 3285 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) → ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)))
19455, 193impbid 214 . 2 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
195194abbidv 2883 1 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1081   = wceq 1530  wcel 2107  {cab 2797  wne 3014  wrex 3137  Vcvv 3493  cdif 3931  cun 3932  cin 3933  wss 3934  c0 4289  {csn 4559  cmpt 5137   I cid 5452   × cxp 5546  ccnv 5547  dom cdm 5548  ran crn 5549  cres 5550  cima 5551  ccom 5552  Rel wrel 5553  Fun wfun 6342  wf 6344  1-1wf1 6345  1-1-ontowf1o 6347  cfv 6348  (class class class)co 7148  m cmap 8398  0cc0 10529  0cn0 11889  cz 11973
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-i2m1 10597  ax-1ne0 10598  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-map 8400  df-neg 10865  df-nn 11631  df-n0 11890  df-z 11974
This theorem is referenced by:  eldioph2  39349  eldioph2b  39350
  Copyright terms: Public domain W3C validator