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 42318
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 483 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) → 𝑏 ∈ (ℕ0m 𝑆))
2 nn0ex 12511 . . . . . . . . . 10 0 ∈ V
3 simp1 1133 . . . . . . . . . . 11 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V)
43adantr 479 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) → 𝑆 ∈ V)
5 elmapg 8858 . . . . . . . . . 10 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0m 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
62, 4, 5sylancr 585 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) → (𝑏 ∈ (ℕ0m 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
71, 6mpbid 231 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) → 𝑏:𝑆⟶ℕ0)
87adantr 479 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0)
9 simp2 1134 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇1-1𝑆)
10 f1f 6793 . . . . . . . . 9 (𝑀:𝑇1-1𝑆𝑀:𝑇𝑆)
119, 10syl 17 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇𝑆)
1211ad2antrr 724 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑀:𝑇𝑆)
13 fco 6747 . . . . . . 7 ((𝑏:𝑆⟶ℕ0𝑀:𝑇𝑆) → (𝑏𝑀):𝑇⟶ℕ0)
148, 12, 13syl2anc 582 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀):𝑇⟶ℕ0)
15 f1dmex 7961 . . . . . . . . 9 ((𝑀:𝑇1-1𝑆𝑆 ∈ V) → 𝑇 ∈ V)
169, 3, 15syl2anc 582 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V)
1716ad2antrr 724 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V)
18 elmapg 8858 . . . . . . 7 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏𝑀) ∈ (ℕ0m 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
192, 17, 18sylancr 585 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ∈ (ℕ0m 𝑇) ↔ (𝑏𝑀):𝑇⟶ℕ0))
2014, 19mpbird 256 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏𝑀) ∈ (ℕ0m 𝑇))
21 simprl 769 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏𝑂))
22 resco 6256 . . . . . . 7 ((𝑏𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀𝑂))
23 simpll3 1211 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑀𝑂) = ( I ↾ 𝑂))
2423coeq2d 5865 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏 ∘ ( I ↾ 𝑂)))
25 coires1 6270 . . . . . . . 8 (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏𝑂)
2624, 25eqtrdi 2781 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀𝑂)) = (𝑏𝑂))
2722, 26eqtrid 2777 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ((𝑏𝑀) ↾ 𝑂) = (𝑏𝑂))
2821, 27eqtr4d 2768 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏𝑀) ↾ 𝑂))
29 simpll1 1209 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V)
30 oveq2 7427 . . . . . . . . . . 11 (𝑎 = 𝑆 → (ℕ0m 𝑎) = (ℕ0m 𝑆))
31 oveq2 7427 . . . . . . . . . . 11 (𝑎 = 𝑆 → (ℤ ↑m 𝑎) = (ℤ ↑m 𝑆))
3230, 31sseq12d 4010 . . . . . . . . . 10 (𝑎 = 𝑆 → ((ℕ0m 𝑎) ⊆ (ℤ ↑m 𝑎) ↔ (ℕ0m 𝑆) ⊆ (ℤ ↑m 𝑆)))
33 zex 12600 . . . . . . . . . . 11 ℤ ∈ V
34 nn0ssz 12614 . . . . . . . . . . 11 0 ⊆ ℤ
35 mapss 8908 . . . . . . . . . . 11 ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0m 𝑎) ⊆ (ℤ ↑m 𝑎))
3633, 34, 35mp2an 690 . . . . . . . . . 10 (ℕ0m 𝑎) ⊆ (ℤ ↑m 𝑎)
3732, 36vtoclg 3532 . . . . . . . . 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 3977 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑m 𝑆))
41 coeq1 5860 . . . . . . . . 9 (𝑑 = 𝑏 → (𝑑𝑀) = (𝑏𝑀))
4241fveq2d 6900 . . . . . . . 8 (𝑑 = 𝑏 → (𝑃‘(𝑑𝑀)) = (𝑃‘(𝑏𝑀)))
43 eqid 2725 . . . . . . . 8 (𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀))) = (𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))
44 fvex 6909 . . . . . . . 8 (𝑃‘(𝑏𝑀)) ∈ V
4542, 43, 44fvmpt 7004 . . . . . . 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 2767 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏𝑀)) = 0)
49 reseq1 5979 . . . . . . . 8 (𝑐 = (𝑏𝑀) → (𝑐𝑂) = ((𝑏𝑀) ↾ 𝑂))
5049eqeq2d 2736 . . . . . . 7 (𝑐 = (𝑏𝑀) → (𝑎 = (𝑐𝑂) ↔ 𝑎 = ((𝑏𝑀) ↾ 𝑂)))
51 fveqeq2 6905 . . . . . . 7 (𝑐 = (𝑏𝑀) → ((𝑃𝑐) = 0 ↔ (𝑃‘(𝑏𝑀)) = 0))
5250, 51anbi12d 630 . . . . . 6 (𝑐 = (𝑏𝑀) → ((𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) ↔ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)))
5352rspcev 3606 . . . . 5 (((𝑏𝑀) ∈ (ℕ0m 𝑇) ∧ (𝑎 = ((𝑏𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5420, 28, 48, 53syl12anc 835 . . . 4 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0m 𝑆)) ∧ (𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0))
5554rexlimdva2 3146 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
56 simpr 483 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑐 ∈ (ℕ0m 𝑇))
5716adantr 479 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑇 ∈ V)
58 elmapg 8858 . . . . . . . . . . . 12 ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0m 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
592, 57, 58sylancr 585 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑐 ∈ (ℕ0m 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
6056, 59mpbid 231 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑐:𝑇⟶ℕ0)
6160adantr 479 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℕ0)
629ad2antrr 724 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:𝑇1-1𝑆)
63 f1cnv 6862 . . . . . . . . . 10 (𝑀:𝑇1-1𝑆𝑀:ran 𝑀1-1-onto𝑇)
64 f1of 6838 . . . . . . . . . 10 (𝑀:ran 𝑀1-1-onto𝑇𝑀:ran 𝑀𝑇)
6562, 63, 643syl 18 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑀:ran 𝑀𝑇)
66 fco 6747 . . . . . . . . 9 ((𝑐:𝑇⟶ℕ0𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℕ0)
6761, 65, 66syl2anc 582 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℕ0)
68 c0ex 11240 . . . . . . . . . 10 0 ∈ V
6968fconst 6783 . . . . . . . . 9 ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}
7069a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0})
71 disjdif 4473 . . . . . . . . 9 (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅
7271a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
73 fun 6759 . . . . . . . 8 ((((𝑐𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
7467, 70, 72, 73syl21anc 836 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
75 frn 6730 . . . . . . . . . . 11 (𝑀:𝑇𝑆 → ran 𝑀𝑆)
769, 10, 753syl 18 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → ran 𝑀𝑆)
7776ad2antrr 724 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ran 𝑀𝑆)
78 undif 4483 . . . . . . . . 9 (ran 𝑀𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
7977, 78sylib 217 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
80 0nn0 12520 . . . . . . . . . . 11 0 ∈ ℕ0
81 snssi 4813 . . . . . . . . . . 11 (0 ∈ ℕ0 → {0} ⊆ ℕ0)
8280, 81ax-mp 5 . . . . . . . . . 10 {0} ⊆ ℕ0
83 ssequn2 4181 . . . . . . . . . 10 ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
8482, 83mpbi 229 . . . . . . . . 9 (ℕ0 ∪ {0}) = ℕ0
8584a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ℕ0 ∪ {0}) = ℕ0)
8679, 85feq23d 6718 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
8774, 86mpbid 231 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)
88 elmapg 8858 . . . . . . . 8 ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0m 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
892, 3, 88sylancr 585 . . . . . . 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 256 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0m 𝑆))
92 simprl 769 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (𝑐𝑂))
93 resundir 6000 . . . . . . . . 9 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂))
94 resco 6256 . . . . . . . . . . 11 ((𝑐𝑀) ↾ 𝑂) = (𝑐 ∘ (𝑀𝑂))
95 simpl2 1189 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑀:𝑇1-1𝑆)
96 df-f1 6554 . . . . . . . . . . . . . . . . 17 (𝑀:𝑇1-1𝑆 ↔ (𝑀:𝑇𝑆 ∧ Fun 𝑀))
9796simprbi 495 . . . . . . . . . . . . . . . 16 (𝑀:𝑇1-1𝑆 → Fun 𝑀)
98 funcnvres 6632 . . . . . . . . . . . . . . . 16 (Fun 𝑀(𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
9995, 97, 983syl 18 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = (𝑀 ↾ (𝑀𝑂)))
100 simpl3 1190 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
101100cnveqd 5878 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
102 df-ima 5691 . . . . . . . . . . . . . . . . 17 (𝑀𝑂) = ran (𝑀𝑂)
103100rneqd 5940 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ran (𝑀𝑂) = ran ( I ↾ 𝑂))
104 rnresi 6079 . . . . . . . . . . . . . . . . . 18 ran ( I ↾ 𝑂) = 𝑂
105103, 104eqtrdi 2781 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ran (𝑀𝑂) = 𝑂)
106102, 105eqtrid 2777 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = 𝑂)
107106reseq2d 5985 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀 ↾ (𝑀𝑂)) = (𝑀𝑂))
10899, 101, 1073eqtr3d 2773 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ( I ↾ 𝑂) = (𝑀𝑂))
109 cnvresid 6633 . . . . . . . . . . . . . 14 ( I ↾ 𝑂) = ( I ↾ 𝑂)
110108, 109eqtr3di 2780 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑀𝑂) = ( I ↾ 𝑂))
111110coeq2d 5865 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐 ∘ ( I ↾ 𝑂)))
112 coires1 6270 . . . . . . . . . . . 12 (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐𝑂)
113111, 112eqtrdi 2781 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑐 ∘ (𝑀𝑂)) = (𝑐𝑂))
11494, 113eqtrid 2777 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ((𝑐𝑀) ↾ 𝑂) = (𝑐𝑂))
115 dmres 6017 . . . . . . . . . . . 12 dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0}))
11668snnz 4782 . . . . . . . . . . . . . . 15 {0} ≠ ∅
117 dmxp 5931 . . . . . . . . . . . . . . 15 ({0} ≠ ∅ → dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀))
118116, 117ax-mp 5 . . . . . . . . . . . . . 14 dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀)
119118ineq2i 4207 . . . . . . . . . . . . 13 (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀))
120 inss1 4227 . . . . . . . . . . . . . . 15 (𝑂𝑆) ⊆ 𝑂
121103, 104eqtr2di 2782 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑂 = ran (𝑀𝑂))
122 resss 6007 . . . . . . . . . . . . . . . . 17 (𝑀𝑂) ⊆ 𝑀
123 rnss 5941 . . . . . . . . . . . . . . . . 17 ((𝑀𝑂) ⊆ 𝑀 → ran (𝑀𝑂) ⊆ ran 𝑀)
124122, 123mp1i 13 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → ran (𝑀𝑂) ⊆ ran 𝑀)
125121, 124eqsstrd 4015 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑂 ⊆ ran 𝑀)
126120, 125sstrid 3988 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑂𝑆) ⊆ ran 𝑀)
127 inssdif0 4371 . . . . . . . . . . . . . 14 ((𝑂𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
128126, 127sylib 217 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
129119, 128eqtrid 2777 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅)
130115, 129eqtrid 2777 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
131 relres 6011 . . . . . . . . . . . 12 Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)
132 reldm0 5930 . . . . . . . . . . . 12 (Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) → ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅))
133131, 132ax-mp 5 . . . . . . . . . . 11 ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
134130, 133sylibr 233 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
135114, 134uneq12d 4161 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (((𝑐𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐𝑂) ∪ ∅))
13693, 135eqtrid 2777 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐𝑂) ∪ ∅))
137 un0 4392 . . . . . . . 8 ((𝑐𝑂) ∪ ∅) = (𝑐𝑂)
138136, 137eqtr2di 2782 . . . . . . 7 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
139138adantr 479 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
14092, 139eqtrd 2765 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
141 fss 6739 . . . . . . . . . . . . 13 ((𝑐:𝑇⟶ℕ0 ∧ ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ)
14260, 34, 141sylancl 584 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) → 𝑐:𝑇⟶ℤ)
143142adantr 479 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → 𝑐:𝑇⟶ℤ)
144 fco 6747 . . . . . . . . . . 11 ((𝑐:𝑇⟶ℤ ∧ 𝑀:ran 𝑀𝑇) → (𝑐𝑀):ran 𝑀⟶ℤ)
145143, 65, 144syl2anc 582 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐𝑀):ran 𝑀⟶ℤ)
146 fun 6759 . . . . . . . . . 10 ((((𝑐𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
147145, 70, 72, 146syl21anc 836 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
148 0z 12602 . . . . . . . . . . . . 13 0 ∈ ℤ
149 snssi 4813 . . . . . . . . . . . . 13 (0 ∈ ℤ → {0} ⊆ ℤ)
150148, 149ax-mp 5 . . . . . . . . . . . 12 {0} ⊆ ℤ
151 ssequn2 4181 . . . . . . . . . . . 12 ({0} ⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ)
152150, 151mpbi 229 . . . . . . . . . . 11 (ℤ ∪ {0}) = ℤ
153152a1i 11 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (ℤ ∪ {0}) = ℤ)
15479, 153feq23d 6718 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
155147, 154mpbid 231 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)
156 elmapg 8858 . . . . . . . . . 10 ((ℤ ∈ V ∧ 𝑆 ∈ V) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) ↔ ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
15733, 3, 156sylancr 585 . . . . . . . . 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 256 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆))
160 coeq1 5860 . . . . . . . . 9 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑𝑀) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))
161160fveq2d 6900 . . . . . . . 8 (𝑑 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑𝑀)) = (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
162 fvex 6909 . . . . . . . 8 (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V
163161, 43, 162fvmpt 7004 . . . . . . 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 6254 . . . . . . . 8 (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀))
166 coass 6271 . . . . . . . . . . 11 ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ (𝑀𝑀))
167 f1cocnv1 6868 . . . . . . . . . . . . 13 (𝑀:𝑇1-1𝑆 → (𝑀𝑀) = ( I ↾ 𝑇))
168167coeq2d 5865 . . . . . . . . . . . 12 (𝑀:𝑇1-1𝑆 → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
16962, 168syl 17 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ (𝑀𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
170166, 169eqtrid 2777 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇)))
171118ineq1i 4206 . . . . . . . . . . . . 13 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀)
172 incom 4199 . . . . . . . . . . . . 13 ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀))
173171, 172, 713eqtri 2757 . . . . . . . . . . . 12 (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅
174 coeq0 6261 . . . . . . . . . . . 12 ((((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ ↔ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅)
175173, 174mpbir 230 . . . . . . . . . . 11 (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅
176175a1i 11 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅)
177170, 176uneq12d 4161 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅))
178 un0 4392 . . . . . . . . . 10 ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇))
179 fcoi1 6771 . . . . . . . . . . 11 (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
18061, 179syl 17 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
181178, 180eqtrid 2777 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐)
182177, 181eqtrd 2765 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐)
183165, 182eqtrid 2777 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐)
184183fveq2d 6900 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃‘(((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃𝑐))
185 simprr 771 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → (𝑃𝑐) = 0)
186164, 184, 1853eqtrd 2769 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)
187 reseq1 5979 . . . . . . . 8 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏𝑂) = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
188187eqeq2d 2736 . . . . . . 7 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏𝑂) ↔ 𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)))
189 fveqeq2 6905 . . . . . . 7 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))
190188, 189anbi12d 630 . . . . . 6 (𝑏 = ((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)))
191190rspcev 3606 . . . . 5 ((((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0m 𝑆) ∧ (𝑎 = (((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘((𝑐𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
19291, 140, 186, 191syl12anc 835 . . . 4 ((((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0m 𝑇)) ∧ (𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)) → ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0))
193192rexlimdva2 3146 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0) → ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)))
19455, 193impbid 211 . 2 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)))
195194abbidv 2794 1 ((𝑆 ∈ V ∧ 𝑀:𝑇1-1𝑆 ∧ (𝑀𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0m 𝑆)(𝑎 = (𝑏𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0m 𝑇)(𝑎 = (𝑐𝑂) ∧ (𝑃𝑐) = 0)})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wcel 2098  {cab 2702  wne 2929  wrex 3059  Vcvv 3461  cdif 3941  cun 3942  cin 3943  wss 3944  c0 4322  {csn 4630  cmpt 5232   I cid 5575   × cxp 5676  ccnv 5677  dom cdm 5678  ran crn 5679  cres 5680  cima 5681  ccom 5682  Rel wrel 5683  Fun wfun 6543  wf 6545  1-1wf1 6546  1-1-ontowf1o 6548  cfv 6549  (class class class)co 7419  m cmap 8845  0cc0 11140  0cn0 12505  cz 12591
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 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-cnex 11196  ax-resscn 11197  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-i2m1 11208  ax-1ne0 11209  ax-rnegex 11211  ax-rrecex 11212  ax-cnre 11213
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-iun 4999  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-map 8847  df-neg 11479  df-nn 12246  df-n0 12506  df-z 12592
This theorem is referenced by:  eldioph2  42321  eldioph2b  42322
  Copyright terms: Public domain W3C validator