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 43994

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 3417	. . . . . 6 ⊢ {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} = {𝑎 ∣ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)}
2		dfsbcq 3744	. . . . . . . . . . 11 ⊢ (𝑏 = 𝑐 → ([𝑏 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
3	2	cbvrexvw 3245	. . . . . . . . . 10 ⊢ (∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓 ↔ ∃𝑐 ∈ ℕ₀ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)
4	3	anbi2i 635	. . . . . . . . 9 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑐 ∈ ℕ₀ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
5		r19.42v 3198	. . . . . . . . 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 43920	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ 𝑐 ∈ ℕ₀) → (𝑎 ∪ {⟨𝑀, 𝑐⟩}) ∈ (ℕ₀ ↑_m (1...𝑀)))
12	7, 8, 9, 11	syl3anc 1399	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → (𝑎 ∪ {⟨𝑀, 𝑐⟩}) ∈ (ℕ₀ ↑_m (1...𝑀)))
13	12	adantrr 730	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → (𝑎 ∪ {⟨𝑀, 𝑐⟩}) ∈ (ℕ₀ ↑_m (1...𝑀)))
14	10	mapfzcons2 43923	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ 𝑐 ∈ ℕ₀) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) = 𝑐)
15	8, 9, 14	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) = 𝑐)
16	15	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑐 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀))
17	10	mapfzcons1 43921	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) = 𝑎)
18	17	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) = 𝑎)
19	18	eqcomd 2769	. . . . . . . . . . . . . . 15 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))
20	19	sbceq1d 3747	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑐 ∈ ℕ₀) ∧ 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁))) → ([𝑎 / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
21	16, 20	sbceqbid 3749	. . . . . . . . . . . . 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 6907	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑏‘𝑀) = ((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀))
26		reseq1 5975	. . . . . . . . . . . . . . 15 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑏 ↾ (1...𝑁)) = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))
27	26	sbceq1d 3747	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → ([(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
28	25, 27	sbceqbid 3749	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓))
29	26	eqeq2d 2774	. . . . . . . . . . . . 13 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁))))
30	28, 29	anbi12d 644	. . . . . . . . . . . 12 ⊢ (𝑏 = (𝑎 ∪ {⟨𝑀, 𝑐⟩}) → (([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ([((𝑎 ∪ {⟨𝑀, 𝑐⟩})‘𝑀) / 𝑣][((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = ((𝑎 ∪ {⟨𝑀, 𝑐⟩}) ↾ (1...𝑁)))))
31	30	rspcev 3580	. . . . . . . . . . 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 3169	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) → ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))))
34		elmapi 8897	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (ℕ₀ ↑_m (1...𝑀)) → 𝑏:(1...𝑀)⟶ℕ₀)
35		nn0p1nn 12672	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
36	10, 35	eqeltrid 2868	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ ℕ)
37		elfz1end 13715	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀))
38	36, 37	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ (1...𝑀))
39		ffvelcdm 7105	. . . . . . . . . . . . 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 43922	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ (ℕ₀ ↑_m (1...𝑀)) → (𝑏 ↾ (1...𝑁)) ∈ (ℕ₀ ↑_m (1...𝑁)))
44	43	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → (𝑏 ↾ (1...𝑁)) ∈ (ℕ₀ ↑_m (1...𝑁)))
45	42, 44	eqeltrd 2864	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → 𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)))
46		simprl 783	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓)
47		dfsbcq 3744	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (𝑏 ↾ (1...𝑁)) → ([𝑎 / 𝑢]𝜓 ↔ [(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
48	47	sbcbidv 3797	. . . . . . . . . . . . 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 3744	. . . . . . . . . . . . 13 ⊢ (𝑐 = (𝑏‘𝑀) → ([𝑐 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓))
52	51	anbi2d 642	. . . . . . . . . . . 12 ⊢ (𝑐 = (𝑏‘𝑀) → ((𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)))
53	52	rspcev 3580	. . . . . . . . . . 11 ⊢ (((𝑏‘𝑀) ∈ ℕ₀ ∧ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)) → ∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
54	41, 45, 50, 53	syl12anc 850	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → ∃𝑐 ∈ ℕ₀ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))
55	54	rexlimdva2 3169	. . . . . . . . 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 2829	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → {𝑎 ∣ (𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∧ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))})
59	1, 58	eqtrid 2810	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))})
60		nfcv 2926	. . . . . 6 ⊢ Ⅎ𝑢(ℕ₀ ↑_m (1...𝑁))
61		nfcv 2926	. . . . . 6 ⊢ Ⅎ𝑎(ℕ₀ ↑_m (1...𝑁))
62		nfv 1949	. . . . . 6 ⊢ Ⅎ𝑎∃𝑣 ∈ ℕ₀ 𝜓
63		nfcv 2926	. . . . . . 7 ⊢ Ⅎ𝑢ℕ₀
64		nfcv 2926	. . . . . . . 8 ⊢ Ⅎ𝑢𝑏
65		nfsbc1v 3762	. . . . . . . 8 ⊢ Ⅎ𝑢[𝑎 / 𝑢]𝜓
66	64, 65	nfsbcw 3764	. . . . . . 7 ⊢ Ⅎ𝑢[𝑏 / 𝑣][𝑎 / 𝑢]𝜓
67	63, 66	nfrexw 3314	. . . . . 6 ⊢ Ⅎ𝑢∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓
68		sbceq1a 3753	. . . . . . . 8 ⊢ (𝑢 = 𝑎 → (𝜓 ↔ [𝑎 / 𝑢]𝜓))
69	68	rexbidv 3190	. . . . . . 7 ⊢ (𝑢 = 𝑎 → (∃𝑣 ∈ ℕ₀ 𝜓 ↔ ∃𝑣 ∈ ℕ₀ [𝑎 / 𝑢]𝜓))
70		nfv 1949	. . . . . . . 8 ⊢ Ⅎ𝑏[𝑎 / 𝑢]𝜓
71		nfsbc1v 3762	. . . . . . . 8 ⊢ Ⅎ𝑣[𝑏 / 𝑣][𝑎 / 𝑢]𝜓
72		sbceq1a 3753	. . . . . . . 8 ⊢ (𝑣 = 𝑏 → ([𝑎 / 𝑢]𝜓 ↔ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓))
73	70, 71, 72	cbvrexw 3309	. . . . . . 7 ⊢ (∃𝑣 ∈ ℕ₀ [𝑎 / 𝑢]𝜓 ↔ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)
74	69, 73	bitrdi 290	. . . . . 6 ⊢ (𝑢 = 𝑎 → (∃𝑣 ∈ ℕ₀ 𝜓 ↔ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓))
75	60, 61, 62, 67, 74	cbvrabw 3450	. . . . 5 ⊢ {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} = {𝑎 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑏 ∈ ℕ₀ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓}
76		fveq1 6907	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → (𝑡‘𝑀) = (𝑏‘𝑀))
77		reseq1 5975	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (𝑡 ↾ (1...𝑁)) = (𝑏 ↾ (1...𝑁)))
78	77	sbceq1d 3747	. . . . . . . 8 ⊢ (𝑡 = 𝑏 → ([(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
79	76, 78	sbceqbid 3749	. . . . . . 7 ⊢ (𝑡 = 𝑏 → ([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓))
80	79	rexrab 3657	. . . . . 6 ⊢ (∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))
81	80	abbii 2830	. . . . 5 ⊢ {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ (ℕ₀ ↑_m (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))}
82	59, 75, 81	3eqtr4g 2823	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → {𝑢 ∈ (ℕ₀ ↑_m (1...𝑁)) ∣ ∃𝑣 ∈ ℕ₀ 𝜓} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))})
83		fvex 6921	. . . . . . . 8 ⊢ (𝑡‘𝑀) ∈ V
84		vex 3458	. . . . . . . . 9 ⊢ 𝑡 ∈ V
85	84	resex 6030	. . . . . . . 8 ⊢ (𝑡 ↾ (1...𝑁)) ∈ V
86		rexrabdioph.2	. . . . . . . . 9 ⊢ (𝑣 = (𝑡‘𝑀) → (𝜓 ↔ 𝜒))
87		rexrabdioph.3	. . . . . . . . 9 ⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝜒 ↔ 𝜑))
88	86, 87	sylan9bb 519	. . . . . . . 8 ⊢ ((𝑣 = (𝑡‘𝑀) ∧ 𝑢 = (𝑡 ↾ (1...𝑁))) → (𝜓 ↔ 𝜑))
89	83, 85, 88	sbc2ie 3818	. . . . . . 7 ⊢ ([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ 𝜑)
90	89	rabbii 3421	. . . . . 6 ⊢ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓} = {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}
91	90	rexeqi 3322	. . . . 5 ⊢ (∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁)))
92	91	abbii 2830	. . . 4 ⊢ {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))}
93	82, 92	eqtrdi 2814	. . 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 12744	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℤ)
97		uzid 13007	. . . . . 6 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ_≥‘𝑁))
98		peano2uz 13055	. . . . . 6 ⊢ (𝑁 ∈ (ℤ_≥‘𝑁) → (𝑁 + 1) ∈ (ℤ_≥‘𝑁))
99	96, 97, 98	3syl 19	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ (ℤ_≥‘𝑁))
100	10, 99	eqeltrid 2868	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → 𝑀 ∈ (ℤ_≥‘𝑁))
101	100	adantr 486	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → 𝑀 ∈ (ℤ_≥‘𝑁))
102		simpr 490	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀))
103		diophrex 43979	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑀 ∈ (ℤ_≥‘𝑁) ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁))
104	95, 101, 102, 103	syl3anc 1399	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ₀ ↑_m (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁))
105	94, 104	eqeltrd 2864	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 2147 {cab 2741 ∃wrex 3090 {crab 3416 [wsbc 3742 ∪ cun 4152 {csn 4588 ⟨cop 4838 ↾ cres 5657 ⟶wf 6554 ‘cfv 6558 (class class class)co 7443 ↑_m cmap 8875 1c1 11228 + caddc 11230 ℕcn 12362 ℕ₀cn0 12633 ℤcz 12720 ℤ_≥cuz 12992 ...cfz 13666 Diophcdioph 43959

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-inf2 9669 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-of 7717 df-om 7902 df-1st 8025 df-2nd 8026 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-oadd 8508 df-er 8745 df-map 8877 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-dju 10009 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-nn 12363 df-n0 12634 df-z 12721 df-uz 12993 df-fz 13667 df-hash 14502 df-mzpcl 43927 df-mzp 43928 df-dioph 43960

This theorem is used by: rexfrabdioph 43995 elnn0rabdioph 44003 dvdsrabdioph 44010

W3C validator