rexrabdioph - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > rexrabdioph		Structured version Visualization version GIF version

Theorem rexrabdioph 43754

Description: Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014.)

**Hypotheses**
Ref	Expression
rexrabdioph.1	⊢ 𝑀 = (𝑁 + 1)
rexrabdioph.2	⊢ (𝑣 = (𝑡‘𝑀) → (𝜓 ↔ 𝜒))
rexrabdioph.3	⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝜒 ↔ 𝜑))

**Assertion**
Ref	Expression
rexrabdioph	⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} ∈ (Dioph‘𝑁))

Distinct variable groups: 𝑡,𝑁,𝑢,𝑣 𝑡,𝑀,𝑢,𝑣 𝜑,𝑢,𝑣 𝜓,𝑡 𝜒,𝑣 Allowed substitution hints: 𝜑(𝑡) 𝜓(𝑣, 𝑢) 𝜒(𝑢, 𝑡)

Proof of Theorem rexrabdioph Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rab 3414	. . . . . 6 ⊢ {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} = {𝑎 ∣ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)}
2		dfsbcq 3741	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ([𝑏 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
3	2	cbvrexvw 3242	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓 ↔ ∃𝑐 ∈ ℕ₀ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)
4	3	anbi2i 635	. . . . . . . . 9 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑐 ∈ ℕ₀ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
5		r19.42v 3195	. . . . . . . . 9 ⊢ (∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑐 ∈ ℕ₀ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
6	4, 5	bitr4i 281	. . . . . . . 8 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) ↔ ∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
7		simpll 779	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑁 ∈ ℕ₀)
8		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)))
9		simplr 781	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑐 ∈ ℕ₀)
10		rexrabdioph.1	. . . . . . . . . . . . . 14 ⊢ 𝑀 = (𝑁 + 1)
11	10	mapfzcons 43680	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ 𝑐 ∈ ℕ₀) → (𝑎 ∪ {⟨𝑀, 𝑐⟩}) ∈ (ℕ₀ ↑_m (1...𝑀)))
12	7, 8, 9, 11	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → (𝑎 ∪ {⟨𝑀, 𝑐⟩}) ∈ (ℕ₀ ↑_m (1...𝑀)))
13	12	adantrr 730	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → (𝑎 ∪ {⟨𝑀, 𝑐⟩}) ∈ (ℕ₀ ↑_m (1...𝑀)))
14	10	mapfzcons2 43683	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ 𝑐 ∈ ℕ₀) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) = 𝑐)
15	8, 9, 14	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) = 𝑐)
16	15	eqcomd 2767	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑐 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀))
17	10	mapfzcons1 43681	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) = 𝑎)
18	17	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) = 𝑎)
19	18	eqcomd 2767	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))
20	19	sbceq1d 3744	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ([𝑎 / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
21	16, 20	sbceqbid 3746	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ([𝑐 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
22	21	biimpd 232	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ([𝑐 / 𝑣][𝑎 / 𝑢]𝜓 → [((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
23	22	impr 460	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → [((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓)
24	19	adantrr 730	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))
25		fveq1 6876	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑏‘𝑀) = ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀))
26		reseq1 5964	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑏 ↾ (1...𝑁)) = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))
27	26	sbceq1d 3744	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → ([(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
28	25, 27	sbceqbid 3746	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
29	26	eqeq2d 2772	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁))))
30	28, 29	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ([((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))))
31	30	rspcev 3577	. . . . . . . . . . 11 ⊢ (((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ∈ (ℕ₀ ↑_m (1...𝑀)) ∧ ([((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))) → ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))
32	13, 23, 24, 31	syl12anc 850	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))
33	32	rexlimdva2 3166	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) → ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))))
34		elmapi 8853	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (ℕ₀ ↑_m (1...𝑀)) → 𝑏:(1...𝑀)⟶ℕ₀)
35		nn0p1nn 12626	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
36	10, 35	eqeltrid 2865	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ ℕ)
37		elfz1end 13668	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀))
38	36, 37	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ (1...𝑀))
39		ffvelcdm 7073	. . . . . . . . . . . . 13 ⊢ ((𝑏:(1...𝑀)⟶ℕ₀ ∧ 𝑀 ∈ (1...𝑀)) → (𝑏‘𝑀) ∈ ℕ₀)
40	34, 38, 39	syl2anr 609	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) → (𝑏‘𝑀) ∈ ℕ₀)
41	40	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → (𝑏‘𝑀) ∈ ℕ₀)
42		simprr 785	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → 𝑎 = (𝑏 ↾ (1...𝑁)))
43	10	mapfzcons1cl 43682	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (ℕ₀ ↑_m (1...𝑀)) → (𝑏 ↾ (1...𝑁)) ∈ (ℕ₀ ↑_m (1...𝑁)))
44	43	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → (𝑏 ↾ (1...𝑁)) ∈ (ℕ₀ ↑_m (1...𝑁)))
45	42, 44	eqeltrd 2861	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)))
46		simprl 783	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓)
47		dfsbcq 3741	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑏 ↾ (1...𝑁)) → ([𝑎 / 𝑢]𝜓 ↔ [(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
48	47	sbcbidv 3794	. . . . . . . . . . . . 13 ⊢ (𝑎 = (𝑏 ↾ (1...𝑁)) → ([(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
49	48	ad2antll 742	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → ([(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
50	46, 49	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)
51		dfsbcq 3741	. . . . . . . . . . . . 13 ⊢ (𝑐 = (𝑏‘𝑀) → ([𝑐 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓))
52	51	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑏‘𝑀) → ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)))
53	52	rspcev 3577	. . . . . . . . . . 11 ⊢ (((𝑏‘𝑀) ∈ ℕ₀ ∧ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)) → ∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
54	41, 45, 50, 53	syl12anc 850	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → ∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
55	54	rexlimdva2 3166	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) → ∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)))
56	33, 55	impbid 215	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → (∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) ↔ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))))
57	6, 56	bitrid 286	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) ↔ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))))
58	57	abbidv 2827	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → {𝑎 ∣ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))})
59	1, 58	eqtrid 2808	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))})
60		nfcv 2923	. . . . . 6 ⊢ Ⅎ𝑢(ℕ₀ ↑_m (1...𝑁))
61		nfcv 2923	. . . . . 6 ⊢ Ⅎ𝑎(ℕ₀ ↑_m (1...𝑁))
62		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑎∃𝑣 ∈ ℕ₀ 𝜓
63		nfcv 2923	. . . . . . 7 ⊢ Ⅎ𝑢ℕ₀
64		nfcv 2923	. . . . . . . 8 ⊢ Ⅎ𝑢𝑏
65		nfsbc1v 3759	. . . . . . . 8 ⊢ Ⅎ𝑢[𝑎 / 𝑢]𝜓
66	64, 65	nfsbcw 3761	. . . . . . 7 ⊢ Ⅎ𝑢[𝑏 / 𝑣][𝑎 / 𝑢]𝜓
67	63, 66	nfrexw 3311	. . . . . 6 ⊢ Ⅎ𝑢∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓
68		sbceq1a 3750	. . . . . . . 8 ⊢ (𝑢 = 𝑎 → (𝜓 ↔ [𝑎 / 𝑢]𝜓))
69	68	rexbidv 3187	. . . . . . 7 ⊢ (𝑢 = 𝑎 → (∃𝑣 ∈ ℕ₀ 𝜓 ↔ ∃𝑣 ∈ ℕ₀ [𝑎 / 𝑢]𝜓))
70		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑏[𝑎 / 𝑢]𝜓
71		nfsbc1v 3759	. . . . . . . 8 ⊢ Ⅎ𝑣[𝑏 / 𝑣][𝑎 / 𝑢]𝜓
72		sbceq1a 3750	. . . . . . . 8 ⊢ (𝑣 = 𝑏 → ([𝑎 / 𝑢]𝜓 ↔ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓))
73	70, 71, 72	cbvrexw 3306	. . . . . . 7 ⊢ (∃𝑣 ∈ ℕ₀ [𝑎 / 𝑢]𝜓 ↔ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)
74	69, 73	bitrdi 290	. . . . . 6 ⊢ (𝑢 = 𝑎 → (∃𝑣 ∈ ℕ₀ 𝜓 ↔ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓))
75	60, 61, 62, 67, 74	cbvrabw 3447	. . . . 5 ⊢ {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} = {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓}
76		fveq1 6876	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (𝑡‘𝑀) = (𝑏‘𝑀))
77		reseq1 5964	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (𝑡 ↾ (1...𝑁)) = (𝑏 ↾ (1...𝑁)))
78	77	sbceq1d 3744	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → ([(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
79	76, 78	sbceqbid 3746	. . . . . . 7 ⊢ (𝑡 = 𝑏 → ([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
80	79	rexrab 3654	. . . . . 6 ⊢ (∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))
81	80	abbii 2828	. . . . 5 ⊢ {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))}
82	59, 75, 81	3eqtr4g 2821	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))})
83		fvex 6890	. . . . . . . 8 ⊢ (𝑡‘𝑀) ∈ V
84		vex 3455	. . . . . . . . 9 ⊢ 𝑡 ∈ V
85	84	resex 6020	. . . . . . . 8 ⊢ (𝑡 ↾ (1...𝑁)) ∈ V
86		rexrabdioph.2	. . . . . . . . 9 ⊢ (𝑣 = (𝑡‘𝑀) → (𝜓 ↔ 𝜒))
87		rexrabdioph.3	. . . . . . . . 9 ⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝜒 ↔ 𝜑))
88	86, 87	sylan9bb 519	. . . . . . . 8 ⊢ ((𝑣 = (𝑡‘𝑀) ∧ 𝑢 = (𝑡 ↾ (1...𝑁))) → (𝜓 ↔ 𝜑))
89	83, 85, 88	sbc2ie 3814	. . . . . . 7 ⊢ ([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ 𝜑)
90	89	rabbii 3418	. . . . . 6 ⊢ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓} = {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}
91	90	rexeqi 3319	. . . . 5 ⊢ (∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁)))
92	91	abbii 2828	. . . 4 ⊢ {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))}
93	82, 92	eqtrdi 2812	. . 3 ⊢ (𝑁 ∈ ℕ₀ → {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))})
94	93	adantr 486	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))})
95		simpl 488	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → 𝑁 ∈ ℕ₀)
96		nn0z 12698	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
97		uzid 12961	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
98		peano2uz 13009	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘𝑁) → (𝑁 + 1) ∈ (ℤ_≥‘𝑁))
99	96, 97, 98	3syl 19	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ (ℤ_≥‘𝑁))
100	10, 99	eqeltrid 2865	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ (ℤ_≥‘𝑁))
101	100	adantr 486	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → 𝑀 ∈ (ℤ_≥‘𝑁))
102		simpr 490	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀))
103		diophrex 43739	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑀 ∈ (ℤ_≥‘𝑁) ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁))
104	95, 101, 102, 103	syl3anc 1398	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁))
105	94, 104	eqeltrd 2861	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} ∈ (Dioph‘𝑁))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 {cab 2739 ∃wrex 3087 {crab 3413 [wsbc 3739 ∪ cun 3897 {csn 4584 ⟨cop 4590 ↾ cres 5653 ⟶wf 6527 ‘cfv 6531 (class class class)co 7412 ↑_m cmap 8831 1c1 11182 + caddc 11184 ℕcn 12316 ℕ₀cn0 12587 ℤcz 12674 ℤ_≥cuz 12946 ...cfz 13620 Diophcdioph 43719

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7740 ax-inf2 9626 ax-cnex 11237 ax-resscn 11238 ax-1cn 11239 ax-icn 11240 ax-addcl 11241 ax-addrcl 11242 ax-mulcl 11243 ax-mulrcl 11244 ax-mulcom 11245 ax-addass 11246 ax-mulass 11247 ax-distr 11248 ax-i2m1 11249 ax-1ne0 11250 ax-1rid 11251 ax-rnegex 11252 ax-rrecex 11253 ax-cnre 11254 ax-pre-lttri 11255 ax-pre-lttrn 11256 ax-pre-ltadd 11257 ax-pre-mulgt0 11258

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6297 df-ord 6358 df-on 6359 df-lim 6360 df-suc 6361 df-iota 6487 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7682 df-om 7867 df-1st 7990 df-2nd 7991 df-frecs 8283 df-wrecs 8314 df-recs 8363 df-rdg 8402 df-1o 8460 df-oadd 8464 df-er 8701 df-map 8833 df-en 8958 df-dom 8959 df-sdom 8960 df-fin 8961 df-dju 9963 df-card 10001 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11524 df-neg 11525 df-nn 12317 df-n0 12588 df-z 12675 df-uz 12947 df-fz 13621 df-hash 14455 df-mzpcl 43687 df-mzp 43688 df-dioph 43720

This theorem is used by: rexfrabdioph 43755 elnn0rabdioph 43763 dvdsrabdioph 43770

W3C validator