Theorem diophrw 37322

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 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)})

Distinct variable groups:   𝑆,𝑎,𝑏,𝑐,𝑑   𝑇,𝑎,𝑏,𝑐,𝑑   𝑀,𝑎,𝑏,𝑐,𝑑   𝑂,𝑎,𝑏,𝑐,𝑑   𝑃,𝑏,𝑐,𝑑

Allowed substitution hint:   𝑃(𝑎)

Proof of Theorem diophrw

Step	Hyp	Ref	Expression
1		simpr 477	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → 𝑏 ∈ (ℕ0 ↑𝑚 𝑆))
2		nn0ex 11298	. . . . . . . . . . 11 ⊢ ℕ0 ∈ V
3		simp1 1061	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V)
4	3	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → 𝑆 ∈ V)
5		elmapg 7870	. . . . . . . . . . 11 ⊢ ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0 ↑𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
6	2, 4, 5	sylancr 695	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → (𝑏 ∈ (ℕ0 ↑𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
7	1, 6	mpbid 222	. . . . . . . . 9 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → 𝑏:𝑆⟶ℕ0)
8	7	adantr 481	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0)
9		simp2 1062	. . . . . . . . . 10 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇–1-1→𝑆)
10		f1f 6101	. . . . . . . . . 10 ⊢ (𝑀:𝑇–1-1→𝑆 → 𝑀:𝑇⟶𝑆)
11	9, 10	syl 17	. . . . . . . . 9 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇⟶𝑆)
12	11	ad2antrr 762	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑀:𝑇⟶𝑆)
13		fco 6058	. . . . . . . 8 ⊢ ((𝑏:𝑆⟶ℕ0 ∧ 𝑀:𝑇⟶𝑆) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0)
14	8, 12, 13	syl2anc 693	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0)
15		f1dmex 7136	. . . . . . . . . 10 ⊢ ((𝑀:𝑇–1-1→𝑆 ∧ 𝑆 ∈ V) → 𝑇 ∈ V)
16	9, 3, 15	syl2anc 693	. . . . . . . . 9 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V)
17	16	ad2antrr 762	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V)
18		elmapg 7870	. . . . . . . 8 ⊢ ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑𝑚 𝑇) ↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0))
19	2, 17, 18	sylancr 695	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑𝑚 𝑇) ↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0))
20	14, 19	mpbird 247	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀) ∈ (ℕ0 ↑𝑚 𝑇))
21		simprl 794	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏 ↾ 𝑂))
22		resco 5639	. . . . . . . 8 ⊢ ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀 ↾ 𝑂))
23		simpll3 1102	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
24	23	coeq2d 5284	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ∘ ( I ↾ 𝑂)))
25		coires1 5653	. . . . . . . . 9 ⊢ (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏 ↾ 𝑂)
26	24, 25	syl6eq 2672	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ↾ 𝑂))
27	22, 26	syl5eq 2668	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ↾ 𝑂))
28	21, 27	eqtr4d 2659	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂))
29		simpll1 1100	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V)
30		oveq2 6658	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑆 → (ℕ0 ↑𝑚 𝑎) = (ℕ0 ↑𝑚 𝑆))
31		oveq2 6658	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝑆 → (ℤ ↑𝑚 𝑎) = (ℤ ↑𝑚 𝑆))
32	30, 31	sseq12d 3634	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑆 → ((ℕ0 ↑𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎) ↔ (ℕ0 ↑𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆)))
33		zex 11386	. . . . . . . . . . . 12 ⊢ ℤ ∈ V
34		nn0ssz 11398	. . . . . . . . . . . 12 ⊢ ℕ0 ⊆ ℤ
35		mapss 7900	. . . . . . . . . . . 12 ⊢ ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0 ↑𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎))
36	33, 34, 35	mp2an 708	. . . . . . . . . . 11 ⊢ (ℕ0 ↑𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎)
37	32, 36	vtoclg 3266	. . . . . . . . . 10 ⊢ (𝑆 ∈ V → (ℕ0 ↑𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
38	29, 37	syl 17	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (ℕ0 ↑𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
39		simplr 792	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0 ↑𝑚 𝑆))
40	38, 39	sseldd 3604	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑𝑚 𝑆))
41		coeq1 5279	. . . . . . . . . 10 ⊢ (𝑑 = 𝑏 → (𝑑 ∘ 𝑀) = (𝑏 ∘ 𝑀))
42	41	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑑 = 𝑏 → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(𝑏 ∘ 𝑀)))
43		eqid 2622	. . . . . . . . 9 ⊢ (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀))) = (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))
44		fvex 6201	. . . . . . . . 9 ⊢ (𝑃‘(𝑏 ∘ 𝑀)) ∈ V
45	42, 43, 44	fvmpt 6282	. . . . . . . 8 ⊢ (𝑏 ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀)))
46	40, 45	syl 17	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀)))
47		simprr 796	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)
48	46, 47	eqtr3d 2658	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏 ∘ 𝑀)) = 0)
49		reseq1 5390	. . . . . . . . 9 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑐 ↾ 𝑂) = ((𝑏 ∘ 𝑀) ↾ 𝑂))
50	49	eqeq2d 2632	. . . . . . . 8 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑎 = (𝑐 ↾ 𝑂) ↔ 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂)))
51		fveq2 6191	. . . . . . . . 9 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑃‘𝑐) = (𝑃‘(𝑏 ∘ 𝑀)))
52	51	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑃‘𝑐) = 0 ↔ (𝑃‘(𝑏 ∘ 𝑀)) = 0))
53	50, 52	anbi12d 747	. . . . . . 7 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) ↔ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0)))
54	53	rspcev 3309	. . . . . 6 ⊢ (((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑𝑚 𝑇) ∧ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))
55	20, 28, 48, 54	syl12anc 1324	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))
56	55	ex 450	. . . 4 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → ((𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)))
57	56	rexlimdva 3031	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)))
58		simpr 477	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑐 ∈ (ℕ0 ↑𝑚 𝑇))
59	16	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑇 ∈ V)
60		elmapg 7870	. . . . . . . . . . . . 13 ⊢ ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0 ↑𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
61	2, 59, 60	sylancr 695	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑐 ∈ (ℕ0 ↑𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
62	58, 61	mpbid 222	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑐:𝑇⟶ℕ0)
63	62	adantr 481	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℕ0)
64	9	ad2antrr 762	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑀:𝑇–1-1→𝑆)
65		f1cnv 6160	. . . . . . . . . . 11 ⊢ (𝑀:𝑇–1-1→𝑆 → ◡𝑀:ran 𝑀–1-1-onto→𝑇)
66		f1of 6137	. . . . . . . . . . 11 ⊢ (◡𝑀:ran 𝑀–1-1-onto→𝑇 → ◡𝑀:ran 𝑀⟶𝑇)
67	64, 65, 66	3syl 18	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ◡𝑀:ran 𝑀⟶𝑇)
68		fco 6058	. . . . . . . . . 10 ⊢ ((𝑐:𝑇⟶ℕ0 ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0)
69	63, 67, 68	syl2anc 693	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0)
70		c0ex 10034	. . . . . . . . . . 11 ⊢ 0 ∈ V
71	70	fconst 6091	. . . . . . . . . 10 ⊢ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}
72	71	a1i 11	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0})
73		disjdif 4040	. . . . . . . . . 10 ⊢ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅
74	73	a1i 11	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
75		fun 6066	. . . . . . . . 9 ⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
76	69, 72, 74, 75	syl21anc 1325	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
77		frn 6053	. . . . . . . . . . . 12 ⊢ (𝑀:𝑇⟶𝑆 → ran 𝑀 ⊆ 𝑆)
78	9, 10, 77	3syl 18	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → ran 𝑀 ⊆ 𝑆)
79	78	ad2antrr 762	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ran 𝑀 ⊆ 𝑆)
80		undif 4049	. . . . . . . . . 10 ⊢ (ran 𝑀 ⊆ 𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
81	79, 80	sylib 208	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
82		0nn0 11307	. . . . . . . . . . . 12 ⊢ 0 ∈ ℕ0
83		snssi 4339	. . . . . . . . . . . 12 ⊢ (0 ∈ ℕ0 → {0} ⊆ ℕ0)
84	82, 83	ax-mp 5	. . . . . . . . . . 11 ⊢ {0} ⊆ ℕ0
85		ssequn2 3786	. . . . . . . . . . 11 ⊢ ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
86	84, 85	mpbi 220	. . . . . . . . . 10 ⊢ (ℕ0 ∪ {0}) = ℕ0
87	86	a1i 11	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℕ0 ∪ {0}) = ℕ0)
88	81, 87	feq23d 6040	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
89	76, 88	mpbid 222	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)
90		elmapg 7870	. . . . . . . . 9 ⊢ ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
91	2, 3, 90	sylancr 695	. . . . . . . 8 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
92	91	ad2antrr 762	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
93	89, 92	mpbird 247	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆))
94		simprl 794	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (𝑐 ↾ 𝑂))
95		resundir 5411	. . . . . . . . . 10 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂))
96		resco 5639	. . . . . . . . . . . 12 ⊢ ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ∘ (◡𝑀 ↾ 𝑂))
97		cnvresid 5968	. . . . . . . . . . . . . . 15 ⊢ ◡( I ↾ 𝑂) = ( I ↾ 𝑂)
98		simpl2 1065	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑀:𝑇–1-1→𝑆)
99		df-f1 5893	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀:𝑇–1-1→𝑆 ↔ (𝑀:𝑇⟶𝑆 ∧ Fun ◡𝑀))
100	99	simprbi 480	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀:𝑇–1-1→𝑆 → Fun ◡𝑀)
101		funcnvres 5967	. . . . . . . . . . . . . . . . 17 ⊢ (Fun ◡𝑀 → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂)))
102	98, 100, 101	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂)))
103		simpl3 1066	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
104	103	cnveqd 5298	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ◡(𝑀 ↾ 𝑂) = ◡( I ↾ 𝑂))
105		df-ima 5127	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 “ 𝑂) = ran (𝑀 ↾ 𝑂)
106	103	rneqd 5353	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) = ran ( I ↾ 𝑂))
107		rnresi 5479	. . . . . . . . . . . . . . . . . . 19 ⊢ ran ( I ↾ 𝑂) = 𝑂
108	106, 107	syl6eq 2672	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) = 𝑂)
109	105, 108	syl5eq 2668	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑀 “ 𝑂) = 𝑂)
110	109	reseq2d 5396	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (◡𝑀 ↾ (𝑀 “ 𝑂)) = (◡𝑀 ↾ 𝑂))
111	102, 104, 110	3eqtr3d 2664	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ◡( I ↾ 𝑂) = (◡𝑀 ↾ 𝑂))
112	97, 111	syl5reqr 2671	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (◡𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
113	112	coeq2d 5284	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ∘ ( I ↾ 𝑂)))
114		coires1 5653	. . . . . . . . . . . . 13 ⊢ (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐 ↾ 𝑂)
115	113, 114	syl6eq 2672	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ↾ 𝑂))
116	96, 115	syl5eq 2668	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ↾ 𝑂))
117		dmres 5419	. . . . . . . . . . . . 13 ⊢ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0}))
118	70	snnz 4309	. . . . . . . . . . . . . . . 16 ⊢ {0} ≠ ∅
119		dmxp 5344	. . . . . . . . . . . . . . . 16 ⊢ ({0} ≠ ∅ → dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀))
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀)
121	120	ineq2i 3811	. . . . . . . . . . . . . 14 ⊢ (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀))
122		inss1 3833	. . . . . . . . . . . . . . . 16 ⊢ (𝑂 ∩ 𝑆) ⊆ 𝑂
123	106, 107	syl6req 2673	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑂 = ran (𝑀 ↾ 𝑂))
124		resss 5422	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ↾ 𝑂) ⊆ 𝑀
125		rnss 5354	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ↾ 𝑂) ⊆ 𝑀 → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀)
126	124, 125	mp1i 13	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀)
127	123, 126	eqsstrd 3639	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑂 ⊆ ran 𝑀)
128	122, 127	syl5ss 3614	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑂 ∩ 𝑆) ⊆ ran 𝑀)
129		inssdif0 3947	. . . . . . . . . . . . . . 15 ⊢ ((𝑂 ∩ 𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
130	128, 129	sylib 208	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
131	121, 130	syl5eq 2668	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅)
132	117, 131	syl5eq 2668	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
133		relres 5426	. . . . . . . . . . . . 13 ⊢ Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)
134		reldm0 5343	. . . . . . . . . . . . 13 ⊢ (Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) → ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅))
135	133, 134	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
136	132, 135	sylibr 224	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
137	116, 136	uneq12d 3768	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐 ↾ 𝑂) ∪ ∅))
138	95, 137	syl5eq 2668	. . . . . . . . 9 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐 ↾ 𝑂) ∪ ∅))
139		un0 3967	. . . . . . . . 9 ⊢ ((𝑐 ↾ 𝑂) ∪ ∅) = (𝑐 ↾ 𝑂)
140	138, 139	syl6req 2673	. . . . . . . 8 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
141	140	adantr 481	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
142	94, 141	eqtrd 2656	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
143		fss 6056	. . . . . . . . . . . . . 14 ⊢ ((𝑐:𝑇⟶ℕ0 ∧ ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ)
144	62, 34, 143	sylancl 694	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑐:𝑇⟶ℤ)
145	144	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℤ)
146		fco 6058	. . . . . . . . . . . 12 ⊢ ((𝑐:𝑇⟶ℤ ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ)
147	145, 67, 146	syl2anc 693	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ)
148		fun 6066	. . . . . . . . . . 11 ⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
149	147, 72, 74, 148	syl21anc 1325	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
150		0z 11388	. . . . . . . . . . . . . 14 ⊢ 0 ∈ ℤ
151		snssi 4339	. . . . . . . . . . . . . 14 ⊢ (0 ∈ ℤ → {0} ⊆ ℤ)
152	150, 151	ax-mp 5	. . . . . . . . . . . . 13 ⊢ {0} ⊆ ℤ
153		ssequn2 3786	. . . . . . . . . . . . 13 ⊢ ({0} ⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ)
154	152, 153	mpbi 220	. . . . . . . . . . . 12 ⊢ (ℤ ∪ {0}) = ℤ
155	154	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℤ ∪ {0}) = ℤ)
156	81, 155	feq23d 6040	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
157	149, 156	mpbid 222	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)
158		elmapg 7870	. . . . . . . . . . 11 ⊢ ((ℤ ∈ V ∧ 𝑆 ∈ V) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
159	33, 3, 158	sylancr 695	. . . . . . . . . 10 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
160	159	ad2antrr 762	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
161	157, 160	mpbird 247	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆))
162		coeq1 5279	. . . . . . . . . 10 ⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑 ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))
163	162	fveq2d 6195	. . . . . . . . 9 ⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
164		fvex 6201	. . . . . . . . 9 ⊢ (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V
165	163, 43, 164	fvmpt 6282	. . . . . . . 8 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
166	161, 165	syl 17	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
167		coundir 5637	. . . . . . . . 9 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀))
168		coass 5654	. . . . . . . . . . . 12 ⊢ ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ (◡𝑀 ∘ 𝑀))
169		f1cocnv1 6166	. . . . . . . . . . . . . 14 ⊢ (𝑀:𝑇–1-1→𝑆 → (◡𝑀 ∘ 𝑀) = ( I ↾ 𝑇))
170	169	coeq2d 5284	. . . . . . . . . . . . 13 ⊢ (𝑀:𝑇–1-1→𝑆 → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
171	64, 170	syl 17	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
172	168, 171	syl5eq 2668	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇)))
173	120	ineq1i 3810	. . . . . . . . . . . . . 14 ⊢ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀)
174		incom 3805	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀))
175	173, 174, 73	3eqtri 2648	. . . . . . . . . . . . 13 ⊢ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅
176		coeq0 5644	. . . . . . . . . . . . 13 ⊢ ((((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ ↔ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅)
177	175, 176	mpbir 221	. . . . . . . . . . . 12 ⊢ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅
178	177	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅)
179	172, 178	uneq12d 3768	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅))
180		un0 3967	. . . . . . . . . . 11 ⊢ ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇))
181		fcoi1 6078	. . . . . . . . . . . 12 ⊢ (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
182	63, 181	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
183	180, 182	syl5eq 2668	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐)
184	179, 183	eqtrd 2656	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐)
185	167, 184	syl5eq 2668	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐)
186	185	fveq2d 6195	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃‘𝑐))
187		simprr 796	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘𝑐) = 0)
188	166, 186, 187	3eqtrd 2660	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)
189		reseq1 5390	. . . . . . . . 9 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
190	189	eqeq2d 2632	. . . . . . . 8 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏 ↾ 𝑂) ↔ 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)))
191		fveq2 6191	. . . . . . . . 9 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))))
192	191	eqeq1d 2624	. . . . . . . 8 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))
193	190, 192	anbi12d 747	. . . . . . 7 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)))
194	193	rspcev 3309	. . . . . 6 ⊢ ((((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆) ∧ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0))
195	93, 142, 188, 194	syl12anc 1324	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0))
196	195	ex 450	. . . 4 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ((𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) → ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)))
197	196	rexlimdva 3031	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) → ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)))
198	57, 197	impbid 202	. 2 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)))
199	198	abbidv 2741	1 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)})

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  {cab 2608   ≠ wne 2794  ∃wrex 2913  Vcvv 3200   ∖ cdif 3571   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915  {csn 4177   ↦ cmpt 4729   I cid 5023   × cxp 5112  ^◡ccnv 5113  dom cdm 5114  ran crn 5115   ↾ cres 5116   “ cima 5117   ∘ ccom 5118  Rel wrel 5119  Fun wfun 5882  ⟶wf 5884  –1-1→wf1 5885  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ↑_𝑚 cmap 7857  0cc0 9936  ℕ₀cn0 11292  ℤcz 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378

This theorem is referenced by:  eldioph2  37325  eldioph2b  37326