Theorem diophrw 38282

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 479	. . . . . . . . 9 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → 𝑏 ∈ (ℕ0 ↑𝑚 𝑆))
2		nn0ex 11649	. . . . . . . . . 10 ⊢ ℕ0 ∈ V
3		simp1 1127	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V)
4	3	adantr 474	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → 𝑆 ∈ V)
5		elmapg 8153	. . . . . . . . . 10 ⊢ ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0 ↑𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
6	2, 4, 5	sylancr 581	. . . . . . . . 9 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → (𝑏 ∈ (ℕ0 ↑𝑚 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
7	1, 6	mpbid 224	. . . . . . . 8 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) → 𝑏:𝑆⟶ℕ0)
8	7	adantr 474	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0)
9		simp2 1128	. . . . . . . . 9 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇–1-1→𝑆)
10		f1f 6351	. . . . . . . . 9 ⊢ (𝑀:𝑇–1-1→𝑆 → 𝑀:𝑇⟶𝑆)
11	9, 10	syl 17	. . . . . . . 8 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇⟶𝑆)
12	11	ad2antrr 716	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑀:𝑇⟶𝑆)
13		fco 6308	. . . . . . 7 ⊢ ((𝑏:𝑆⟶ℕ0 ∧ 𝑀:𝑇⟶𝑆) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0)
14	8, 12, 13	syl2anc 579	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0)
15		f1dmex 7415	. . . . . . . . 9 ⊢ ((𝑀:𝑇–1-1→𝑆 ∧ 𝑆 ∈ V) → 𝑇 ∈ V)
16	9, 3, 15	syl2anc 579	. . . . . . . 8 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V)
17	16	ad2antrr 716	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V)
18		elmapg 8153	. . . . . . 7 ⊢ ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑𝑚 𝑇) ↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0))
19	2, 17, 18	sylancr 581	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑𝑚 𝑇) ↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0))
20	14, 19	mpbird 249	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀) ∈ (ℕ0 ↑𝑚 𝑇))
21		simprl 761	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏 ↾ 𝑂))
22		resco 5893	. . . . . . 7 ⊢ ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀 ↾ 𝑂))
23		simpll3 1230	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
24	23	coeq2d 5530	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ∘ ( I ↾ 𝑂)))
25		coires1 5907	. . . . . . . 8 ⊢ (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏 ↾ 𝑂)
26	24, 25	syl6eq 2830	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ↾ 𝑂))
27	22, 26	syl5eq 2826	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ↾ 𝑂))
28	21, 27	eqtr4d 2817	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂))
29		simpll1 1226	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V)
30		oveq2 6930	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑆 → (ℕ0 ↑𝑚 𝑎) = (ℕ0 ↑𝑚 𝑆))
31		oveq2 6930	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑆 → (ℤ ↑𝑚 𝑎) = (ℤ ↑𝑚 𝑆))
32	30, 31	sseq12d 3853	. . . . . . . . . 10 ⊢ (𝑎 = 𝑆 → ((ℕ0 ↑𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎) ↔ (ℕ0 ↑𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆)))
33		zex 11737	. . . . . . . . . . 11 ⊢ ℤ ∈ V
34		nn0ssz 11750	. . . . . . . . . . 11 ⊢ ℕ0 ⊆ ℤ
35		mapss 8186	. . . . . . . . . . 11 ⊢ ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0 ↑𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎))
36	33, 34, 35	mp2an 682	. . . . . . . . . 10 ⊢ (ℕ0 ↑𝑚 𝑎) ⊆ (ℤ ↑𝑚 𝑎)
37	32, 36	vtoclg 3467	. . . . . . . . 9 ⊢ (𝑆 ∈ V → (ℕ0 ↑𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
38	29, 37	syl 17	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (ℕ0 ↑𝑚 𝑆) ⊆ (ℤ ↑𝑚 𝑆))
39		simplr 759	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0 ↑𝑚 𝑆))
40	38, 39	sseldd 3822	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑𝑚 𝑆))
41		coeq1 5525	. . . . . . . . 9 ⊢ (𝑑 = 𝑏 → (𝑑 ∘ 𝑀) = (𝑏 ∘ 𝑀))
42	41	fveq2d 6450	. . . . . . . 8 ⊢ (𝑑 = 𝑏 → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(𝑏 ∘ 𝑀)))
43		eqid 2778	. . . . . . . 8 ⊢ (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀))) = (𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))
44		fvex 6459	. . . . . . . 8 ⊢ (𝑃‘(𝑏 ∘ 𝑀)) ∈ V
45	42, 43, 44	fvmpt 6542	. . . . . . 7 ⊢ (𝑏 ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀)))
46	40, 45	syl 17	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀)))
47		simprr 763	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)
48	46, 47	eqtr3d 2816	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏 ∘ 𝑀)) = 0)
49		reseq1 5636	. . . . . . . 8 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑐 ↾ 𝑂) = ((𝑏 ∘ 𝑀) ↾ 𝑂))
50	49	eqeq2d 2788	. . . . . . 7 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑎 = (𝑐 ↾ 𝑂) ↔ 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂)))
51		fveqeq2 6455	. . . . . . 7 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑃‘𝑐) = 0 ↔ (𝑃‘(𝑏 ∘ 𝑀)) = 0))
52	50, 51	anbi12d 624	. . . . . 6 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) ↔ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0)))
53	52	rspcev 3511	. . . . 5 ⊢ (((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑𝑚 𝑇) ∧ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))
54	20, 28, 48, 53	syl12anc 827	. . . 4 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑𝑚 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))
55	54	rexlimdva2 3216	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)))
56		simpr 479	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑐 ∈ (ℕ0 ↑𝑚 𝑇))
57	16	adantr 474	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑇 ∈ V)
58		elmapg 8153	. . . . . . . . . . . 12 ⊢ ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0 ↑𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
59	2, 57, 58	sylancr 581	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑐 ∈ (ℕ0 ↑𝑚 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
60	56, 59	mpbid 224	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑐:𝑇⟶ℕ0)
61	60	adantr 474	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℕ0)
62	9	ad2antrr 716	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑀:𝑇–1-1→𝑆)
63		f1cnv 6414	. . . . . . . . . 10 ⊢ (𝑀:𝑇–1-1→𝑆 → ◡𝑀:ran 𝑀–1-1-onto→𝑇)
64		f1of 6391	. . . . . . . . . 10 ⊢ (◡𝑀:ran 𝑀–1-1-onto→𝑇 → ◡𝑀:ran 𝑀⟶𝑇)
65	62, 63, 64	3syl 18	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ◡𝑀:ran 𝑀⟶𝑇)
66		fco 6308	. . . . . . . . 9 ⊢ ((𝑐:𝑇⟶ℕ0 ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0)
67	61, 65, 66	syl2anc 579	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0)
68		c0ex 10370	. . . . . . . . . 10 ⊢ 0 ∈ V
69	68	fconst 6341	. . . . . . . . 9 ⊢ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}
70	69	a1i 11	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0})
71		disjdif 4264	. . . . . . . . 9 ⊢ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅
72	71	a1i 11	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
73		fun 6316	. . . . . . . 8 ⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
74	67, 70, 72, 73	syl21anc 828	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
75		frn 6297	. . . . . . . . . . 11 ⊢ (𝑀:𝑇⟶𝑆 → ran 𝑀 ⊆ 𝑆)
76	9, 10, 75	3syl 18	. . . . . . . . . 10 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → ran 𝑀 ⊆ 𝑆)
77	76	ad2antrr 716	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ran 𝑀 ⊆ 𝑆)
78		undif 4273	. . . . . . . . 9 ⊢ (ran 𝑀 ⊆ 𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
79	77, 78	sylib 210	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
80		0nn0 11659	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
81		snssi 4570	. . . . . . . . . . 11 ⊢ (0 ∈ ℕ0 → {0} ⊆ ℕ0)
82	80, 81	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ ℕ0
83		ssequn2 4009	. . . . . . . . . 10 ⊢ ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
84	82, 83	mpbi 222	. . . . . . . . 9 ⊢ (ℕ0 ∪ {0}) = ℕ0
85	84	a1i 11	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℕ0 ∪ {0}) = ℕ0)
86	79, 85	feq23d 6286	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
87	74, 86	mpbid 224	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)
88		elmapg 8153	. . . . . . . 8 ⊢ ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
89	2, 3, 88	sylancr 581	. . . . . . 7 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
90	89	ad2antrr 716	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
91	87, 90	mpbird 249	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆))
92		simprl 761	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (𝑐 ↾ 𝑂))
93		resundir 5661	. . . . . . . . 9 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂))
94		resco 5893	. . . . . . . . . . 11 ⊢ ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ∘ (◡𝑀 ↾ 𝑂))
95		cnvresid 6213	. . . . . . . . . . . . . 14 ⊢ ◡( I ↾ 𝑂) = ( I ↾ 𝑂)
96		simpl2 1201	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑀:𝑇–1-1→𝑆)
97		df-f1 6140	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀:𝑇–1-1→𝑆 ↔ (𝑀:𝑇⟶𝑆 ∧ Fun ◡𝑀))
98	97	simprbi 492	. . . . . . . . . . . . . . . 16 ⊢ (𝑀:𝑇–1-1→𝑆 → Fun ◡𝑀)
99		funcnvres 6212	. . . . . . . . . . . . . . . 16 ⊢ (Fun ◡𝑀 → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂)))
100	96, 98, 99	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂)))
101		simpl3 1203	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
102	101	cnveqd 5543	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ◡(𝑀 ↾ 𝑂) = ◡( I ↾ 𝑂))
103		df-ima 5368	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 “ 𝑂) = ran (𝑀 ↾ 𝑂)
104	101	rneqd 5598	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) = ran ( I ↾ 𝑂))
105		rnresi 5733	. . . . . . . . . . . . . . . . . 18 ⊢ ran ( I ↾ 𝑂) = 𝑂
106	104, 105	syl6eq 2830	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) = 𝑂)
107	103, 106	syl5eq 2826	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑀 “ 𝑂) = 𝑂)
108	107	reseq2d 5642	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (◡𝑀 ↾ (𝑀 “ 𝑂)) = (◡𝑀 ↾ 𝑂))
109	100, 102, 108	3eqtr3d 2822	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ◡( I ↾ 𝑂) = (◡𝑀 ↾ 𝑂))
110	95, 109	syl5reqr 2829	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (◡𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
111	110	coeq2d 5530	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ∘ ( I ↾ 𝑂)))
112		coires1 5907	. . . . . . . . . . . 12 ⊢ (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐 ↾ 𝑂)
113	111, 112	syl6eq 2830	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ↾ 𝑂))
114	94, 113	syl5eq 2826	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ↾ 𝑂))
115		dmres 5668	. . . . . . . . . . . 12 ⊢ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0}))
116	68	snnz 4542	. . . . . . . . . . . . . . 15 ⊢ {0} ≠ ∅
117		dmxp 5589	. . . . . . . . . . . . . . 15 ⊢ ({0} ≠ ∅ → dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀))
118	116, 117	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀)
119	118	ineq2i 4034	. . . . . . . . . . . . 13 ⊢ (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀))
120		inss1 4053	. . . . . . . . . . . . . . 15 ⊢ (𝑂 ∩ 𝑆) ⊆ 𝑂
121	104, 105	syl6req 2831	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑂 = ran (𝑀 ↾ 𝑂))
122		resss 5671	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ↾ 𝑂) ⊆ 𝑀
123		rnss 5599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ↾ 𝑂) ⊆ 𝑀 → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀)
124	122, 123	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀)
125	121, 124	eqsstrd 3858	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑂 ⊆ ran 𝑀)
126	120, 125	syl5ss 3832	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑂 ∩ 𝑆) ⊆ ran 𝑀)
127		inssdif0 4178	. . . . . . . . . . . . . 14 ⊢ ((𝑂 ∩ 𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
128	126, 127	sylib 210	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
129	119, 128	syl5eq 2826	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅)
130	115, 129	syl5eq 2826	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
131		relres 5675	. . . . . . . . . . . 12 ⊢ Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)
132		reldm0 5588	. . . . . . . . . . . 12 ⊢ (Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) → ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅))
133	131, 132	ax-mp 5	. . . . . . . . . . 11 ⊢ ((((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅ ↔ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
134	130, 133	sylibr 226	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
135	114, 134	uneq12d 3991	. . . . . . . . 9 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐 ↾ 𝑂) ∪ ∅))
136	93, 135	syl5eq 2826	. . . . . . . 8 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐 ↾ 𝑂) ∪ ∅))
137		un0 4193	. . . . . . . 8 ⊢ ((𝑐 ↾ 𝑂) ∪ ∅) = (𝑐 ↾ 𝑂)
138	136, 137	syl6req 2831	. . . . . . 7 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
139	138	adantr 474	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
140	92, 139	eqtrd 2814	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
141		fss 6304	. . . . . . . . . . . . 13 ⊢ ((𝑐:𝑇⟶ℕ0 ∧ ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ)
142	60, 34, 141	sylancl 580	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) → 𝑐:𝑇⟶ℤ)
143	142	adantr 474	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℤ)
144		fco 6308	. . . . . . . . . . 11 ⊢ ((𝑐:𝑇⟶ℤ ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ)
145	143, 65, 144	syl2anc 579	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ)
146		fun 6316	. . . . . . . . . 10 ⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
147	145, 70, 72, 146	syl21anc 828	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
148		0z 11739	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
149		snssi 4570	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℤ → {0} ⊆ ℤ)
150	148, 149	ax-mp 5	. . . . . . . . . . . 12 ⊢ {0} ⊆ ℤ
151		ssequn2 4009	. . . . . . . . . . . 12 ⊢ ({0} ⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ)
152	150, 151	mpbi 222	. . . . . . . . . . 11 ⊢ (ℤ ∪ {0}) = ℤ
153	152	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℤ ∪ {0}) = ℤ)
154	79, 153	feq23d 6286	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
155	147, 154	mpbid 224	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)
156		elmapg 8153	. . . . . . . . . 10 ⊢ ((ℤ ∈ V ∧ 𝑆 ∈ V) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
157	33, 3, 156	sylancr 581	. . . . . . . . 9 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
158	157	ad2antrr 716	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
159	155, 158	mpbird 249	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆))
160		coeq1 5525	. . . . . . . . 9 ⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑 ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))
161	160	fveq2d 6450	. . . . . . . 8 ⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
162		fvex 6459	. . . . . . . 8 ⊢ (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V
163	161, 43, 162	fvmpt 6542	. . . . . . 7 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑𝑚 𝑆) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
164	159, 163	syl 17	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
165		coundir 5891	. . . . . . . 8 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀))
166		coass 5908	. . . . . . . . . . 11 ⊢ ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ (◡𝑀 ∘ 𝑀))
167		f1cocnv1 6420	. . . . . . . . . . . . 13 ⊢ (𝑀:𝑇–1-1→𝑆 → (◡𝑀 ∘ 𝑀) = ( I ↾ 𝑇))
168	167	coeq2d 5530	. . . . . . . . . . . 12 ⊢ (𝑀:𝑇–1-1→𝑆 → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
169	62, 168	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
170	166, 169	syl5eq 2826	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇)))
171	118	ineq1i 4033	. . . . . . . . . . . . 13 ⊢ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀)
172		incom 4028	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀))
173	171, 172, 71	3eqtri 2806	. . . . . . . . . . . 12 ⊢ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅
174		coeq0 5898	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ ↔ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅)
175	173, 174	mpbir 223	. . . . . . . . . . 11 ⊢ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅
176	175	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅)
177	170, 176	uneq12d 3991	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅))
178		un0 4193	. . . . . . . . . 10 ⊢ ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇))
179		fcoi1 6328	. . . . . . . . . . 11 ⊢ (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
180	61, 179	syl 17	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
181	178, 180	syl5eq 2826	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐)
182	177, 181	eqtrd 2814	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐)
183	165, 182	syl5eq 2826	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐)
184	183	fveq2d 6450	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃‘𝑐))
185		simprr 763	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘𝑐) = 0)
186	164, 184, 185	3eqtrd 2818	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)
187		reseq1 5636	. . . . . . . 8 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
188	187	eqeq2d 2788	. . . . . . 7 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏 ↾ 𝑂) ↔ 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)))
189		fveqeq2 6455	. . . . . . 7 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))
190	188, 189	anbi12d 624	. . . . . 6 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)))
191	190	rspcev 3511	. . . . 5 ⊢ ((((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑𝑚 𝑆) ∧ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0))
192	91, 140, 186, 191	syl12anc 827	. . . 4 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑𝑚 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0))
193	192	rexlimdva2 3216	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) → ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)))
194	55, 193	impbid 204	. 2 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)))
195	194	abbidv 2906	1 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ↑𝑚 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑𝑚 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0 ↑𝑚 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)})

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107  {cab 2763   ≠ wne 2969  ∃wrex 3091  Vcvv 3398   ∖ cdif 3789   ∪ cun 3790   ∩ cin 3791   ⊆ wss 3792  ∅c0 4141  {csn 4398   ↦ cmpt 4965   I cid 5260   × cxp 5353  ^◡ccnv 5354  dom cdm 5355  ran crn 5356   ↾ cres 5357   “ cima 5358   ∘ ccom 5359  Rel wrel 5360  Fun wfun 6129  ⟶wf 6131  –1-1→wf1 6132  –1-1-onto→wf1o 6134  ‘cfv 6135  (class class class)co 6922   ↑_𝑚 cmap 8140  0cc0 10272  ℕ₀cn0 11642  ℤcz 11728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-i2m1 10340  ax-1ne0 10341  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-map 8142  df-neg 10609  df-nn 11375  df-n0 11643  df-z 11729

This theorem is referenced by:  eldioph2  38285  eldioph2b  38286