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 41483
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 486 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) β†’ 𝑏 ∈ (β„•0 ↑m 𝑆))
2 nn0ex 12475 . . . . . . . . . 10 β„•0 ∈ V
3 simp1 1137 . . . . . . . . . . 11 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ 𝑆 ∈ V)
43adantr 482 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) β†’ 𝑆 ∈ V)
5 elmapg 8830 . . . . . . . . . 10 ((β„•0 ∈ V ∧ 𝑆 ∈ V) β†’ (𝑏 ∈ (β„•0 ↑m 𝑆) ↔ 𝑏:π‘†βŸΆβ„•0))
62, 4, 5sylancr 588 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) β†’ (𝑏 ∈ (β„•0 ↑m 𝑆) ↔ 𝑏:π‘†βŸΆβ„•0))
71, 6mpbid 231 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) β†’ 𝑏:π‘†βŸΆβ„•0)
87adantr 482 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑏:π‘†βŸΆβ„•0)
9 simp2 1138 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ 𝑀:𝑇–1-1→𝑆)
10 f1f 6785 . . . . . . . . 9 (𝑀:𝑇–1-1→𝑆 β†’ 𝑀:π‘‡βŸΆπ‘†)
119, 10syl 17 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ 𝑀:π‘‡βŸΆπ‘†)
1211ad2antrr 725 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑀:π‘‡βŸΆπ‘†)
13 fco 6739 . . . . . . 7 ((𝑏:π‘†βŸΆβ„•0 ∧ 𝑀:π‘‡βŸΆπ‘†) β†’ (𝑏 ∘ 𝑀):π‘‡βŸΆβ„•0)
148, 12, 13syl2anc 585 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑏 ∘ 𝑀):π‘‡βŸΆβ„•0)
15 f1dmex 7940 . . . . . . . . 9 ((𝑀:𝑇–1-1→𝑆 ∧ 𝑆 ∈ V) β†’ 𝑇 ∈ V)
169, 3, 15syl2anc 585 . . . . . . . 8 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ 𝑇 ∈ V)
1716ad2antrr 725 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑇 ∈ V)
18 elmapg 8830 . . . . . . 7 ((β„•0 ∈ V ∧ 𝑇 ∈ V) β†’ ((𝑏 ∘ 𝑀) ∈ (β„•0 ↑m 𝑇) ↔ (𝑏 ∘ 𝑀):π‘‡βŸΆβ„•0))
192, 17, 18sylancr 588 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ ((𝑏 ∘ 𝑀) ∈ (β„•0 ↑m 𝑇) ↔ (𝑏 ∘ 𝑀):π‘‡βŸΆβ„•0))
2014, 19mpbird 257 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑏 ∘ 𝑀) ∈ (β„•0 ↑m 𝑇))
21 simprl 770 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ π‘Ž = (𝑏 β†Ύ 𝑂))
22 resco 6247 . . . . . . 7 ((𝑏 ∘ 𝑀) β†Ύ 𝑂) = (𝑏 ∘ (𝑀 β†Ύ 𝑂))
23 simpll3 1215 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂))
2423coeq2d 5861 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑏 ∘ (𝑀 β†Ύ 𝑂)) = (𝑏 ∘ ( I β†Ύ 𝑂)))
25 coires1 6261 . . . . . . . 8 (𝑏 ∘ ( I β†Ύ 𝑂)) = (𝑏 β†Ύ 𝑂)
2624, 25eqtrdi 2789 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (𝑏 ∘ (𝑀 β†Ύ 𝑂)) = (𝑏 β†Ύ 𝑂))
2722, 26eqtrid 2785 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ ((𝑏 ∘ 𝑀) β†Ύ 𝑂) = (𝑏 β†Ύ 𝑂))
2821, 27eqtr4d 2776 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ π‘Ž = ((𝑏 ∘ 𝑀) β†Ύ 𝑂))
29 simpll1 1213 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑆 ∈ V)
30 oveq2 7414 . . . . . . . . . . 11 (π‘Ž = 𝑆 β†’ (β„•0 ↑m π‘Ž) = (β„•0 ↑m 𝑆))
31 oveq2 7414 . . . . . . . . . . 11 (π‘Ž = 𝑆 β†’ (β„€ ↑m π‘Ž) = (β„€ ↑m 𝑆))
3230, 31sseq12d 4015 . . . . . . . . . 10 (π‘Ž = 𝑆 β†’ ((β„•0 ↑m π‘Ž) βŠ† (β„€ ↑m π‘Ž) ↔ (β„•0 ↑m 𝑆) βŠ† (β„€ ↑m 𝑆)))
33 zex 12564 . . . . . . . . . . 11 β„€ ∈ V
34 nn0ssz 12578 . . . . . . . . . . 11 β„•0 βŠ† β„€
35 mapss 8880 . . . . . . . . . . 11 ((β„€ ∈ V ∧ β„•0 βŠ† β„€) β†’ (β„•0 ↑m π‘Ž) βŠ† (β„€ ↑m π‘Ž))
3633, 34, 35mp2an 691 . . . . . . . . . 10 (β„•0 ↑m π‘Ž) βŠ† (β„€ ↑m π‘Ž)
3732, 36vtoclg 3557 . . . . . . . . 9 (𝑆 ∈ V β†’ (β„•0 ↑m 𝑆) βŠ† (β„€ ↑m 𝑆))
3829, 37syl 17 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (β„•0 ↑m 𝑆) βŠ† (β„€ ↑m 𝑆))
39 simplr 768 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑏 ∈ (β„•0 ↑m 𝑆))
4038, 39sseldd 3983 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ 𝑏 ∈ (β„€ ↑m 𝑆))
41 coeq1 5856 . . . . . . . . 9 (𝑑 = 𝑏 β†’ (𝑑 ∘ 𝑀) = (𝑏 ∘ 𝑀))
4241fveq2d 6893 . . . . . . . 8 (𝑑 = 𝑏 β†’ (π‘ƒβ€˜(𝑑 ∘ 𝑀)) = (π‘ƒβ€˜(𝑏 ∘ 𝑀)))
43 eqid 2733 . . . . . . . 8 (𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀))) = (𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))
44 fvex 6902 . . . . . . . 8 (π‘ƒβ€˜(𝑏 ∘ 𝑀)) ∈ V
4542, 43, 44fvmpt 6996 . . . . . . 7 (𝑏 ∈ (β„€ ↑m 𝑆) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = (π‘ƒβ€˜(𝑏 ∘ 𝑀)))
4640, 45syl 17 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = (π‘ƒβ€˜(𝑏 ∘ 𝑀)))
47 simprr 772 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)
4846, 47eqtr3d 2775 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ (π‘ƒβ€˜(𝑏 ∘ 𝑀)) = 0)
49 reseq1 5974 . . . . . . . 8 (𝑐 = (𝑏 ∘ 𝑀) β†’ (𝑐 β†Ύ 𝑂) = ((𝑏 ∘ 𝑀) β†Ύ 𝑂))
5049eqeq2d 2744 . . . . . . 7 (𝑐 = (𝑏 ∘ 𝑀) β†’ (π‘Ž = (𝑐 β†Ύ 𝑂) ↔ π‘Ž = ((𝑏 ∘ 𝑀) β†Ύ 𝑂)))
51 fveqeq2 6898 . . . . . . 7 (𝑐 = (𝑏 ∘ 𝑀) β†’ ((π‘ƒβ€˜π‘) = 0 ↔ (π‘ƒβ€˜(𝑏 ∘ 𝑀)) = 0))
5250, 51anbi12d 632 . . . . . 6 (𝑐 = (𝑏 ∘ 𝑀) β†’ ((π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0) ↔ (π‘Ž = ((𝑏 ∘ 𝑀) β†Ύ 𝑂) ∧ (π‘ƒβ€˜(𝑏 ∘ 𝑀)) = 0)))
5352rspcev 3613 . . . . 5 (((𝑏 ∘ 𝑀) ∈ (β„•0 ↑m 𝑇) ∧ (π‘Ž = ((𝑏 ∘ 𝑀) β†Ύ 𝑂) ∧ (π‘ƒβ€˜(𝑏 ∘ 𝑀)) = 0)) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0))
5420, 28, 48, 53syl12anc 836 . . . 4 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑏 ∈ (β„•0 ↑m 𝑆)) ∧ (π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0)) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0))
5554rexlimdva2 3158 . . 3 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ (βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑇)(π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)))
56 simpr 486 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑐 ∈ (β„•0 ↑m 𝑇))
5716adantr 482 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑇 ∈ V)
58 elmapg 8830 . . . . . . . . . . . 12 ((β„•0 ∈ V ∧ 𝑇 ∈ V) β†’ (𝑐 ∈ (β„•0 ↑m 𝑇) ↔ 𝑐:π‘‡βŸΆβ„•0))
592, 57, 58sylancr 588 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑐 ∈ (β„•0 ↑m 𝑇) ↔ 𝑐:π‘‡βŸΆβ„•0))
6056, 59mpbid 231 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑐:π‘‡βŸΆβ„•0)
6160adantr 482 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ 𝑐:π‘‡βŸΆβ„•0)
629ad2antrr 725 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ 𝑀:𝑇–1-1→𝑆)
63 f1cnv 6855 . . . . . . . . . 10 (𝑀:𝑇–1-1→𝑆 β†’ ◑𝑀:ran 𝑀–1-1-onto→𝑇)
64 f1of 6831 . . . . . . . . . 10 (◑𝑀:ran 𝑀–1-1-onto→𝑇 β†’ ◑𝑀:ran π‘€βŸΆπ‘‡)
6562, 63, 643syl 18 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ◑𝑀:ran π‘€βŸΆπ‘‡)
66 fco 6739 . . . . . . . . 9 ((𝑐:π‘‡βŸΆβ„•0 ∧ ◑𝑀:ran π‘€βŸΆπ‘‡) β†’ (𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„•0)
6761, 65, 66syl2anc 585 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„•0)
68 c0ex 11205 . . . . . . . . . 10 0 ∈ V
6968fconst 6775 . . . . . . . . 9 ((𝑆 βˆ– ran 𝑀) Γ— {0}):(𝑆 βˆ– ran 𝑀)⟢{0}
7069a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑆 βˆ– ran 𝑀) Γ— {0}):(𝑆 βˆ– ran 𝑀)⟢{0})
71 disjdif 4471 . . . . . . . . 9 (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…
7271a1i 11 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…)
73 fun 6751 . . . . . . . 8 ((((𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„•0 ∧ ((𝑆 βˆ– ran 𝑀) Γ— {0}):(𝑆 βˆ– ran 𝑀)⟢{0}) ∧ (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„•0 βˆͺ {0}))
7467, 70, 72, 73syl21anc 837 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„•0 βˆͺ {0}))
75 frn 6722 . . . . . . . . . . 11 (𝑀:π‘‡βŸΆπ‘† β†’ ran 𝑀 βŠ† 𝑆)
769, 10, 753syl 18 . . . . . . . . . 10 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ ran 𝑀 βŠ† 𝑆)
7776ad2antrr 725 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ran 𝑀 βŠ† 𝑆)
78 undif 4481 . . . . . . . . 9 (ran 𝑀 βŠ† 𝑆 ↔ (ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀)) = 𝑆)
7977, 78sylib 217 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀)) = 𝑆)
80 0nn0 12484 . . . . . . . . . . 11 0 ∈ β„•0
81 snssi 4811 . . . . . . . . . . 11 (0 ∈ β„•0 β†’ {0} βŠ† β„•0)
8280, 81ax-mp 5 . . . . . . . . . 10 {0} βŠ† β„•0
83 ssequn2 4183 . . . . . . . . . 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 6710 . . . . . . 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 8830 . . . . . . . 8 ((β„•0 ∈ V ∧ 𝑆 ∈ V) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„•0))
892, 3, 88sylancr 588 . . . . . . 7 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„•0))
9089ad2antrr 725 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„•0))
9187, 90mpbird 257 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆))
92 simprl 770 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ π‘Ž = (𝑐 β†Ύ 𝑂))
93 resundir 5995 . . . . . . . . 9 (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂) = (((𝑐 ∘ ◑𝑀) β†Ύ 𝑂) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂))
94 resco 6247 . . . . . . . . . . 11 ((𝑐 ∘ ◑𝑀) β†Ύ 𝑂) = (𝑐 ∘ (◑𝑀 β†Ύ 𝑂))
95 simpl2 1193 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑀:𝑇–1-1→𝑆)
96 df-f1 6546 . . . . . . . . . . . . . . . . 17 (𝑀:𝑇–1-1→𝑆 ↔ (𝑀:π‘‡βŸΆπ‘† ∧ Fun ◑𝑀))
9796simprbi 498 . . . . . . . . . . . . . . . 16 (𝑀:𝑇–1-1→𝑆 β†’ Fun ◑𝑀)
98 funcnvres 6624 . . . . . . . . . . . . . . . 16 (Fun ◑𝑀 β†’ β—‘(𝑀 β†Ύ 𝑂) = (◑𝑀 β†Ύ (𝑀 β€œ 𝑂)))
9995, 97, 983syl 18 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ β—‘(𝑀 β†Ύ 𝑂) = (◑𝑀 β†Ύ (𝑀 β€œ 𝑂)))
100 simpl3 1194 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂))
101100cnveqd 5874 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ β—‘(𝑀 β†Ύ 𝑂) = β—‘( I β†Ύ 𝑂))
102 df-ima 5689 . . . . . . . . . . . . . . . . 17 (𝑀 β€œ 𝑂) = ran (𝑀 β†Ύ 𝑂)
103100rneqd 5936 . . . . . . . . . . . . . . . . . 18 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ ran (𝑀 β†Ύ 𝑂) = ran ( I β†Ύ 𝑂))
104 rnresi 6072 . . . . . . . . . . . . . . . . . 18 ran ( I β†Ύ 𝑂) = 𝑂
105103, 104eqtrdi 2789 . . . . . . . . . . . . . . . . 17 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ ran (𝑀 β†Ύ 𝑂) = 𝑂)
106102, 105eqtrid 2785 . . . . . . . . . . . . . . . 16 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑀 β€œ 𝑂) = 𝑂)
107106reseq2d 5980 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (◑𝑀 β†Ύ (𝑀 β€œ 𝑂)) = (◑𝑀 β†Ύ 𝑂))
10899, 101, 1073eqtr3d 2781 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ β—‘( I β†Ύ 𝑂) = (◑𝑀 β†Ύ 𝑂))
109 cnvresid 6625 . . . . . . . . . . . . . 14 β—‘( I β†Ύ 𝑂) = ( I β†Ύ 𝑂)
110108, 109eqtr3di 2788 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (◑𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂))
111110coeq2d 5861 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑐 ∘ (◑𝑀 β†Ύ 𝑂)) = (𝑐 ∘ ( I β†Ύ 𝑂)))
112 coires1 6261 . . . . . . . . . . . 12 (𝑐 ∘ ( I β†Ύ 𝑂)) = (𝑐 β†Ύ 𝑂)
113111, 112eqtrdi 2789 . . . . . . . . . . 11 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑐 ∘ (◑𝑀 β†Ύ 𝑂)) = (𝑐 β†Ύ 𝑂))
11494, 113eqtrid 2785 . . . . . . . . . 10 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ ((𝑐 ∘ ◑𝑀) β†Ύ 𝑂) = (𝑐 β†Ύ 𝑂))
115 dmres 6002 . . . . . . . . . . . 12 dom (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂) = (𝑂 ∩ dom ((𝑆 βˆ– ran 𝑀) Γ— {0}))
11668snnz 4780 . . . . . . . . . . . . . . 15 {0} β‰  βˆ…
117 dmxp 5927 . . . . . . . . . . . . . . 15 ({0} β‰  βˆ… β†’ dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) = (𝑆 βˆ– ran 𝑀))
118116, 117ax-mp 5 . . . . . . . . . . . . . 14 dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) = (𝑆 βˆ– ran 𝑀)
119118ineq2i 4209 . . . . . . . . . . . . 13 (𝑂 ∩ dom ((𝑆 βˆ– ran 𝑀) Γ— {0})) = (𝑂 ∩ (𝑆 βˆ– ran 𝑀))
120 inss1 4228 . . . . . . . . . . . . . . 15 (𝑂 ∩ 𝑆) βŠ† 𝑂
121103, 104eqtr2di 2790 . . . . . . . . . . . . . . . 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 4020 . . . . . . . . . . . . . . 15 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑂 βŠ† ran 𝑀)
126120, 125sstrid 3993 . . . . . . . . . . . . . 14 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑂 ∩ 𝑆) βŠ† ran 𝑀)
127 inssdif0 4369 . . . . . . . . . . . . . 14 ((𝑂 ∩ 𝑆) βŠ† ran 𝑀 ↔ (𝑂 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…)
128126, 127sylib 217 . . . . . . . . . . . . 13 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑂 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…)
129119, 128eqtrid 2785 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑂 ∩ dom ((𝑆 βˆ– ran 𝑀) Γ— {0})) = βˆ…)
130115, 129eqtrid 2785 . . . . . . . . . . 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 4164 . . . . . . . . 9 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (((𝑐 ∘ ◑𝑀) β†Ύ 𝑂) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) β†Ύ 𝑂)) = ((𝑐 β†Ύ 𝑂) βˆͺ βˆ…))
13693, 135eqtrid 2785 . . . . . . . 8 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂) = ((𝑐 β†Ύ 𝑂) βˆͺ βˆ…))
137 un0 4390 . . . . . . . 8 ((𝑐 β†Ύ 𝑂) βˆͺ βˆ…) = (𝑐 β†Ύ 𝑂)
138136, 137eqtr2di 2790 . . . . . . 7 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ (𝑐 β†Ύ 𝑂) = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂))
139138adantr 482 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 β†Ύ 𝑂) = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂))
14092, 139eqtrd 2773 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ π‘Ž = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂))
141 fss 6732 . . . . . . . . . . . . 13 ((𝑐:π‘‡βŸΆβ„•0 ∧ β„•0 βŠ† β„€) β†’ 𝑐:π‘‡βŸΆβ„€)
14260, 34, 141sylancl 587 . . . . . . . . . . . 12 (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) β†’ 𝑐:π‘‡βŸΆβ„€)
143142adantr 482 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ 𝑐:π‘‡βŸΆβ„€)
144 fco 6739 . . . . . . . . . . 11 ((𝑐:π‘‡βŸΆβ„€ ∧ ◑𝑀:ran π‘€βŸΆπ‘‡) β†’ (𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„€)
145143, 65, 144syl2anc 585 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„€)
146 fun 6751 . . . . . . . . . 10 ((((𝑐 ∘ ◑𝑀):ran π‘€βŸΆβ„€ ∧ ((𝑆 βˆ– ran 𝑀) Γ— {0}):(𝑆 βˆ– ran 𝑀)⟢{0}) ∧ (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀)) = βˆ…) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„€ βˆͺ {0}))
147145, 70, 72, 146syl21anc 837 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):(ran 𝑀 βˆͺ (𝑆 βˆ– ran 𝑀))⟢(β„€ βˆͺ {0}))
148 0z 12566 . . . . . . . . . . . . 13 0 ∈ β„€
149 snssi 4811 . . . . . . . . . . . . 13 (0 ∈ β„€ β†’ {0} βŠ† β„€)
150148, 149ax-mp 5 . . . . . . . . . . . 12 {0} βŠ† β„€
151 ssequn2 4183 . . . . . . . . . . . 12 ({0} βŠ† β„€ ↔ (β„€ βˆͺ {0}) = β„€)
152150, 151mpbi 229 . . . . . . . . . . 11 (β„€ βˆͺ {0}) = β„€
153152a1i 11 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (β„€ βˆͺ {0}) = β„€)
15479, 153feq23d 6710 . . . . . . . . 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 8830 . . . . . . . . . 10 ((β„€ ∈ V ∧ 𝑆 ∈ V) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„€))
15733, 3, 156sylancr 588 . . . . . . . . 9 ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„€))
158157ad2antrr 725 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆) ↔ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})):π‘†βŸΆβ„€))
159155, 158mpbird 257 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„€ ↑m 𝑆))
160 coeq1 5856 . . . . . . . . 9 (𝑑 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (𝑑 ∘ 𝑀) = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀))
161160fveq2d 6893 . . . . . . . 8 (𝑑 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (π‘ƒβ€˜(𝑑 ∘ 𝑀)) = (π‘ƒβ€˜(((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀)))
162 fvex 6902 . . . . . . . 8 (π‘ƒβ€˜(((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀)) ∈ V
163161, 43, 162fvmpt 6996 . . . . . . 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 6245 . . . . . . . 8 (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀) = (((𝑐 ∘ ◑𝑀) ∘ 𝑀) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀))
166 coass 6262 . . . . . . . . . . 11 ((𝑐 ∘ ◑𝑀) ∘ 𝑀) = (𝑐 ∘ (◑𝑀 ∘ 𝑀))
167 f1cocnv1 6861 . . . . . . . . . . . . 13 (𝑀:𝑇–1-1→𝑆 β†’ (◑𝑀 ∘ 𝑀) = ( I β†Ύ 𝑇))
168167coeq2d 5861 . . . . . . . . . . . 12 (𝑀:𝑇–1-1→𝑆 β†’ (𝑐 ∘ (◑𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I β†Ύ 𝑇)))
16962, 168syl 17 . . . . . . . . . . 11 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 ∘ (◑𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I β†Ύ 𝑇)))
170166, 169eqtrid 2785 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ◑𝑀) ∘ 𝑀) = (𝑐 ∘ ( I β†Ύ 𝑇)))
171118ineq1i 4208 . . . . . . . . . . . . 13 (dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) ∩ ran 𝑀) = ((𝑆 βˆ– ran 𝑀) ∩ ran 𝑀)
172 incom 4201 . . . . . . . . . . . . 13 ((𝑆 βˆ– ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 βˆ– ran 𝑀))
173171, 172, 713eqtri 2765 . . . . . . . . . . . 12 (dom ((𝑆 βˆ– ran 𝑀) Γ— {0}) ∩ ran 𝑀) = βˆ…
174 coeq0 6252 . . . . . . . . . . . 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 4164 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) ∘ 𝑀) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I β†Ύ 𝑇)) βˆͺ βˆ…))
178 un0 4390 . . . . . . . . . 10 ((𝑐 ∘ ( I β†Ύ 𝑇)) βˆͺ βˆ…) = (𝑐 ∘ ( I β†Ύ 𝑇))
179 fcoi1 6763 . . . . . . . . . . 11 (𝑐:π‘‡βŸΆβ„•0 β†’ (𝑐 ∘ ( I β†Ύ 𝑇)) = 𝑐)
18061, 179syl 17 . . . . . . . . . 10 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (𝑐 ∘ ( I β†Ύ 𝑇)) = 𝑐)
181178, 180eqtrid 2785 . . . . . . . . 9 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑐 ∘ ( I β†Ύ 𝑇)) βˆͺ βˆ…) = 𝑐)
182177, 181eqtrd 2773 . . . . . . . 8 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) ∘ 𝑀) βˆͺ (((𝑆 βˆ– ran 𝑀) Γ— {0}) ∘ 𝑀)) = 𝑐)
183165, 182eqtrid 2785 . . . . . . 7 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀) = 𝑐)
184183fveq2d 6893 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (π‘ƒβ€˜(((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∘ 𝑀)) = (π‘ƒβ€˜π‘))
185 simprr 772 . . . . . 6 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ (π‘ƒβ€˜π‘) = 0)
186164, 184, 1853eqtrd 2777 . . . . 5 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = 0)
187 reseq1 5974 . . . . . . . 8 (𝑏 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (𝑏 β†Ύ 𝑂) = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂))
188187eqeq2d 2744 . . . . . . 7 (𝑏 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (π‘Ž = (𝑏 β†Ύ 𝑂) ↔ π‘Ž = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂)))
189 fveqeq2 6898 . . . . . . 7 (𝑏 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ (((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0 ↔ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = 0))
190188, 189anbi12d 632 . . . . . 6 (𝑏 = ((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†’ ((π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0) ↔ (π‘Ž = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = 0)))
191190rspcev 3613 . . . . 5 ((((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) ∈ (β„•0 ↑m 𝑆) ∧ (π‘Ž = (((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0})) β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜((𝑐 ∘ ◑𝑀) βˆͺ ((𝑆 βˆ– ran 𝑀) Γ— {0}))) = 0)) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0))
19291, 140, 186, 191syl12anc 836 . . . 4 ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 β†Ύ 𝑂) = ( I β†Ύ 𝑂)) ∧ 𝑐 ∈ (β„•0 ↑m 𝑇)) ∧ (π‘Ž = (𝑐 β†Ύ 𝑂) ∧ (π‘ƒβ€˜π‘) = 0)) β†’ βˆƒπ‘ ∈ (β„•0 ↑m 𝑆)(π‘Ž = (𝑏 β†Ύ 𝑂) ∧ ((𝑑 ∈ (β„€ ↑m 𝑆) ↦ (π‘ƒβ€˜(𝑑 ∘ 𝑀)))β€˜π‘) = 0))
193192rexlimdva2 3158 . . 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 2802 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 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆƒwrex 3071  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628   ↦ cmpt 5231   I cid 5573   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   ∘ ccom 5680  Rel wrel 5681  Fun wfun 6535  βŸΆwf 6537  β€“1-1β†’wf1 6538  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541  (class class class)co 7406   ↑m cmap 8817  0cc0 11107  β„•0cn0 12469  β„€cz 12555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-i2m1 11175  ax-1ne0 11176  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-map 8819  df-neg 11444  df-nn 12210  df-n0 12470  df-z 12556
This theorem is referenced by:  eldioph2  41486  eldioph2b  41487
  Copyright terms: Public domain W3C validator