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 43562

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 3420	. . . . . 6 ⊢ {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} = {𝑎 ∣ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)}
2		dfsbcq 3749	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ([𝑏 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
3	2	cbvrexvw 3247	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓 ↔ ∃𝑐 ∈ ℕ₀ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)
4	3	anbi2i 635	. . . . . . . . 9 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑐 ∈ ℕ₀ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
5		r19.42v 3200	. . . . . . . . 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 43488	. . . . . . . . . . . . 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 43491	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ 𝑐 ∈ ℕ₀) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) = 𝑐)
15	8, 9, 14	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) = 𝑐)
16	15	eqcomd 2772	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑐 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀))
17	10	mapfzcons1 43489	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) = 𝑎)
18	17	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) = 𝑎)
19	18	eqcomd 2772	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))
20	19	sbceq1d 3752	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ([𝑎 / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
21	16, 20	sbceqbid 3754	. . . . . . . . . . . . 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 6887	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑏‘𝑀) = ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀))
26		reseq1 5977	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑏 ↾ (1...𝑁)) = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))
27	26	sbceq1d 3752	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → ([(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
28	25, 27	sbceqbid 3754	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
29	26	eqeq2d 2777	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁))))
30	28, 29	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ([((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))))
31	30	rspcev 3584	. . . . . . . . . . 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 3171	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) → ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))))
34		elmapi 8855	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (ℕ₀ ↑_m (1...𝑀)) → 𝑏:(1...𝑀)⟶ℕ₀)
35		nn0p1nn 12561	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
36	10, 35	eqeltrid 2870	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ ℕ)
37		elfz1end 13601	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀))
38	36, 37	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ (1...𝑀))
39		ffvelcdm 7083	. . . . . . . . . . . . 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 43490	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (ℕ₀ ↑_m (1...𝑀)) → (𝑏 ↾ (1...𝑁)) ∈ (ℕ₀ ↑_m (1...𝑁)))
44	43	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → (𝑏 ↾ (1...𝑁)) ∈ (ℕ₀ ↑_m (1...𝑁)))
45	42, 44	eqeltrd 2866	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)))
46		simprl 783	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓)
47		dfsbcq 3749	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑏 ↾ (1...𝑁)) → ([𝑎 / 𝑢]𝜓 ↔ [(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
48	47	sbcbidv 3802	. . . . . . . . . . . . 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 3749	. . . . . . . . . . . . 13 ⊢ (𝑐 = (𝑏‘𝑀) → ([𝑐 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓))
52	51	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑏‘𝑀) → ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)))
53	52	rspcev 3584	. . . . . . . . . . 11 ⊢ (((𝑏‘𝑀) ∈ ℕ₀ ∧ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)) → ∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
54	41, 45, 50, 53	syl12anc 850	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → ∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
55	54	rexlimdva2 3171	. . . . . . . . 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 2832	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → {𝑎 ∣ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))})
59	1, 58	eqtrid 2813	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))})
60		nfcv 2928	. . . . . 6 ⊢ Ⅎ𝑢(ℕ₀ ↑_m (1...𝑁))
61		nfcv 2928	. . . . . 6 ⊢ Ⅎ𝑎(ℕ₀ ↑_m (1...𝑁))
62		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑎∃𝑣 ∈ ℕ₀ 𝜓
63		nfcv 2928	. . . . . . 7 ⊢ Ⅎ𝑢ℕ₀
64		nfcv 2928	. . . . . . . 8 ⊢ Ⅎ𝑢𝑏
65		nfsbc1v 3767	. . . . . . . 8 ⊢ Ⅎ𝑢[𝑎 / 𝑢]𝜓
66	64, 65	nfsbcw 3769	. . . . . . 7 ⊢ Ⅎ𝑢[𝑏 / 𝑣][𝑎 / 𝑢]𝜓
67	63, 66	nfrexw 3316	. . . . . 6 ⊢ Ⅎ𝑢∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓
68		sbceq1a 3758	. . . . . . . 8 ⊢ (𝑢 = 𝑎 → (𝜓 ↔ [𝑎 / 𝑢]𝜓))
69	68	rexbidv 3192	. . . . . . 7 ⊢ (𝑢 = 𝑎 → (∃𝑣 ∈ ℕ₀ 𝜓 ↔ ∃𝑣 ∈ ℕ₀ [𝑎 / 𝑢]𝜓))
70		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑏[𝑎 / 𝑢]𝜓
71		nfsbc1v 3767	. . . . . . . 8 ⊢ Ⅎ𝑣[𝑏 / 𝑣][𝑎 / 𝑢]𝜓
72		sbceq1a 3758	. . . . . . . 8 ⊢ (𝑣 = 𝑏 → ([𝑎 / 𝑢]𝜓 ↔ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓))
73	70, 71, 72	cbvrexw 3311	. . . . . . 7 ⊢ (∃𝑣 ∈ ℕ₀ [𝑎 / 𝑢]𝜓 ↔ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)
74	69, 73	bitrdi 290	. . . . . 6 ⊢ (𝑢 = 𝑎 → (∃𝑣 ∈ ℕ₀ 𝜓 ↔ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓))
75	60, 61, 62, 67, 74	cbvrabw 3454	. . . . 5 ⊢ {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} = {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓}
76		fveq1 6887	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (𝑡‘𝑀) = (𝑏‘𝑀))
77		reseq1 5977	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (𝑡 ↾ (1...𝑁)) = (𝑏 ↾ (1...𝑁)))
78	77	sbceq1d 3752	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → ([(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
79	76, 78	sbceqbid 3754	. . . . . . 7 ⊢ (𝑡 = 𝑏 → ([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
80	79	rexrab 3662	. . . . . 6 ⊢ (∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))
81	80	abbii 2833	. . . . 5 ⊢ {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))}
82	59, 75, 81	3eqtr4g 2826	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))})
83		fvex 6901	. . . . . . . 8 ⊢ (𝑡‘𝑀) ∈ V
84		vex 3462	. . . . . . . . 9 ⊢ 𝑡 ∈ V
85	84	resex 6033	. . . . . . . 8 ⊢ (𝑡 ↾ (1...𝑁)) ∈ V
86		rexrabdioph.2	. . . . . . . . 9 ⊢ (𝑣 = (𝑡‘𝑀) → (𝜓 ↔ 𝜒))
87		rexrabdioph.3	. . . . . . . . 9 ⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝜒 ↔ 𝜑))
88	86, 87	sylan9bb 519	. . . . . . . 8 ⊢ ((𝑣 = (𝑡‘𝑀) ∧ 𝑢 = (𝑡 ↾ (1...𝑁))) → (𝜓 ↔ 𝜑))
89	83, 85, 88	sbc2ie 3822	. . . . . . 7 ⊢ ([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ 𝜑)
90	89	rabbii 3424	. . . . . 6 ⊢ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓} = {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}
91	90	rexeqi 3325	. . . . 5 ⊢ (∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁)))
92	91	abbii 2833	. . . 4 ⊢ {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))}
93	82, 92	eqtrdi 2817	. . 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 12633	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
97		uzid 12895	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
98		peano2uz 12943	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘𝑁) → (𝑁 + 1) ∈ (ℤ_≥‘𝑁))
99	96, 97, 98	3syl 19	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ (ℤ_≥‘𝑁))
100	10, 99	eqeltrid 2870	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ (ℤ_≥‘𝑁))
101	100	adantr 486	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → 𝑀 ∈ (ℤ_≥‘𝑁))
102		simpr 490	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀))
103		diophrex 43547	. . 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 2866	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 2146 {cab 2744 ∃wrex 3092 {crab 3419 [wsbc 3747 ∪ cun 3906 {csn 4594 ⟨cop 4600 ↾ cres 5668 ⟶wf 6539 ‘cfv 6543 (class class class)co 7423 ↑_m cmap 8833 1c1 11119 + caddc 11121 ℕcn 12251 ℕ₀cn0 12522 ℤcz 12609 ℤ_≥cuz 12880 ...cfz 13553 Diophcdioph 43527

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-inf2 9620 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-of 7687 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-oadd 8466 df-er 8703 df-map 8835 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-dju 9906 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-nn 12252 df-n0 12523 df-z 12610 df-uz 12881 df-fz 13554 df-hash 14387 df-mzpcl 43495 df-mzp 43496 df-dioph 43528

This theorem is used by: rexfrabdioph 43563 elnn0rabdioph 43571 dvdsrabdioph 43578

W3C validator