Metamath Proof Explorer

Theorem diophrw

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)

Ref Expression
Assertion diophrw ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) } = { 𝑎 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) } )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) → 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) )
2 nn0ex ⊢ ℕ0 ∈ V
3 simp1 ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → 𝑆 ∈ V )
4 3 adantr ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) → 𝑆 ∈ V )
5 elmapg ⊢ ( ( ℕ0 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ↔ 𝑏 : 𝑆 ⟶ ℕ0 ) )
6 2 4 5 sylancr ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) → ( 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ↔ 𝑏 : 𝑆 ⟶ ℕ0 ) )
7 1 6 mpbid ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) → 𝑏 : 𝑆 ⟶ ℕ0 )
8 7 adantr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → 𝑏 : 𝑆 ⟶ ℕ0 )
9 simp2 ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → 𝑀 : 𝑇 –1-1→ 𝑆 )
10 f1f ⊢ ( 𝑀 : 𝑇 –1-1→ 𝑆 → 𝑀 : 𝑇 ⟶ 𝑆 )
11 9 10 syl ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → 𝑀 : 𝑇 ⟶ 𝑆 )
12 11 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → 𝑀 : 𝑇 ⟶ 𝑆 )
13 fco ⊢ ( ( 𝑏 : 𝑆 ⟶ ℕ0 ∧ 𝑀 : 𝑇 ⟶ 𝑆 ) → ( 𝑏 ∘ 𝑀 ) : 𝑇 ⟶ ℕ0 )
14 8 12 13 syl2anc ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( 𝑏 ∘ 𝑀 ) : 𝑇 ⟶ ℕ0 )
15 f1dmex ⊢ ( ( 𝑀 : 𝑇 –1-1→ 𝑆 ∧ 𝑆 ∈ V ) → 𝑇 ∈ V )
16 9 3 15 syl2anc ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → 𝑇 ∈ V )
17 16 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → 𝑇 ∈ V )
18 elmapg ⊢ ( ( ℕ0 ∈ V ∧ 𝑇 ∈ V ) → ( ( 𝑏 ∘ 𝑀 ) ∈ ( ℕ0 ↑m 𝑇 ) ↔ ( 𝑏 ∘ 𝑀 ) : 𝑇 ⟶ ℕ0 ) )
19 2 17 18 sylancr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( ( 𝑏 ∘ 𝑀 ) ∈ ( ℕ0 ↑m 𝑇 ) ↔ ( 𝑏 ∘ 𝑀 ) : 𝑇 ⟶ ℕ0 ) )
20 14 19 mpbird ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( 𝑏 ∘ 𝑀 ) ∈ ( ℕ0 ↑m 𝑇 ) )
21 simprl ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → 𝑎 = ( 𝑏 ↾ 𝑂 ) )
22 resco ⊢ ( ( 𝑏 ∘ 𝑀 ) ↾ 𝑂 ) = ( 𝑏 ∘ ( 𝑀 ↾ 𝑂 ) )
23 simpll3 ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) )
24 23 coeq2d ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( 𝑏 ∘ ( 𝑀 ↾ 𝑂 ) ) = ( 𝑏 ∘ ( I ↾ 𝑂 ) ) )
25 coires1 ⊢ ( 𝑏 ∘ ( I ↾ 𝑂 ) ) = ( 𝑏 ↾ 𝑂 )
26 24 25 eqtrdi ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( 𝑏 ∘ ( 𝑀 ↾ 𝑂 ) ) = ( 𝑏 ↾ 𝑂 ) )
27 22 26 eqtrid ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( ( 𝑏 ∘ 𝑀 ) ↾ 𝑂 ) = ( 𝑏 ↾ 𝑂 ) )
28 21 27 eqtr4d ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → 𝑎 = ( ( 𝑏 ∘ 𝑀 ) ↾ 𝑂 ) )
29 simpll1 ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → 𝑆 ∈ V )
30 oveq2 ⊢ ( 𝑎 = 𝑆 → ( ℕ0 ↑m 𝑎 ) = ( ℕ0 ↑m 𝑆 ) )
31 oveq2 ⊢ ( 𝑎 = 𝑆 → ( ℤ ↑m 𝑎 ) = ( ℤ ↑m 𝑆 ) )
32 30 31 sseq12d ⊢ ( 𝑎 = 𝑆 → ( ( ℕ0 ↑m 𝑎 ) ⊆ ( ℤ ↑m 𝑎 ) ↔ ( ℕ0 ↑m 𝑆 ) ⊆ ( ℤ ↑m 𝑆 ) ) )
33 zex ⊢ ℤ ∈ V
34 nn0ssz ⊢ ℕ0 ⊆ ℤ
35 mapss ⊢ ( ( ℤ ∈ V ∧ ℕ0 ⊆ ℤ ) → ( ℕ0 ↑m 𝑎 ) ⊆ ( ℤ ↑m 𝑎 ) )
36 33 34 35 mp2an ⊢ ( ℕ0 ↑m 𝑎 ) ⊆ ( ℤ ↑m 𝑎 )
37 32 36 vtoclg ⊢ ( 𝑆 ∈ V → ( ℕ0 ↑m 𝑆 ) ⊆ ( ℤ ↑m 𝑆 ) )
38 29 37 syl ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( ℕ0 ↑m 𝑆 ) ⊆ ( ℤ ↑m 𝑆 ) )
39 simplr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) )
40 38 39 sseldd ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → 𝑏 ∈ ( ℤ ↑m 𝑆 ) )
41 coeq1 ⊢ ( 𝑑 = 𝑏 → ( 𝑑 ∘ 𝑀 ) = ( 𝑏 ∘ 𝑀 ) )
42 41 fveq2d ⊢ ( 𝑑 = 𝑏 → ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) = ( 𝑃 ‘ ( 𝑏 ∘ 𝑀 ) ) )
43 eqid ⊢ ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) = ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) )
44 fvex ⊢ ( 𝑃 ‘ ( 𝑏 ∘ 𝑀 ) ) ∈ V
45 42 43 44 fvmpt ⊢ ( 𝑏 ∈ ( ℤ ↑m 𝑆 ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = ( 𝑃 ‘ ( 𝑏 ∘ 𝑀 ) ) )
46 40 45 syl ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = ( 𝑃 ‘ ( 𝑏 ∘ 𝑀 ) ) )
47 simprr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 )
48 46 47 eqtr3d ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ( 𝑃 ‘ ( 𝑏 ∘ 𝑀 ) ) = 0 )
49 reseq1 ⊢ ( 𝑐 = ( 𝑏 ∘ 𝑀 ) → ( 𝑐 ↾ 𝑂 ) = ( ( 𝑏 ∘ 𝑀 ) ↾ 𝑂 ) )
50 49 eqeq2d ⊢ ( 𝑐 = ( 𝑏 ∘ 𝑀 ) → ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ↔ 𝑎 = ( ( 𝑏 ∘ 𝑀 ) ↾ 𝑂 ) ) )
51 fveqeq2 ⊢ ( 𝑐 = ( 𝑏 ∘ 𝑀 ) → ( ( 𝑃 ‘ 𝑐 ) = 0 ↔ ( 𝑃 ‘ ( 𝑏 ∘ 𝑀 ) ) = 0 ) )
52 50 51 anbi12d ⊢ ( 𝑐 = ( 𝑏 ∘ 𝑀 ) → ( ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ↔ ( 𝑎 = ( ( 𝑏 ∘ 𝑀 ) ↾ 𝑂 ) ∧ ( 𝑃 ‘ ( 𝑏 ∘ 𝑀 ) ) = 0 ) ) )
53 52 rspcev ⊢ ( ( ( 𝑏 ∘ 𝑀 ) ∈ ( ℕ0 ↑m 𝑇 ) ∧ ( 𝑎 = ( ( 𝑏 ∘ 𝑀 ) ↾ 𝑂 ) ∧ ( 𝑃 ‘ ( 𝑏 ∘ 𝑀 ) ) = 0 ) ) → ∃ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) )
54 20 28 48 53 syl12anc ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ) ∧ ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) → ∃ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) )
55 54 rexlimdva2 ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) → ∃ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) )
56 simpr ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) )
57 16 adantr ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → 𝑇 ∈ V )
58 elmapg ⊢ ( ( ℕ0 ∈ V ∧ 𝑇 ∈ V ) → ( 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ↔ 𝑐 : 𝑇 ⟶ ℕ0 ) )
59 2 57 58 sylancr ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ↔ 𝑐 : 𝑇 ⟶ ℕ0 ) )
60 56 59 mpbid ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → 𝑐 : 𝑇 ⟶ ℕ0 )
61 60 adantr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → 𝑐 : 𝑇 ⟶ ℕ0 )
62 9 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → 𝑀 : 𝑇 –1-1→ 𝑆 )
63 f1cnv ⊢ ( 𝑀 : 𝑇 –1-1→ 𝑆 → ◡ 𝑀 : ran 𝑀 –1-1-onto→ 𝑇 )
64 f1of ⊢ ( ◡ 𝑀 : ran 𝑀 –1-1-onto→ 𝑇 → ◡ 𝑀 : ran 𝑀 ⟶ 𝑇 )
65 62 63 64 3syl ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ◡ 𝑀 : ran 𝑀 ⟶ 𝑇 )
66 fco ⊢ ( ( 𝑐 : 𝑇 ⟶ ℕ0 ∧ ◡ 𝑀 : ran 𝑀 ⟶ 𝑇 ) → ( 𝑐 ∘ ◡ 𝑀 ) : ran 𝑀 ⟶ ℕ0 )
67 61 65 66 syl2anc ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( 𝑐 ∘ ◡ 𝑀 ) : ran 𝑀 ⟶ ℕ0 )
68 c0ex ⊢ 0 ∈ V
69 68 fconst ⊢ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) : ( 𝑆 ∖ ran 𝑀 ) ⟶ { 0 }
70 69 a1i ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) : ( 𝑆 ∖ ran 𝑀 ) ⟶ { 0 } )
71 disjdif ⊢ ( ran 𝑀 ∩ ( 𝑆 ∖ ran 𝑀 ) ) = ∅
72 71 a1i ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ran 𝑀 ∩ ( 𝑆 ∖ ran 𝑀 ) ) = ∅ )
73 fun ⊢ ( ( ( ( 𝑐 ∘ ◡ 𝑀 ) : ran 𝑀 ⟶ ℕ0 ∧ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) : ( 𝑆 ∖ ran 𝑀 ) ⟶ { 0 } ) ∧ ( ran 𝑀 ∩ ( 𝑆 ∖ ran 𝑀 ) ) = ∅ ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : ( ran 𝑀 ∪ ( 𝑆 ∖ ran 𝑀 ) ) ⟶ ( ℕ0 ∪ { 0 } ) )
74 67 70 72 73 syl21anc ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : ( ran 𝑀 ∪ ( 𝑆 ∖ ran 𝑀 ) ) ⟶ ( ℕ0 ∪ { 0 } ) )
75 frn ⊢ ( 𝑀 : 𝑇 ⟶ 𝑆 → ran 𝑀 ⊆ 𝑆 )
76 9 10 75 3syl ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → ran 𝑀 ⊆ 𝑆 )
77 76 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ran 𝑀 ⊆ 𝑆 )
78 undif ⊢ ( ran 𝑀 ⊆ 𝑆 ↔ ( ran 𝑀 ∪ ( 𝑆 ∖ ran 𝑀 ) ) = 𝑆 )
79 77 78 sylib ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ran 𝑀 ∪ ( 𝑆 ∖ ran 𝑀 ) ) = 𝑆 )
80 0nn0 ⊢ 0 ∈ ℕ0
81 snssi ⊢ ( 0 ∈ ℕ0 → { 0 } ⊆ ℕ0 )
82 80 81 ax-mp ⊢ { 0 } ⊆ ℕ0
83 ssequn2 ⊢ ( { 0 } ⊆ ℕ0 ↔ ( ℕ0 ∪ { 0 } ) = ℕ0 )
84 82 83 mpbi ⊢ ( ℕ0 ∪ { 0 } ) = ℕ0
85 84 a1i ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ℕ0 ∪ { 0 } ) = ℕ0 )
86 79 85 feq23d ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : ( ran 𝑀 ∪ ( 𝑆 ∖ ran 𝑀 ) ) ⟶ ( ℕ0 ∪ { 0 } ) ↔ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℕ0 ) )
87 74 86 mpbid ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℕ0 )
88 elmapg ⊢ ( ( ℕ0 ∈ V ∧ 𝑆 ∈ V ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℕ0 ↑m 𝑆 ) ↔ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℕ0 ) )
89 2 3 88 sylancr ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℕ0 ↑m 𝑆 ) ↔ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℕ0 ) )
90 89 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℕ0 ↑m 𝑆 ) ↔ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℕ0 ) )
91 87 90 mpbird ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℕ0 ↑m 𝑆 ) )
92 simprl ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → 𝑎 = ( 𝑐 ↾ 𝑂 ) )
93 resundir ⊢ ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ↾ 𝑂 ) ∪ ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) )
94 resco ⊢ ( ( 𝑐 ∘ ◡ 𝑀 ) ↾ 𝑂 ) = ( 𝑐 ∘ ( ◡ 𝑀 ↾ 𝑂 ) )
95 simpl2 ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → 𝑀 : 𝑇 –1-1→ 𝑆 )
96 df-f1 ⊢ ( 𝑀 : 𝑇 –1-1→ 𝑆 ↔ ( 𝑀 : 𝑇 ⟶ 𝑆 ∧ Fun ◡ 𝑀 ) )
97 96 simprbi ⊢ ( 𝑀 : 𝑇 –1-1→ 𝑆 → Fun ◡ 𝑀 )
98 funcnvres ⊢ ( Fun ◡ 𝑀 → ◡ ( 𝑀 ↾ 𝑂 ) = ( ◡ 𝑀 ↾ ( 𝑀 “ 𝑂 ) ) )
99 95 97 98 3syl ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ◡ ( 𝑀 ↾ 𝑂 ) = ( ◡ 𝑀 ↾ ( 𝑀 “ 𝑂 ) ) )
100 simpl3 ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) )
101 100 cnveqd ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ◡ ( 𝑀 ↾ 𝑂 ) = ◡ ( I ↾ 𝑂 ) )
102 df-ima ⊢ ( 𝑀 “ 𝑂 ) = ran ( 𝑀 ↾ 𝑂 )
103 100 rneqd ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ran ( 𝑀 ↾ 𝑂 ) = ran ( I ↾ 𝑂 ) )
104 rnresi ⊢ ran ( I ↾ 𝑂 ) = 𝑂
105 103 104 eqtrdi ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ran ( 𝑀 ↾ 𝑂 ) = 𝑂 )
106 102 105 eqtrid ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑀 “ 𝑂 ) = 𝑂 )
107 106 reseq2d ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( ◡ 𝑀 ↾ ( 𝑀 “ 𝑂 ) ) = ( ◡ 𝑀 ↾ 𝑂 ) )
108 99 101 107 3eqtr3d ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ◡ ( I ↾ 𝑂 ) = ( ◡ 𝑀 ↾ 𝑂 ) )
109 cnvresid ⊢ ◡ ( I ↾ 𝑂 ) = ( I ↾ 𝑂 )
110 108 109 eqtr3di ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( ◡ 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) )
111 110 coeq2d ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑐 ∘ ( ◡ 𝑀 ↾ 𝑂 ) ) = ( 𝑐 ∘ ( I ↾ 𝑂 ) ) )
112 coires1 ⊢ ( 𝑐 ∘ ( I ↾ 𝑂 ) ) = ( 𝑐 ↾ 𝑂 )
113 111 112 eqtrdi ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑐 ∘ ( ◡ 𝑀 ↾ 𝑂 ) ) = ( 𝑐 ↾ 𝑂 ) )
114 94 113 eqtrid ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ↾ 𝑂 ) = ( 𝑐 ↾ 𝑂 ) )
115 dmres ⊢ dom ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) = ( 𝑂 ∩ dom ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) )
116 68 snnz ⊢ { 0 } ≠ ∅
117 dmxp ⊢ ( { 0 } ≠ ∅ → dom ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) = ( 𝑆 ∖ ran 𝑀 ) )
118 116 117 ax-mp ⊢ dom ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) = ( 𝑆 ∖ ran 𝑀 )
119 118 ineq2i ⊢ ( 𝑂 ∩ dom ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) = ( 𝑂 ∩ ( 𝑆 ∖ ran 𝑀 ) )
120 inss1 ⊢ ( 𝑂 ∩ 𝑆 ) ⊆ 𝑂
121 103 104 eqtr2di ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → 𝑂 = ran ( 𝑀 ↾ 𝑂 ) )
122 resss ⊢ ( 𝑀 ↾ 𝑂 ) ⊆ 𝑀
123 rnss ⊢ ( ( 𝑀 ↾ 𝑂 ) ⊆ 𝑀 → ran ( 𝑀 ↾ 𝑂 ) ⊆ ran 𝑀 )
124 122 123 mp1i ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ran ( 𝑀 ↾ 𝑂 ) ⊆ ran 𝑀 )
125 121 124 eqsstrd ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → 𝑂 ⊆ ran 𝑀 )
126 120 125 sstrid ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑂 ∩ 𝑆 ) ⊆ ran 𝑀 )
127 inssdif0 ⊢ ( ( 𝑂 ∩ 𝑆 ) ⊆ ran 𝑀 ↔ ( 𝑂 ∩ ( 𝑆 ∖ ran 𝑀 ) ) = ∅ )
128 126 127 sylib ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑂 ∩ ( 𝑆 ∖ ran 𝑀 ) ) = ∅ )
129 119 128 eqtrid ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑂 ∩ dom ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) = ∅ )
130 115 129 eqtrid ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → dom ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) = ∅ )
131 relres ⊢ Rel ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 )
132 reldm0 ⊢ ( Rel ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) → ( ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) = ∅ ↔ dom ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) = ∅ ) )
133 131 132 ax-mp ⊢ ( ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) = ∅ ↔ dom ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) = ∅ )
134 130 133 sylibr ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) = ∅ )
135 114 134 uneq12d ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ↾ 𝑂 ) ∪ ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ↾ 𝑂 ) ) = ( ( 𝑐 ↾ 𝑂 ) ∪ ∅ ) )
136 93 135 eqtrid ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) = ( ( 𝑐 ↾ 𝑂 ) ∪ ∅ ) )
137 un0 ⊢ ( ( 𝑐 ↾ 𝑂 ) ∪ ∅ ) = ( 𝑐 ↾ 𝑂 )
138 136 137 eqtr2di ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → ( 𝑐 ↾ 𝑂 ) = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) )
139 138 adantr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( 𝑐 ↾ 𝑂 ) = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) )
140 92 139 eqtrd ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → 𝑎 = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) )
141 fss ⊢ ( ( 𝑐 : 𝑇 ⟶ ℕ0 ∧ ℕ0 ⊆ ℤ ) → 𝑐 : 𝑇 ⟶ ℤ )
142 60 34 141 sylancl ⊢ ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) → 𝑐 : 𝑇 ⟶ ℤ )
143 142 adantr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → 𝑐 : 𝑇 ⟶ ℤ )
144 fco ⊢ ( ( 𝑐 : 𝑇 ⟶ ℤ ∧ ◡ 𝑀 : ran 𝑀 ⟶ 𝑇 ) → ( 𝑐 ∘ ◡ 𝑀 ) : ran 𝑀 ⟶ ℤ )
145 143 65 144 syl2anc ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( 𝑐 ∘ ◡ 𝑀 ) : ran 𝑀 ⟶ ℤ )
146 fun ⊢ ( ( ( ( 𝑐 ∘ ◡ 𝑀 ) : ran 𝑀 ⟶ ℤ ∧ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) : ( 𝑆 ∖ ran 𝑀 ) ⟶ { 0 } ) ∧ ( ran 𝑀 ∩ ( 𝑆 ∖ ran 𝑀 ) ) = ∅ ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : ( ran 𝑀 ∪ ( 𝑆 ∖ ran 𝑀 ) ) ⟶ ( ℤ ∪ { 0 } ) )
147 145 70 72 146 syl21anc ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : ( ran 𝑀 ∪ ( 𝑆 ∖ ran 𝑀 ) ) ⟶ ( ℤ ∪ { 0 } ) )
148 0z ⊢ 0 ∈ ℤ
149 snssi ⊢ ( 0 ∈ ℤ → { 0 } ⊆ ℤ )
150 148 149 ax-mp ⊢ { 0 } ⊆ ℤ
151 ssequn2 ⊢ ( { 0 } ⊆ ℤ ↔ ( ℤ ∪ { 0 } ) = ℤ )
152 150 151 mpbi ⊢ ( ℤ ∪ { 0 } ) = ℤ
153 152 a1i ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ℤ ∪ { 0 } ) = ℤ )
154 79 153 feq23d ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : ( ran 𝑀 ∪ ( 𝑆 ∖ ran 𝑀 ) ) ⟶ ( ℤ ∪ { 0 } ) ↔ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℤ ) )
155 147 154 mpbid ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℤ )
156 elmapg ⊢ ( ( ℤ ∈ V ∧ 𝑆 ∈ V ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℤ ↑m 𝑆 ) ↔ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℤ ) )
157 33 3 156 sylancr ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℤ ↑m 𝑆 ) ↔ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℤ ) )
158 157 ad2antrr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℤ ↑m 𝑆 ) ↔ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) : 𝑆 ⟶ ℤ ) )
159 155 158 mpbird ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℤ ↑m 𝑆 ) )
160 coeq1 ⊢ ( 𝑑 = ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) → ( 𝑑 ∘ 𝑀 ) = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∘ 𝑀 ) )
161 160 fveq2d ⊢ ( 𝑑 = ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) → ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) = ( 𝑃 ‘ ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∘ 𝑀 ) ) )
162 fvex ⊢ ( 𝑃 ‘ ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∘ 𝑀 ) ) ∈ V
163 161 43 162 fvmpt ⊢ ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℤ ↑m 𝑆 ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ) = ( 𝑃 ‘ ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∘ 𝑀 ) ) )
164 159 163 syl ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ) = ( 𝑃 ‘ ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∘ 𝑀 ) ) )
165 coundir ⊢ ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∘ 𝑀 ) = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∘ 𝑀 ) ∪ ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∘ 𝑀 ) )
166 coass ⊢ ( ( 𝑐 ∘ ◡ 𝑀 ) ∘ 𝑀 ) = ( 𝑐 ∘ ( ◡ 𝑀 ∘ 𝑀 ) )
167 f1cocnv1 ⊢ ( 𝑀 : 𝑇 –1-1→ 𝑆 → ( ◡ 𝑀 ∘ 𝑀 ) = ( I ↾ 𝑇 ) )
168 167 coeq2d ⊢ ( 𝑀 : 𝑇 –1-1→ 𝑆 → ( 𝑐 ∘ ( ◡ 𝑀 ∘ 𝑀 ) ) = ( 𝑐 ∘ ( I ↾ 𝑇 ) ) )
169 62 168 syl ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( 𝑐 ∘ ( ◡ 𝑀 ∘ 𝑀 ) ) = ( 𝑐 ∘ ( I ↾ 𝑇 ) ) )
170 166 169 eqtrid ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑐 ∘ ◡ 𝑀 ) ∘ 𝑀 ) = ( 𝑐 ∘ ( I ↾ 𝑇 ) ) )
171 118 ineq1i ⊢ ( dom ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∩ ran 𝑀 ) = ( ( 𝑆 ∖ ran 𝑀 ) ∩ ran 𝑀 )
172 incom ⊢ ( ( 𝑆 ∖ ran 𝑀 ) ∩ ran 𝑀 ) = ( ran 𝑀 ∩ ( 𝑆 ∖ ran 𝑀 ) )
173 171 172 71 3eqtri ⊢ ( dom ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∩ ran 𝑀 ) = ∅
174 coeq0 ⊢ ( ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∘ 𝑀 ) = ∅ ↔ ( dom ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∩ ran 𝑀 ) = ∅ )
175 173 174 mpbir ⊢ ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∘ 𝑀 ) = ∅
176 175 a1i ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∘ 𝑀 ) = ∅ )
177 170 176 uneq12d ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∘ 𝑀 ) ∪ ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∘ 𝑀 ) ) = ( ( 𝑐 ∘ ( I ↾ 𝑇 ) ) ∪ ∅ ) )
178 un0 ⊢ ( ( 𝑐 ∘ ( I ↾ 𝑇 ) ) ∪ ∅ ) = ( 𝑐 ∘ ( I ↾ 𝑇 ) )
179 fcoi1 ⊢ ( 𝑐 : 𝑇 ⟶ ℕ0 → ( 𝑐 ∘ ( I ↾ 𝑇 ) ) = 𝑐 )
180 61 179 syl ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( 𝑐 ∘ ( I ↾ 𝑇 ) ) = 𝑐 )
181 178 180 eqtrid ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑐 ∘ ( I ↾ 𝑇 ) ) ∪ ∅ ) = 𝑐 )
182 177 181 eqtrd ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∘ 𝑀 ) ∪ ( ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ∘ 𝑀 ) ) = 𝑐 )
183 165 182 eqtrid ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∘ 𝑀 ) = 𝑐 )
184 183 fveq2d ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( 𝑃 ‘ ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∘ 𝑀 ) ) = ( 𝑃 ‘ 𝑐 ) )
185 simprr ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( 𝑃 ‘ 𝑐 ) = 0 )
186 164 184 185 3eqtrd ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ) = 0 )
187 reseq1 ⊢ ( 𝑏 = ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) → ( 𝑏 ↾ 𝑂 ) = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) )
188 187 eqeq2d ⊢ ( 𝑏 = ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) → ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ↔ 𝑎 = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) ) )
189 fveqeq2 ⊢ ( 𝑏 = ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) → ( ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ↔ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ) = 0 ) )
190 188 189 anbi12d ⊢ ( 𝑏 = ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) → ( ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ↔ ( 𝑎 = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ) = 0 ) ) )
191 190 rspcev ⊢ ( ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ∈ ( ℕ0 ↑m 𝑆 ) ∧ ( 𝑎 = ( ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ ( ( 𝑐 ∘ ◡ 𝑀 ) ∪ ( ( 𝑆 ∖ ran 𝑀 ) × { 0 } ) ) ) = 0 ) ) → ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) )
192 91 140 186 191 syl12anc ⊢ ( ( ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) ∧ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ) ∧ ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) → ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) )
193 192 rexlimdva2 ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → ( ∃ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) → ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ) )
194 55 193 impbid ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) ↔ ∃ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) ) )
195 194 abbidv ⊢ ( ( 𝑆 ∈ V ∧ 𝑀 : 𝑇 –1-1→ 𝑆 ∧ ( 𝑀 ↾ 𝑂 ) = ( I ↾ 𝑂 ) ) → { 𝑎 ∣ ∃ 𝑏 ∈ ( ℕ0 ↑m 𝑆 ) ( 𝑎 = ( 𝑏 ↾ 𝑂 ) ∧ ( ( 𝑑 ∈ ( ℤ ↑m 𝑆 ) ↦ ( 𝑃 ‘ ( 𝑑 ∘ 𝑀 ) ) ) ‘ 𝑏 ) = 0 ) } = { 𝑎 ∣ ∃ 𝑐 ∈ ( ℕ0 ↑m 𝑇 ) ( 𝑎 = ( 𝑐 ↾ 𝑂 ) ∧ ( 𝑃 ‘ 𝑐 ) = 0 ) } )