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 41799
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 β†Ύ 𝑂)) β†’ {π‘Ž ∣ βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)} = {π‘Ž ∣ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)})
Distinct variable groups:   𝑆,π‘Ž,𝑏,𝑐,𝑑   𝑇,π‘Ž,𝑏,𝑐,𝑑   𝑀,π‘Ž,𝑏,𝑐,𝑑   𝑂,π‘Ž,𝑏,𝑐,𝑑   𝑃,𝑏,𝑐,𝑑
Allowed substitution hint:   𝑃(π‘Ž)
Proof of Theorem diophrw
StepHypRef Expression
1 simpr 483 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) β†’ 𝑏 ∈ (β„•0 ↑m 𝑆))
2 nn0ex 12482 . . . . . . . . . 10 β„•0 ∈ V
3 simp1 1134 . . . . . . . . . . 11 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ 𝑆 ∈ V)
43adantr 479 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) β†’ 𝑆 ∈ V)
5 elmapg 8835 . . . . . . . . . 10 ((β„•0 ∈ V ∧ 𝑆 ∈ V) β†’ (𝑏 ∈ (β„•0 ↑m 𝑆) ↔ 𝑏:π‘†βŸΆβ„•0))
62, 4, 5sylancr 585 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) β†’ (𝑏 ∈ (β„•0 ↑m 𝑆) ↔ 𝑏:π‘†βŸΆβ„•0))
71, 6mpbid 231 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) β†’ 𝑏:π‘†βŸΆβ„•0)
87adantr 479 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑏:π‘†βŸΆβ„•0)
9 simp2 1135 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ 𝑀:𝑇–1-1→𝑆)
10 f1f 6786 . . . . . . . . 9 (𝑀:𝑇–1-1→𝑆 β†’ 𝑀:π‘‡βŸΆπ‘†)
119, 10syl 17 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ 𝑀:π‘‡βŸΆπ‘†)
1211ad2antrr 722 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑀:π‘‡βŸΆπ‘†)
13 fco 6740 . . . . . . 7 ((𝑏:π‘†βŸΆβ„•0 ∧ 𝑀:π‘‡βŸΆπ‘†) β†’ (𝑏 ∘ 𝑀):π‘‡βŸΆβ„•0)
148, 12, 13syl2anc 582 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑏 ∘ 𝑀):π‘‡βŸΆβ„•0)
15 f1dmex 7945 . . . . . . . . 9 ((𝑀:𝑇–1-1→𝑆 ∧ 𝑆 ∈ V) β†’ 𝑇 ∈ V)
169, 3, 15syl2anc 582 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ 𝑇 ∈ V)
1716ad2antrr 722 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑇 ∈ V)
18 elmapg 8835 . . . . . . 7 ((β„•0 ∈ V ∧ 𝑇 ∈ V) β†’ ((𝑏 ∘ 𝑀) ∈ (β„•0 ↑m 𝑇) ↔ (𝑏 ∘ 𝑀):π‘‡βŸΆβ„•0))
192, 17, 18sylancr 585 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ ((𝑏 ∘ 𝑀) ∈ (β„•0 ↑m 𝑇) ↔ (𝑏 ∘ 𝑀):π‘‡βŸΆβ„•0))
2014, 19mpbird 256 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑏 ∘ 𝑀) ∈ (β„•0 ↑m 𝑇))
21 simprl 767 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ π‘Ž = (𝑏 β†Ύ 𝑂))
22 resco 6248 . . . . . . 7 ((𝑏 ∘ 𝑀) β†Ύ 𝑂) = (𝑏 ∘ (𝑀 β†Ύ 𝑂))
23 simpll3 1212 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂))
2423coeq2d 5861 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑏 ∘ (𝑀 β†Ύ 𝑂)) = (𝑏 ∘ ( I β†Ύ 𝑂)))
25 coires1 6262 . . . . . . . 8 (𝑏 ∘ ( I β†Ύ 𝑂)) = (𝑏 β†Ύ 𝑂)
2624, 25eqtrdi 2786 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑏 ∘ (𝑀 β†Ύ 𝑂)) = (𝑏 β†Ύ 𝑂))
2722, 26eqtrid 2782 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ ((𝑏 ∘ 𝑀) β†Ύ 𝑂) = (𝑏 β†Ύ 𝑂))
2821, 27eqtr4d 2773 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ π‘Ž = ((𝑏 ∘ 𝑀) β†Ύ 𝑂))
29 simpll1 1210 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑆 ∈ V)
30 oveq2 7419 . . . . . . . . . . 11 (π‘Ž = 𝑆 β†’ (β„•0 ↑m π‘Ž) = (β„•0 ↑m 𝑆))
31 oveq2 7419 . . . . . . . . . . 11 (π‘Ž = 𝑆 β†’ (β„€ ↑m π‘Ž) = (β„€ ↑m 𝑆))
3230, 31sseq12d 4014 . . . . . . . . . 10 (π‘Ž = 𝑆 β†’ ((β„•0 ↑m π‘Ž) βŠ† (β„€ ↑m π‘Ž) ↔ (β„•0 ↑m 𝑆) βŠ† (β„€ ↑m 𝑆)))
33 zex 12571 . . . . . . . . . . 11 β„€ ∈ V
34 nn0ssz 12585 . . . . . . . . . . 11 β„•0 βŠ† β„€
35 mapss 8885 . . . . . . . . . . 11 ((β„€ ∈ V ∧ β„•0 βŠ† β„€) β†’ (β„•0 ↑m π‘Ž) βŠ† (β„€ ↑m π‘Ž))
3633, 34, 35mp2an 688 . . . . . . . . . 10 (β„•0 ↑m π‘Ž) βŠ† (β„€ ↑m π‘Ž)
3732, 36vtoclg 3541 . . . . . . . . 9 (𝑆 ∈ V β†’ (β„•0 ↑m 𝑆) βŠ† (β„€ ↑m 𝑆))
3829, 37syl 17 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (β„•0 ↑m 𝑆) βŠ† (β„€ ↑m 𝑆))
39 simplr 765 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑏 ∈ (β„•0 ↑m 𝑆))
4038, 39sseldd 3982 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑏 ∈ (β„€ ↑m 𝑆))
41 coeq1 5856 . . . . . . . . 9 (𝑑 = 𝑏 β†’ (𝑑 ∘ 𝑀) = (𝑏 ∘ 𝑀))
4241fveq2d 6894 . . . . . . . 8 (𝑑 = 𝑏 β†’ (π‘ƒβ€˜(𝑑 ∘ 𝑀)) = (π‘ƒβ€˜(𝑏 ∘ 𝑀)))
43 eqid 2730 . . . . . . . 8 (𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀))) = (𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))
44 fvex 6903 . . . . . . . 8 (π‘ƒβ€˜(𝑏 ∘ 𝑀)) ∈ V
4542, 43, 44fvmpt 6997 . . . . . . 7 (𝑏 ∈ (β„€ ↑m 𝑆) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = (π‘ƒβ€˜(𝑏 ∘ 𝑀)))
4640, 45syl 17 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = (π‘ƒβ€˜(𝑏 ∘ 𝑀)))
47 simprr 769 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)
4846, 47eqtr3d 2772 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (π‘ƒβ€˜(𝑏 ∘ 𝑀)) = 0)
49 reseq1 5974 . . . . . . . 8 (𝑐 = (𝑏 ∘ 𝑀) β†’ (𝑐 β†Ύ 𝑂) = ((𝑏 ∘ 𝑀) β†Ύ 𝑂))
5049eqeq2d 2741 . . . . . . 7 (𝑐 = (𝑏 ∘ 𝑀) β†’ (π‘Ž = (𝑐 β†Ύ 𝑂) ↔ π‘Ž = ((𝑏 ∘ 𝑀) β†Ύ 𝑂)))
51 fveqeq2 6899 . . . . . . 7 (𝑐 = (𝑏 ∘ 𝑀) β†’ ((π‘ƒβ€˜π‘) = 0 ↔ (π‘ƒβ€˜(𝑏 ∘ 𝑀)) = 0))
5250, 51anbi12d 629 . . . . . 6 (𝑐 = (𝑏 ∘ 𝑀) β†’ ((π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0) ↔ (π‘Ž = ((𝑏 ∘ 𝑀) β†Ύ 𝑂) ∧ (π‘ƒβ€˜(𝑏 ∘ 𝑀)) = 0)))
5352rspcev 3611 . . . . 5 (((𝑏 ∘ 𝑀) ∈ (β„•0 ↑m 𝑇) ∧ (π‘Ž = ((𝑏 ∘ 𝑀) β†Ύ 𝑂) ∧ (π‘ƒβ€˜(𝑏 ∘ 𝑀)) = 0)) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0))
5420, 28, 48, 53syl12anc 833 . . . 4 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0))
5554rexlimdva2 3155 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ (βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)))
56 simpr 483 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑐 ∈ (β„•0 ↑m 𝑇))
5716adantr 479 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑇 ∈ V)
58 elmapg 8835 . . . . . . . . . . . 12 ((β„•0 ∈ V ∧ 𝑇 ∈ V) β†’ (𝑐 ∈ (β„•0 ↑m 𝑇) ↔ 𝑐:π‘‡βŸΆβ„•0))
592, 57, 58sylancr 585 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑐 ∈ (β„•0 ↑m 𝑇) ↔ 𝑐:π‘‡βŸΆβ„•0))
6056, 59mpbid 231 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑐:π‘‡βŸΆβ„•0)
6160adantr 479 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ 𝑐:π‘‡βŸΆβ„•0)
629ad2antrr 722 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ 𝑀:𝑇–1-1→𝑆)
63 f1cnv 6856 . . . . . . . . . 10 (𝑀:𝑇–1-1→𝑆 β†’ ◑𝑀:ran 𝑀–1-1-onto→𝑇)
64 f1of 6832 . . . . . . . . . 10 (◑𝑀:ran 𝑀–1-1-onto→𝑇 β†’ ◑𝑀:ran π‘€βŸΆπ‘‡)
6562, 63, 643syl 18 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ◑𝑀:ran π‘€βŸΆπ‘‡)
66 fco 6740 . . . . . . . . 9 ((𝑐:π‘‡βŸΆβ„•0 ∧ ◑𝑀:ran π‘€βŸΆπ‘‡) β†’ (𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„•0)
6761, 65, 66syl2anc 582 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„•0)
68 c0ex 11212 . . . . . . . . . 10 0 ∈ V
6968fconst 6776 . . . . . . . . 9 ((𝑆 βˆ– ran 𝑀) Γ— {0}):(𝑆 βˆ– ran 𝑀)⟢{0}
7069a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑆 βˆ– ran 𝑀) Γ— {0}):(𝑆 βˆ– ran 𝑀)⟢{0})
71 disjdif 4470 . . . . . . . . 9 (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…
7271a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…)
73 fun 6752 . . . . . . . 8 ((((𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„•0 ∧ ((𝑆 βˆ– ran 𝑀) Γ— {0}):(𝑆 βˆ– ran 𝑀)⟢{0}) ∧ (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„•0 βˆͺ {0}))
7467, 70, 72, 73syl21anc 834 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„•0 βˆͺ {0}))
75 frn 6723 . . . . . . . . . . 11 (𝑀:π‘‡βŸΆπ‘† β†’ ran 𝑀 βŠ† 𝑆)
769, 10, 753syl 18 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ ran 𝑀 βŠ† 𝑆)
7776ad2antrr 722 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ran 𝑀 βŠ† 𝑆)
78 undif 4480 . . . . . . . . 9 (ran 𝑀 βŠ† 𝑆 ↔ (ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀)) = 𝑆)
7977, 78sylib 217 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀)) = 𝑆)
80 0nn0 12491 . . . . . . . . . . 11 0 ∈ β„•0
81 snssi 4810 . . . . . . . . . . 11 (0 ∈ β„•0 β†’ {0} βŠ† β„•0)
8280, 81ax-mp 5 . . . . . . . . . 10 {0} βŠ† β„•0
83 ssequn2 4182 . . . . . . . . . 10 ({0} βŠ† β„•0 ↔ (β„•0 βˆͺ {0}) = β„•0)
8482, 83mpbi 229 . . . . . . . . 9 (β„•0 βˆͺ {0}) = β„•0
8584a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (β„•0 βˆͺ {0}) = β„•0)
8679, 85feq23d 6711 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„•0 βˆͺ {0}) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„•0))
8774, 86mpbid 231 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„•0)
88 elmapg 8835 . . . . . . . 8 ((β„•0 ∈ V ∧ 𝑆 ∈ V) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„•0))
892, 3, 88sylancr 585 . . . . . . 7 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„•0))
9089ad2antrr 722 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„•0))
9187, 90mpbird 256 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆))
92 simprl 767 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ π‘Ž = (𝑐 β†Ύ 𝑂))
93 resundir 5995 . . . . . . . . 9 (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂) = (((𝑐 ∘ ◑𝑀) β†Ύ 𝑂) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂))
94 resco 6248 . . . . . . . . . . 11 ((𝑐 ∘ ◑𝑀) β†Ύ 𝑂) = (𝑐 ∘ (◑𝑀 β†Ύ 𝑂))
95 simpl2 1190 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑀:𝑇–1-1→𝑆)
96 df-f1 6547 . . . . . . . . . . . . . . . . 17 (𝑀:𝑇–1-1→𝑆 ↔ (𝑀:π‘‡βŸΆπ‘† ∧ Fun ◑𝑀))
9796simprbi 495 . . . . . . . . . . . . . . . 16 (𝑀:𝑇–1-1→𝑆 β†’ Fun ◑𝑀)
98 funcnvres 6625 . . . . . . . . . . . . . . . 16 (Fun ◑𝑀 β†’ β—‘(𝑀 β†Ύ 𝑂) = (◑𝑀 β†Ύ (𝑀 β€œ 𝑂)))
9995, 97, 983syl 18 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ β—‘(𝑀 β†Ύ 𝑂) = (◑𝑀 β†Ύ (𝑀 β€œ 𝑂)))
100 simpl3 1191 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂))
101100cnveqd 5874 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ β—‘(𝑀 β†Ύ 𝑂) = β—‘( I β†Ύ 𝑂))
102 df-ima 5688 . . . . . . . . . . . . . . . . 17 (𝑀 β€œ 𝑂) = ran (𝑀 β†Ύ 𝑂)
103100rneqd 5936 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ ran (𝑀 β†Ύ 𝑂) = ran ( I β†Ύ 𝑂))
104 rnresi 6073 . . . . . . . . . . . . . . . . . 18 ran ( I β†Ύ 𝑂) = 𝑂
105103, 104eqtrdi 2786 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ ran (𝑀 β†Ύ 𝑂) = 𝑂)
106102, 105eqtrid 2782 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑀 β€œ 𝑂) = 𝑂)
107106reseq2d 5980 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (◑𝑀 β†Ύ (𝑀 β€œ 𝑂)) = (◑𝑀 β†Ύ 𝑂))
10899, 101, 1073eqtr3d 2778 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ β—‘( I β†Ύ 𝑂) = (◑𝑀 β†Ύ 𝑂))
109 cnvresid 6626 . . . . . . . . . . . . . 14 β—‘( I β†Ύ 𝑂) = ( I β†Ύ 𝑂)
110108, 109eqtr3di 2785 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (◑𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂))
111110coeq2d 5861 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑐 ∘ (◑𝑀 β†Ύ 𝑂)) = (𝑐 ∘ ( I β†Ύ 𝑂)))
112 coires1 6262 . . . . . . . . . . . 12 (𝑐 ∘ ( I β†Ύ 𝑂)) = (𝑐 β†Ύ 𝑂)
113111, 112eqtrdi 2786 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑐 ∘ (◑𝑀 β†Ύ 𝑂)) = (𝑐 β†Ύ 𝑂))
11494, 113eqtrid 2782 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ ((𝑐 ∘ ◑𝑀) β†Ύ 𝑂) = (𝑐 β†Ύ 𝑂))
115 dmres 6002 . . . . . . . . . . . 12 dom (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂) = (𝑂 ∩ dom ((𝑆 βˆ– ran 𝑀) Γ— {0}))
11668snnz 4779 . . . . . . . . . . . . . . 15 {0} β‰  βˆ…
117 dmxp 5927 . . . . . . . . . . . . . . 15 ({0} β‰  βˆ… β†’ dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) = (𝑆 βˆ– ran 𝑀))
118116, 117ax-mp 5 . . . . . . . . . . . . . 14 dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) = (𝑆 βˆ– ran 𝑀)
119118ineq2i 4208 . . . . . . . . . . . . 13 (𝑂 ∩ dom ((𝑆 βˆ– ran 𝑀) Γ— {0})) = (𝑂 ∩ (𝑆 βˆ– ran 𝑀))
120 inss1 4227 . . . . . . . . . . . . . . 15 (𝑂 ∩ 𝑆) βŠ† 𝑂
121103, 104eqtr2di 2787 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑂 = ran (𝑀 β†Ύ 𝑂))
122 resss 6005 . . . . . . . . . . . . . . . . 17 (𝑀 β†Ύ 𝑂) βŠ† 𝑀
123 rnss 5937 . . . . . . . . . . . . . . . . 17 ((𝑀 β†Ύ 𝑂) βŠ† 𝑀 β†’ ran (𝑀 β†Ύ 𝑂) βŠ† ran 𝑀)
124122, 123mp1i 13 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ ran (𝑀 β†Ύ 𝑂) βŠ† ran 𝑀)
125121, 124eqsstrd 4019 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑂 βŠ† ran 𝑀)
126120, 125sstrid 3992 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑂 ∩ 𝑆) βŠ† ran 𝑀)
127 inssdif0 4368 . . . . . . . . . . . . . 14 ((𝑂 ∩ 𝑆) βŠ† ran 𝑀 ↔ (𝑂 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…)
128126, 127sylib 217 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑂 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…)
129119, 128eqtrid 2782 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑂 ∩ dom ((𝑆 βˆ– ran 𝑀) Γ— {0})) = βˆ…)
130115, 129eqtrid 2782 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ dom (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂) = βˆ…)
131 relres 6009 . . . . . . . . . . . 12 Rel (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂)
132 reldm0 5926 . . . . . . . . . . . 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 β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂) = βˆ…)
135114, 134uneq12d 4163 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (((𝑐 ∘ ◑𝑀) β†Ύ 𝑂) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂)) = ((𝑐 β†Ύ 𝑂) βˆͺ βˆ…))
13693, 135eqtrid 2782 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂) = ((𝑐 β†Ύ 𝑂) βˆͺ βˆ…))
137 un0 4389 . . . . . . . 8 ((𝑐 β†Ύ 𝑂) βˆͺ βˆ…) = (𝑐 β†Ύ 𝑂)
138136, 137eqtr2di 2787 . . . . . . 7 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑐 β†Ύ 𝑂) = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂))
139138adantr 479 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 β†Ύ 𝑂) = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂))
14092, 139eqtrd 2770 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ π‘Ž = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂))
141 fss 6733 . . . . . . . . . . . . 13 ((𝑐:π‘‡βŸΆβ„•0 ∧ β„•0 βŠ† β„€) β†’ 𝑐:π‘‡βŸΆβ„€)
14260, 34, 141sylancl 584 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑐:π‘‡βŸΆβ„€)
143142adantr 479 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ 𝑐:π‘‡βŸΆβ„€)
144 fco 6740 . . . . . . . . . . 11 ((𝑐:π‘‡βŸΆβ„€ ∧ ◑𝑀:ran π‘€βŸΆπ‘‡) β†’ (𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„€)
145143, 65, 144syl2anc 582 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„€)
146 fun 6752 . . . . . . . . . 10 ((((𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„€ ∧ ((𝑆 βˆ– ran 𝑀) Γ— {0}):(𝑆 βˆ– ran 𝑀)⟢{0}) ∧ (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„€ βˆͺ {0}))
147145, 70, 72, 146syl21anc 834 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„€ βˆͺ {0}))
148 0z 12573 . . . . . . . . . . . . 13 0 ∈ β„€
149 snssi 4810 . . . . . . . . . . . . 13 (0 ∈ β„€ β†’ {0} βŠ† β„€)
150148, 149ax-mp 5 . . . . . . . . . . . 12 {0} βŠ† β„€
151 ssequn2 4182 . . . . . . . . . . . 12 ({0} βŠ† β„€ ↔ (β„€ βˆͺ {0}) = β„€)
152150, 151mpbi 229 . . . . . . . . . . 11 (β„€ βˆͺ {0}) = β„€
153152a1i 11 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (β„€ βˆͺ {0}) = β„€)
15479, 153feq23d 6711 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„€ βˆͺ {0}) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„€))
155147, 154mpbid 231 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„€)
156 elmapg 8835 . . . . . . . . . 10 ((β„€ ∈ V ∧ 𝑆 ∈ V) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„€))
15733, 3, 156sylancr 585 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„€))
158157ad2antrr 722 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„€))
159155, 158mpbird 256 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆))
160 coeq1 5856 . . . . . . . . 9 (𝑑 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (𝑑 ∘ 𝑀) = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀))
161160fveq2d 6894 . . . . . . . 8 (𝑑 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (π‘ƒβ€˜(𝑑 ∘ 𝑀)) = (π‘ƒβ€˜(((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀)))
162 fvex 6903 . . . . . . . 8 (π‘ƒβ€˜(((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀)) ∈ V
163161, 43, 162fvmpt 6997 . . . . . . 7 (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = (π‘ƒβ€˜(((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀)))
164159, 163syl 17 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = (π‘ƒβ€˜(((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀)))
165 coundir 6246 . . . . . . . 8 (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀) = (((𝑐 ∘ ◑𝑀) ∘ 𝑀) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀))
166 coass 6263 . . . . . . . . . . 11 ((𝑐 ∘ ◑𝑀) ∘ 𝑀) = (𝑐 ∘ (◑𝑀 ∘ 𝑀))
167 f1cocnv1 6862 . . . . . . . . . . . . 13 (𝑀:𝑇–1-1→𝑆 β†’ (◑𝑀 ∘ 𝑀) = ( I β†Ύ 𝑇))
168167coeq2d 5861 . . . . . . . . . . . 12 (𝑀:𝑇–1-1→𝑆 β†’ (𝑐 ∘ (◑𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I β†Ύ 𝑇)))
16962, 168syl 17 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 ∘ (◑𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I β†Ύ 𝑇)))
170166, 169eqtrid 2782 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) ∘ 𝑀) = (𝑐 ∘ ( I β†Ύ 𝑇)))
171118ineq1i 4207 . . . . . . . . . . . . 13 (dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) ∩ ran 𝑀) = ((𝑆 βˆ– ran 𝑀) ∩ ran 𝑀)
172 incom 4200 . . . . . . . . . . . . 13 ((𝑆 βˆ– ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀))
173171, 172, 713eqtri 2762 . . . . . . . . . . . 12 (dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) ∩ ran 𝑀) = βˆ…
174 coeq0 6253 . . . . . . . . . . . 12 ((((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀) = βˆ… ↔ (dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) ∩ ran 𝑀) = βˆ…)
175173, 174mpbir 230 . . . . . . . . . . 11 (((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀) = βˆ…
176175a1i 11 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀) = βˆ…)
177170, 176uneq12d 4163 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) ∘ 𝑀) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I β†Ύ 𝑇)) βˆͺ βˆ…))
178 un0 4389 . . . . . . . . . 10 ((𝑐 ∘ ( I β†Ύ 𝑇)) βˆͺ βˆ…) = (𝑐 ∘ ( I β†Ύ 𝑇))
179 fcoi1 6764 . . . . . . . . . . 11 (𝑐:π‘‡βŸΆβ„•0 β†’ (𝑐 ∘ ( I β†Ύ 𝑇)) = 𝑐)
18061, 179syl 17 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 ∘ ( I β†Ύ 𝑇)) = 𝑐)
181178, 180eqtrid 2782 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ( I β†Ύ 𝑇)) βˆͺ βˆ…) = 𝑐)
182177, 181eqtrd 2770 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) ∘ 𝑀) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀)) = 𝑐)
183165, 182eqtrid 2782 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀) = 𝑐)
184183fveq2d 6894 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (π‘ƒβ€˜(((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀)) = (π‘ƒβ€˜π‘))
185 simprr 769 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (π‘ƒβ€˜π‘) = 0)
186164, 184, 1853eqtrd 2774 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = 0)
187 reseq1 5974 . . . . . . . 8 (𝑏 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (𝑏 β†Ύ 𝑂) = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂))
188187eqeq2d 2741 . . . . . . 7 (𝑏 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (π‘Ž = (𝑏 β†Ύ 𝑂) ↔ π‘Ž = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂)))
189 fveqeq2 6899 . . . . . . 7 (𝑏 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0 ↔ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = 0))
190188, 189anbi12d 629 . . . . . 6 (𝑏 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ ((π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0) ↔ (π‘Ž = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = 0)))
191190rspcev 3611 . . . . 5 ((((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆) ∧ (π‘Ž = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = 0)) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0))
19291, 140, 186, 191syl12anc 833 . . . 4 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0))
193192rexlimdva2 3155 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ (βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)))
19455, 193impbid 211 . 2 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ (βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0) ↔ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)))
195194abbidv 2799 1 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ {π‘Ž ∣ βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)} = {π‘Ž ∣ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  {cab 2707   β‰  wne 2938  βˆƒwrex 3068  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  {csn 4627   ↦ cmpt 5230   I cid 5572   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   ∘ ccom 5679  Rel wrel 5680  Fun wfun 6536  βŸΆwf 6538  β€“1-1β†’wf1 6539  β€“1-1-ontoβ†’wf1o 6541  β€˜cfv 6542  (class class class)co 7411   ↑m cmap 8822  0cc0 11112  β„•0cn0 12476  β„€cz 12562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-i2m1 11180  ax-1ne0 11181  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-map 8824  df-neg 11451  df-nn 12217  df-n0 12477  df-z 12563
This theorem is referenced by:  eldioph2  41802  eldioph2b  41803
  Copyright terms: Public domain W3C validator