Theorem diophrw 40497

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

Step	Hyp	Ref	Expression
1		simpr 484	. . . . . . . . 9 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) → 𝑏 ∈ (ℕ0 ↑m 𝑆))
2		nn0ex 12169	. . . . . . . . . 10 ⊢ ℕ0 ∈ V
3		simp1 1134	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑆 ∈ V)
4	3	adantr 480	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) → 𝑆 ∈ V)
5		elmapg 8586	. . . . . . . . . 10 ⊢ ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (𝑏 ∈ (ℕ0 ↑m 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
6	2, 4, 5	sylancr 586	. . . . . . . . 9 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) → (𝑏 ∈ (ℕ0 ↑m 𝑆) ↔ 𝑏:𝑆⟶ℕ0))
7	1, 6	mpbid 231	. . . . . . . 8 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) → 𝑏:𝑆⟶ℕ0)
8	7	adantr 480	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏:𝑆⟶ℕ0)
9		simp2 1135	. . . . . . . . 9 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇–1-1→𝑆)
10		f1f 6654	. . . . . . . . 9 ⊢ (𝑀:𝑇–1-1→𝑆 → 𝑀:𝑇⟶𝑆)
11	9, 10	syl 17	. . . . . . . 8 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑀:𝑇⟶𝑆)
12	11	ad2antrr 722	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑀:𝑇⟶𝑆)
13		fco 6608	. . . . . . 7 ⊢ ((𝑏:𝑆⟶ℕ0 ∧ 𝑀:𝑇⟶𝑆) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0)
14	8, 12, 13	syl2anc 583	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀):𝑇⟶ℕ0)
15		f1dmex 7773	. . . . . . . . 9 ⊢ ((𝑀:𝑇–1-1→𝑆 ∧ 𝑆 ∈ V) → 𝑇 ∈ V)
16	9, 3, 15	syl2anc 583	. . . . . . . 8 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → 𝑇 ∈ V)
17	16	ad2antrr 722	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑇 ∈ V)
18		elmapg 8586	. . . . . . 7 ⊢ ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → ((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑m 𝑇) ↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0))
19	2, 17, 18	sylancr 586	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑m 𝑇) ↔ (𝑏 ∘ 𝑀):𝑇⟶ℕ0))
20	14, 19	mpbird 256	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ 𝑀) ∈ (ℕ0 ↑m 𝑇))
21		simprl 767	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = (𝑏 ↾ 𝑂))
22		resco 6143	. . . . . . 7 ⊢ ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ∘ (𝑀 ↾ 𝑂))
23		simpll3 1212	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
24	23	coeq2d 5760	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ∘ ( I ↾ 𝑂)))
25		coires1 6157	. . . . . . . 8 ⊢ (𝑏 ∘ ( I ↾ 𝑂)) = (𝑏 ↾ 𝑂)
26	24, 25	eqtrdi 2795	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑏 ∘ (𝑀 ↾ 𝑂)) = (𝑏 ↾ 𝑂))
27	22, 26	syl5eq 2791	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑏 ∘ 𝑀) ↾ 𝑂) = (𝑏 ↾ 𝑂))
28	21, 27	eqtr4d 2781	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂))
29		simpll1 1210	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑆 ∈ V)
30		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑆 → (ℕ0 ↑m 𝑎) = (ℕ0 ↑m 𝑆))
31		oveq2 7263	. . . . . . . . . . 11 ⊢ (𝑎 = 𝑆 → (ℤ ↑m 𝑎) = (ℤ ↑m 𝑆))
32	30, 31	sseq12d 3950	. . . . . . . . . 10 ⊢ (𝑎 = 𝑆 → ((ℕ0 ↑m 𝑎) ⊆ (ℤ ↑m 𝑎) ↔ (ℕ0 ↑m 𝑆) ⊆ (ℤ ↑m 𝑆)))
33		zex 12258	. . . . . . . . . . 11 ⊢ ℤ ∈ V
34		nn0ssz 12271	. . . . . . . . . . 11 ⊢ ℕ0 ⊆ ℤ
35		mapss 8635	. . . . . . . . . . 11 ⊢ ((ℤ ∈ V ∧ ℕ0 ⊆ ℤ) → (ℕ0 ↑m 𝑎) ⊆ (ℤ ↑m 𝑎))
36	33, 34, 35	mp2an 688	. . . . . . . . . 10 ⊢ (ℕ0 ↑m 𝑎) ⊆ (ℤ ↑m 𝑎)
37	32, 36	vtoclg 3495	. . . . . . . . 9 ⊢ (𝑆 ∈ V → (ℕ0 ↑m 𝑆) ⊆ (ℤ ↑m 𝑆))
38	29, 37	syl 17	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (ℕ0 ↑m 𝑆) ⊆ (ℤ ↑m 𝑆))
39		simplr 765	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℕ0 ↑m 𝑆))
40	38, 39	sseldd 3918	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → 𝑏 ∈ (ℤ ↑m 𝑆))
41		coeq1 5755	. . . . . . . . 9 ⊢ (𝑑 = 𝑏 → (𝑑 ∘ 𝑀) = (𝑏 ∘ 𝑀))
42	41	fveq2d 6760	. . . . . . . 8 ⊢ (𝑑 = 𝑏 → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(𝑏 ∘ 𝑀)))
43		eqid 2738	. . . . . . . 8 ⊢ (𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀))) = (𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))
44		fvex 6769	. . . . . . . 8 ⊢ (𝑃‘(𝑏 ∘ 𝑀)) ∈ V
45	42, 43, 44	fvmpt 6857	. . . . . . 7 ⊢ (𝑏 ∈ (ℤ ↑m 𝑆) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀)))
46	40, 45	syl 17	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = (𝑃‘(𝑏 ∘ 𝑀)))
47		simprr 769	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)
48	46, 47	eqtr3d 2780	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → (𝑃‘(𝑏 ∘ 𝑀)) = 0)
49		reseq1 5874	. . . . . . . 8 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑐 ↾ 𝑂) = ((𝑏 ∘ 𝑀) ↾ 𝑂))
50	49	eqeq2d 2749	. . . . . . 7 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → (𝑎 = (𝑐 ↾ 𝑂) ↔ 𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂)))
51		fveqeq2 6765	. . . . . . 7 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑃‘𝑐) = 0 ↔ (𝑃‘(𝑏 ∘ 𝑀)) = 0))
52	50, 51	anbi12d 630	. . . . . 6 ⊢ (𝑐 = (𝑏 ∘ 𝑀) → ((𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) ↔ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0)))
53	52	rspcev 3552	. . . . 5 ⊢ (((𝑏 ∘ 𝑀) ∈ (ℕ0 ↑m 𝑇) ∧ (𝑎 = ((𝑏 ∘ 𝑀) ↾ 𝑂) ∧ (𝑃‘(𝑏 ∘ 𝑀)) = 0)) → ∃𝑐 ∈ (ℕ0 ↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))
54	20, 28, 48, 53	syl12anc 833	. . . 4 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑏 ∈ (ℕ0 ↑m 𝑆)) ∧ (𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)) → ∃𝑐 ∈ (ℕ0 ↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0))
55	54	rexlimdva2 3215	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0 ↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) → ∃𝑐 ∈ (ℕ0 ↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)))
56		simpr 484	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → 𝑐 ∈ (ℕ0 ↑m 𝑇))
57	16	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → 𝑇 ∈ V)
58		elmapg 8586	. . . . . . . . . . . 12 ⊢ ((ℕ0 ∈ V ∧ 𝑇 ∈ V) → (𝑐 ∈ (ℕ0 ↑m 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
59	2, 57, 58	sylancr 586	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑐 ∈ (ℕ0 ↑m 𝑇) ↔ 𝑐:𝑇⟶ℕ0))
60	56, 59	mpbid 231	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → 𝑐:𝑇⟶ℕ0)
61	60	adantr 480	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℕ0)
62	9	ad2antrr 722	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑀:𝑇–1-1→𝑆)
63		f1cnv 6723	. . . . . . . . . 10 ⊢ (𝑀:𝑇–1-1→𝑆 → ◡𝑀:ran 𝑀–1-1-onto→𝑇)
64		f1of 6700	. . . . . . . . . 10 ⊢ (◡𝑀:ran 𝑀–1-1-onto→𝑇 → ◡𝑀:ran 𝑀⟶𝑇)
65	62, 63, 64	3syl 18	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ◡𝑀:ran 𝑀⟶𝑇)
66		fco 6608	. . . . . . . . 9 ⊢ ((𝑐:𝑇⟶ℕ0 ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0)
67	61, 65, 66	syl2anc 583	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0)
68		c0ex 10900	. . . . . . . . . 10 ⊢ 0 ∈ V
69	68	fconst 6644	. . . . . . . . 9 ⊢ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}
70	69	a1i 11	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0})
71		disjdif 4402	. . . . . . . . 9 ⊢ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅
72	71	a1i 11	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
73		fun 6620	. . . . . . . 8 ⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℕ0 ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
74	67, 70, 72, 73	syl21anc 834	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}))
75		frn 6591	. . . . . . . . . . 11 ⊢ (𝑀:𝑇⟶𝑆 → ran 𝑀 ⊆ 𝑆)
76	9, 10, 75	3syl 18	. . . . . . . . . 10 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → ran 𝑀 ⊆ 𝑆)
77	76	ad2antrr 722	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ran 𝑀 ⊆ 𝑆)
78		undif 4412	. . . . . . . . 9 ⊢ (ran 𝑀 ⊆ 𝑆 ↔ (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
79	77, 78	sylib 217	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ran 𝑀 ∪ (𝑆 ∖ ran 𝑀)) = 𝑆)
80		0nn0 12178	. . . . . . . . . . 11 ⊢ 0 ∈ ℕ0
81		snssi 4738	. . . . . . . . . . 11 ⊢ (0 ∈ ℕ0 → {0} ⊆ ℕ0)
82	80, 81	ax-mp 5	. . . . . . . . . 10 ⊢ {0} ⊆ ℕ0
83		ssequn2 4113	. . . . . . . . . 10 ⊢ ({0} ⊆ ℕ0 ↔ (ℕ0 ∪ {0}) = ℕ0)
84	82, 83	mpbi 229	. . . . . . . . 9 ⊢ (ℕ0 ∪ {0}) = ℕ0
85	84	a1i 11	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℕ0 ∪ {0}) = ℕ0)
86	79, 85	feq23d 6579	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℕ0 ∪ {0}) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
87	74, 86	mpbid 231	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0)
88		elmapg 8586	. . . . . . . 8 ⊢ ((ℕ0 ∈ V ∧ 𝑆 ∈ V) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑m 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
89	2, 3, 88	sylancr 586	. . . . . . 7 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑m 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
90	89	ad2antrr 722	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑m 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℕ0))
91	87, 90	mpbird 256	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑m 𝑆))
92		simprl 767	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (𝑐 ↾ 𝑂))
93		resundir 5895	. . . . . . . . 9 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂))
94		resco 6143	. . . . . . . . . . 11 ⊢ ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ∘ (◡𝑀 ↾ 𝑂))
95		simpl2 1190	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → 𝑀:𝑇–1-1→𝑆)
96		df-f1 6423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀:𝑇–1-1→𝑆 ↔ (𝑀:𝑇⟶𝑆 ∧ Fun ◡𝑀))
97	96	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (𝑀:𝑇–1-1→𝑆 → Fun ◡𝑀)
98		funcnvres 6496	. . . . . . . . . . . . . . . 16 ⊢ (Fun ◡𝑀 → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂)))
99	95, 97, 98	3syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → ◡(𝑀 ↾ 𝑂) = (◡𝑀 ↾ (𝑀 “ 𝑂)))
100		simpl3 1191	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
101	100	cnveqd 5773	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → ◡(𝑀 ↾ 𝑂) = ◡( I ↾ 𝑂))
102		df-ima 5593	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 “ 𝑂) = ran (𝑀 ↾ 𝑂)
103	100	rneqd 5836	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → ran (𝑀 ↾ 𝑂) = ran ( I ↾ 𝑂))
104		rnresi 5972	. . . . . . . . . . . . . . . . . 18 ⊢ ran ( I ↾ 𝑂) = 𝑂
105	103, 104	eqtrdi 2795	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → ran (𝑀 ↾ 𝑂) = 𝑂)
106	102, 105	syl5eq 2791	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑀 “ 𝑂) = 𝑂)
107	106	reseq2d 5880	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (◡𝑀 ↾ (𝑀 “ 𝑂)) = (◡𝑀 ↾ 𝑂))
108	99, 101, 107	3eqtr3d 2786	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → ◡( I ↾ 𝑂) = (◡𝑀 ↾ 𝑂))
109		cnvresid 6497	. . . . . . . . . . . . . 14 ⊢ ◡( I ↾ 𝑂) = ( I ↾ 𝑂)
110	108, 109	eqtr3di 2794	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (◡𝑀 ↾ 𝑂) = ( I ↾ 𝑂))
111	110	coeq2d 5760	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ∘ ( I ↾ 𝑂)))
112		coires1 6157	. . . . . . . . . . . 12 ⊢ (𝑐 ∘ ( I ↾ 𝑂)) = (𝑐 ↾ 𝑂)
113	111, 112	eqtrdi 2795	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑐 ∘ (◡𝑀 ↾ 𝑂)) = (𝑐 ↾ 𝑂))
114	94, 113	syl5eq 2791	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → ((𝑐 ∘ ◡𝑀) ↾ 𝑂) = (𝑐 ↾ 𝑂))
115		dmres 5902	. . . . . . . . . . . 12 ⊢ dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0}))
116	68	snnz 4709	. . . . . . . . . . . . . . 15 ⊢ {0} ≠ ∅
117		dmxp 5827	. . . . . . . . . . . . . . 15 ⊢ ({0} ≠ ∅ → dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀))
118	116, 117	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ dom ((𝑆 ∖ ran 𝑀) × {0}) = (𝑆 ∖ ran 𝑀)
119	118	ineq2i 4140	. . . . . . . . . . . . 13 ⊢ (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = (𝑂 ∩ (𝑆 ∖ ran 𝑀))
120		inss1 4159	. . . . . . . . . . . . . . 15 ⊢ (𝑂 ∩ 𝑆) ⊆ 𝑂
121	103, 104	eqtr2di 2796	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → 𝑂 = ran (𝑀 ↾ 𝑂))
122		resss 5905	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ↾ 𝑂) ⊆ 𝑀
123		rnss 5837	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ↾ 𝑂) ⊆ 𝑀 → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀)
124	122, 123	mp1i 13	. . . . . . . . . . . . . . . 16 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → ran (𝑀 ↾ 𝑂) ⊆ ran 𝑀)
125	121, 124	eqsstrd 3955	. . . . . . . . . . . . . . 15 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → 𝑂 ⊆ ran 𝑀)
126	120, 125	sstrid 3928	. . . . . . . . . . . . . 14 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑂 ∩ 𝑆) ⊆ ran 𝑀)
127		inssdif0 4300	. . . . . . . . . . . . . 14 ⊢ ((𝑂 ∩ 𝑆) ⊆ ran 𝑀 ↔ (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
128	126, 127	sylib 217	. . . . . . . . . . . . 13 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑂 ∩ (𝑆 ∖ ran 𝑀)) = ∅)
129	119, 128	syl5eq 2791	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑂 ∩ dom ((𝑆 ∖ ran 𝑀) × {0})) = ∅)
130	115, 129	syl5eq 2791	. . . . . . . . . . 11 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → dom (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
131		relres 5909	. . . . . . . . . . . 12 ⊢ Rel (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)
132		reldm0 5826	. . . . . . . . . . . 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 233	. . . . . . . . . 10 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂) = ∅)
135	114, 134	uneq12d 4094	. . . . . . . . 9 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (((𝑐 ∘ ◡𝑀) ↾ 𝑂) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ↾ 𝑂)) = ((𝑐 ↾ 𝑂) ∪ ∅))
136	93, 135	syl5eq 2791	. . . . . . . 8 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) = ((𝑐 ↾ 𝑂) ∪ ∅))
137		un0 4321	. . . . . . . 8 ⊢ ((𝑐 ↾ 𝑂) ∪ ∅) = (𝑐 ↾ 𝑂)
138	136, 137	eqtr2di 2796	. . . . . . 7 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
139	138	adantr 480	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
140	92, 139	eqtrd 2778	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
141		fss 6601	. . . . . . . . . . . . 13 ⊢ ((𝑐:𝑇⟶ℕ0 ∧ ℕ0 ⊆ ℤ) → 𝑐:𝑇⟶ℤ)
142	60, 34, 141	sylancl 585	. . . . . . . . . . . 12 ⊢ (((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) → 𝑐:𝑇⟶ℤ)
143	142	adantr 480	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → 𝑐:𝑇⟶ℤ)
144		fco 6608	. . . . . . . . . . 11 ⊢ ((𝑐:𝑇⟶ℤ ∧ ◡𝑀:ran 𝑀⟶𝑇) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ)
145	143, 65, 144	syl2anc 583	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ)
146		fun 6620	. . . . . . . . . 10 ⊢ ((((𝑐 ∘ ◡𝑀):ran 𝑀⟶ℤ ∧ ((𝑆 ∖ ran 𝑀) × {0}):(𝑆 ∖ ran 𝑀)⟶{0}) ∧ (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀)) = ∅) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
147	145, 70, 72, 146	syl21anc 834	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}))
148		0z 12260	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℤ
149		snssi 4738	. . . . . . . . . . . . 13 ⊢ (0 ∈ ℤ → {0} ⊆ ℤ)
150	148, 149	ax-mp 5	. . . . . . . . . . . 12 ⊢ {0} ⊆ ℤ
151		ssequn2 4113	. . . . . . . . . . . 12 ⊢ ({0} ⊆ ℤ ↔ (ℤ ∪ {0}) = ℤ)
152	150, 151	mpbi 229	. . . . . . . . . . 11 ⊢ (ℤ ∪ {0}) = ℤ
153	152	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (ℤ ∪ {0}) = ℤ)
154	79, 153	feq23d 6579	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):(ran 𝑀 ∪ (𝑆 ∖ ran 𝑀))⟶(ℤ ∪ {0}) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
155	147, 154	mpbid 231	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ)
156		elmapg 8586	. . . . . . . . . 10 ⊢ ((ℤ ∈ V ∧ 𝑆 ∈ V) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
157	33, 3, 156	sylancr 586	. . . . . . . . 9 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
158	157	ad2antrr 722	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) ↔ ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})):𝑆⟶ℤ))
159	155, 158	mpbird 256	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆))
160		coeq1 5755	. . . . . . . . 9 ⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑑 ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀))
161	160	fveq2d 6760	. . . . . . . 8 ⊢ (𝑑 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑃‘(𝑑 ∘ 𝑀)) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
162		fvex 6769	. . . . . . . 8 ⊢ (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) ∈ V
163	161, 43, 162	fvmpt 6857	. . . . . . 7 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℤ ↑m 𝑆) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
164	159, 163	syl 17	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)))
165		coundir 6141	. . . . . . . 8 ⊢ (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀))
166		coass 6158	. . . . . . . . . . 11 ⊢ ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ (◡𝑀 ∘ 𝑀))
167		f1cocnv1 6729	. . . . . . . . . . . . 13 ⊢ (𝑀:𝑇–1-1→𝑆 → (◡𝑀 ∘ 𝑀) = ( I ↾ 𝑇))
168	167	coeq2d 5760	. . . . . . . . . . . 12 ⊢ (𝑀:𝑇–1-1→𝑆 → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
169	62, 168	syl 17	. . . . . . . . . . 11 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ (◡𝑀 ∘ 𝑀)) = (𝑐 ∘ ( I ↾ 𝑇)))
170	166, 169	syl5eq 2791	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ◡𝑀) ∘ 𝑀) = (𝑐 ∘ ( I ↾ 𝑇)))
171	118	ineq1i 4139	. . . . . . . . . . . . 13 ⊢ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀)
172		incom 4131	. . . . . . . . . . . . 13 ⊢ ((𝑆 ∖ ran 𝑀) ∩ ran 𝑀) = (ran 𝑀 ∩ (𝑆 ∖ ran 𝑀))
173	171, 172, 71	3eqtri 2770	. . . . . . . . . . . 12 ⊢ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅
174		coeq0 6148	. . . . . . . . . . . 12 ⊢ ((((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅ ↔ (dom ((𝑆 ∖ ran 𝑀) × {0}) ∩ ran 𝑀) = ∅)
175	173, 174	mpbir 230	. . . . . . . . . . 11 ⊢ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅
176	175	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀) = ∅)
177	170, 176	uneq12d 4094	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅))
178		un0 4321	. . . . . . . . . 10 ⊢ ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = (𝑐 ∘ ( I ↾ 𝑇))
179		fcoi1 6632	. . . . . . . . . . 11 ⊢ (𝑐:𝑇⟶ℕ0 → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
180	61, 179	syl 17	. . . . . . . . . 10 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑐 ∘ ( I ↾ 𝑇)) = 𝑐)
181	178, 180	syl5eq 2791	. . . . . . . . 9 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑐 ∘ ( I ↾ 𝑇)) ∪ ∅) = 𝑐)
182	177, 181	eqtrd 2778	. . . . . . . 8 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∘ 𝑀) ∪ (((𝑆 ∖ ran 𝑀) × {0}) ∘ 𝑀)) = 𝑐)
183	165, 182	syl5eq 2791	. . . . . . 7 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀) = 𝑐)
184	183	fveq2d 6760	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘(((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∘ 𝑀)) = (𝑃‘𝑐))
185		simprr 769	. . . . . 6 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → (𝑃‘𝑐) = 0)
186	164, 184, 185	3eqtrd 2782	. . . . 5 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)
187		reseq1 5874	. . . . . . . 8 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑏 ↾ 𝑂) = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂))
188	187	eqeq2d 2749	. . . . . . 7 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (𝑎 = (𝑏 ↾ 𝑂) ↔ 𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂)))
189		fveqeq2 6765	. . . . . . 7 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → (((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0 ↔ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0))
190	188, 189	anbi12d 630	. . . . . 6 ⊢ (𝑏 = ((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) → ((𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)))
191	190	rspcev 3552	. . . . 5 ⊢ ((((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ∈ (ℕ0 ↑m 𝑆) ∧ (𝑎 = (((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0})) ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘((𝑐 ∘ ◡𝑀) ∪ ((𝑆 ∖ ran 𝑀) × {0}))) = 0)) → ∃𝑏 ∈ (ℕ0 ↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0))
192	91, 140, 186, 191	syl12anc 833	. . . 4 ⊢ ((((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) ∧ 𝑐 ∈ (ℕ0 ↑m 𝑇)) ∧ (𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)) → ∃𝑏 ∈ (ℕ0 ↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0))
193	192	rexlimdva2 3215	. . 3 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑐 ∈ (ℕ0 ↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0) → ∃𝑏 ∈ (ℕ0 ↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)))
194	55, 193	impbid 211	. 2 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → (∃𝑏 ∈ (ℕ0 ↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0) ↔ ∃𝑐 ∈ (ℕ0 ↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)))
195	194	abbidv 2808	1 ⊢ ((𝑆 ∈ V ∧ 𝑀:𝑇–1-1→𝑆 ∧ (𝑀 ↾ 𝑂) = ( I ↾ 𝑂)) → {𝑎 ∣ ∃𝑏 ∈ (ℕ0 ↑m 𝑆)(𝑎 = (𝑏 ↾ 𝑂) ∧ ((𝑑 ∈ (ℤ ↑m 𝑆) ↦ (𝑃‘(𝑑 ∘ 𝑀)))‘𝑏) = 0)} = {𝑎 ∣ ∃𝑐 ∈ (ℕ0 ↑m 𝑇)(𝑎 = (𝑐 ↾ 𝑂) ∧ (𝑃‘𝑐) = 0)})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  {cab 2715   ≠ wne 2942  ∃wrex 3064  Vcvv 3422   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  {csn 4558   ↦ cmpt 5153   I cid 5479   × cxp 5578  ^◡ccnv 5579  dom cdm 5580  ran crn 5581   ↾ cres 5582   “ cima 5583   ∘ ccom 5584  Rel wrel 5585  Fun wfun 6412  ⟶wf 6414  –1-1→wf1 6415  –1-1-onto→wf1o 6417  ‘cfv 6418  (class class class)co 7255   ↑_m cmap 8573  0cc0 10802  ℕ₀cn0 12163  ℤcz 12249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-map 8575  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250

This theorem is referenced by:  eldioph2  40500  eldioph2b  40501