Theorem fdc 38066

Description: Finite version of dependent choice. Construct a function whose value depends on the previous function value, except at a final point at which no new value can be chosen. The final hypothesis ensures that the process will terminate. The proof does not use the Axiom of Choice. (Contributed by Jeff Madsen, 18-Jun-2010.)

Hypotheses

Ref	Expression
fdc.1	⊢ 𝐴 ∈ V
fdc.2	⊢ 𝑀 ∈ ℤ
fdc.3	⊢ 𝑍 = (ℤ≥‘𝑀)
fdc.4	⊢ 𝑁 = (𝑀 + 1)
fdc.5	⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓))
fdc.6	⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒))
fdc.7	⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏))
fdc.8	⊢ (𝜂 → 𝐶 ∈ 𝐴)
fdc.9	⊢ (𝜂 → 𝑅 Fr 𝐴)
fdc.10	⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑))
fdc.11	⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎)

Assertion

Ref	Expression
fdc	⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))

Distinct variable groups:   𝐶,𝑓,𝑛   𝐴,𝑎,𝑏,𝑓,𝑛   𝑀,𝑎,𝑏,𝑓,𝑘,𝑛   𝑍,𝑎,𝑏,𝑛   𝑁,𝑎,𝑏,𝑓,𝑘,𝑛   𝑅,𝑎,𝑏   𝜑,𝑓,𝑘   𝜓,𝑎   𝜒,𝑎,𝑏,𝑛   𝜃,𝑓,𝑛   𝜏,𝑎,𝑏   𝜂,𝑎,𝑏

Allowed substitution hints:   𝜑(𝑛,𝑎,𝑏)   𝜓(𝑓,𝑘,𝑛,𝑏)   𝜒(𝑓,𝑘)   𝜃(𝑘,𝑎,𝑏)   𝜏(𝑓,𝑘,𝑛)   𝜂(𝑓,𝑘,𝑛)   𝐴(𝑘)   𝐶(𝑘,𝑎,𝑏)   𝑅(𝑓,𝑘,𝑛)   𝑍(𝑓,𝑘)

Proof of Theorem fdc

Dummy variables 𝑐 𝑑 𝑔 𝑚 𝑥 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fdc.8	. 2 ⊢ (𝜂 → 𝐶 ∈ 𝐴)
2		fdc.2	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑀 ∈ ℤ
3		uzid 12803	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
4	2, 3	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ∈ (ℤ≥‘𝑀)
5		fdc.3	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑍 = (ℤ≥‘𝑀)
6	4, 5	eleqtrri 2835	. . . . . . . . . . . . . . . . 17 ⊢ 𝑀 ∈ 𝑍
7		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩}
8	2	elexi 3452	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑀 ∈ V
9		vex 3433	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑎 ∈ V
10	8, 9	fsn 7088	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ↔ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩})
11	7, 10	mpbir 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎}
12		snssi 4729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
13		fss 6684	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
14	11, 12, 13	sylancr 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ 𝐴 → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
15		fzsn 13520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
16	2, 15	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀...𝑀) = {𝑀}
17	16	feq2i 6660	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
18	14, 17	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ 𝐴 → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
19	18	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
20	8, 9	fvsn 7136	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎
21	20	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎)
22		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → 𝜃)
23		snex 5381	. . . . . . . . . . . . . . . . . . 19 ⊢ {⟨𝑀, 𝑎⟩} ∈ V
24		feq1 6646	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴))
25		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓‘𝑀) = ({⟨𝑀, 𝑎⟩}‘𝑀))
26	25	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓‘𝑀) = 𝑎 ↔ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎))
27	25, 20	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓‘𝑀) = 𝑎)
28		sbceq2a 3740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑀) = 𝑎 → ([(𝑓‘𝑀) / 𝑎]𝜃 ↔ 𝜃))
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ([(𝑓‘𝑀) / 𝑎]𝜃 ↔ 𝜃))
30	26, 29	anbi12d 633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ↔ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃)))
31	24, 30	anbi12d 633	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)) ↔ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃))))
32	23, 31	spcev 3548	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
33	19, 21, 22, 32	syl12anc 837	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
34		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
35	34	feq2d 6652	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...𝑀)⟶𝐴))
36		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓‘𝑛) ∈ V
37		fdc.7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏))
38	36, 37	sbcie 3770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ 𝜏)
39		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑀 → (𝑓‘𝑛) = (𝑓‘𝑀))
40	39	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑀 → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘𝑀) / 𝑎]𝜃))
41	38, 40	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝜏 ↔ [(𝑓‘𝑀) / 𝑎]𝜃))
42	41	anbi2d 631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
43		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀))
44		fdc.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑁 = (𝑀 + 1)
45	44	oveq1i 7377	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁...𝑀) = ((𝑀 + 1)...𝑀)
46	2	zrei 12530	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑀 ∈ ℝ
47	46	ltp1i 12060	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑀 < (𝑀 + 1)
48		peano2z 12568	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
49	2, 48	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑀 + 1) ∈ ℤ
50		fzn 13494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅))
51	49, 2, 50	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)
52	47, 51	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 + 1)...𝑀) = ∅
53	45, 52	eqtri 2759	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁...𝑀) = ∅
54	43, 53	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝑁...𝑛) = ∅)
55	54	raleqdv 3295	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒))
56	35, 42, 55	3anbi123d 1439	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒)))
57		ral0 4438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑘 ∈ ∅ 𝜒
58		df-3an 1089	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒))
59	57, 58	mpbiran2 711	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
60	56, 59	bitrdi 287	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))))
61	60	exbidv 1923	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))))
62	61	rspcev 3564	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
63	6, 33, 62	sylancr 588	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
64	63	adantll 715	. . . . . . . . . . . . . . 15 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜃) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
65	64	a1d 25	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
66		fdc.11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎)
67		breq1 5088	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = 𝑏 → (𝑑𝑅𝑎 ↔ 𝑏𝑅𝑎))
68	67	rspcev 3564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)
69	68	expcom 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
70	66, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
71		dfrex2 3064	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
72	70, 71	imbitrdi 251	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
73	72	con2d 134	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
74		eldif 3899	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
75	74	simplbi2 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))))
76		ssrab2 4020	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴
77		dfss4 4209	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
78	76, 77	mpbi 230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}
79	78	eleq2i 2828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
80		eqeq2 2748	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑏 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝑏))
81	80	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑏 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏)))
82	81	3anbi2d 1444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
83	82	exbidv 1923	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
84	83	rexbidv 3161	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑏 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
85	84	elrab3 3635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ 𝐴 → (𝑏 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
86	79, 85	bitrid 283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
87	75, 86	sylibd 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
88	87	ad2antll 730	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
89		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚))
90	89	feq2d 6652	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...𝑚)⟶𝐴))
91		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
92	91	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘𝑚) / 𝑎]𝜃))
93	38, 92	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝜏 ↔ [(𝑓‘𝑚) / 𝑎]𝜃))
94	93	anbi2d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃)))
95		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚))
96	95	raleqdv 3295	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
97	90, 94, 96	3anbi123d 1439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
98	97	exbidv 1923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
99	98	cbvrexvw 3216	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
100		feq1 6646	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴 ↔ 𝑔:(𝑀...𝑚)⟶𝐴))
101		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑀) = (𝑔‘𝑀))
102	101	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑀) = 𝑏 ↔ (𝑔‘𝑀) = 𝑏))
103		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑚) = (𝑔‘𝑚))
104	103	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑚) / 𝑎]𝜃 ↔ [(𝑔‘𝑚) / 𝑎]𝜃))
105	102, 104	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ↔ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)))
106		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘(𝑘 − 1)) ∈ V
107		fdc.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓))
108	107	sbcbidv 3784	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑓‘𝑘) / 𝑏]𝜓))
109	106, 108	sbcie 3770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑓‘𝑘) / 𝑏]𝜓)
110		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘𝑘) ∈ V
111		fdc.6	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒))
112	110, 111	sbcie 3770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([(𝑓‘𝑘) / 𝑏]𝜓 ↔ 𝜒)
113	109, 112	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ 𝜒)
114		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1)))
115		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑘) = (𝑔‘𝑘))
116	115	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘𝑘) / 𝑏]𝜑))
117	114, 116	sbceqbid 3735	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
118	113, 117	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → (𝜒 ↔ [(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
119	118	ralbidv 3160	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
120	100, 105, 119	3anbi123d 1439	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)))
121	120	cbvexvw 2039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
122	121	rexbii 3084	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑚 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
123	99, 122	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
124	5	peano2uzs 12852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ 𝑍)
125	124	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍)
126		sbceq2a 3740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑 ↔ 𝜑))
127	126	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ↔ (𝜑 ∧ 𝑎 ∈ 𝐴)))
128	127	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ↔ ((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍)))
129		eqeq2 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑑 = 𝑏 → ((𝑔‘𝑀) = 𝑑 ↔ (𝑔‘𝑀) = 𝑏))
130	129	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 = 𝑏 → (((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ↔ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)))
131	130	3anbi2d 1444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 = 𝑏 → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)))
132	131	imbi1d 341	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 = 𝑏 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
133	128, 132	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = 𝑏 → (((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
134		sbceq2a 3740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑))
135		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑎 → (𝑐 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
136	134, 135	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ↔ ([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴)))
137	136	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ↔ (([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍)))
138		eqeq2 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑎 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝑎))
139	138	anbi1d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑎 → (((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
140	139	3anbi2d 1444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑎 → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
141	140	exbidv 1923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
142	141	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = 𝑎 → (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) ↔ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))))
143	137, 142	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 = 𝑎 → (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))) ↔ ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))))
144		peano2uz 12851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (ℤ≥‘𝑀))
145	144, 5	eleq2s 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘𝑀))
146		elfzp12 13557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
147	145, 146	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
148	147	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
149		iftrue 4472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐)
150	149	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ 𝑐 ∈ 𝐴))
151	150	biimprcd 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑐 ∈ 𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
152	151	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
153		1re 11144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 1 ∈ ℝ
154	46, 153	readdcli 11160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑀 + 1) ∈ ℝ
155	46, 154	ltnlei 11267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)
156	47, 155	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ¬ (𝑀 + 1) ≤ 𝑀
157		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1))))
158		elfzle1 13481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀)
159	157, 158	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀))
160	159	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 = 𝑀 → (𝑀 + 1) ≤ 𝑀))
161	156, 160	mtoi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → ¬ 𝑥 = 𝑀)
162	161	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → ¬ 𝑥 = 𝑀)
163	162	iffalsed 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1)))
164		elfzelz 13478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ)
165	164	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ)
166		eluzelz 12798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑚 ∈ ℤ)
167	166, 5	eleq2s 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ)
168	167	peano2zd 12636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ ℤ)
169		1z 12557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 1 ∈ ℤ
170		fzsubel 13514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
171	170	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
172	169, 171	mpanr2 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
173	49, 172	mpanl1 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 + 1) ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
174	173	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 + 1) ∈ ℤ → (𝑥 ∈ ℤ → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))))
175	168, 174	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑚 ∈ 𝑍 → (𝑥 ∈ ℤ → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))))
176	175	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))))
177	176	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
178	165, 177	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))
179	46	recni 11159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑀 ∈ ℂ
180		ax-1cn 11096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 1 ∈ ℂ
181	179, 180	pncan3oi 11409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑀 + 1) − 1) = 𝑀
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑀 + 1) − 1) = 𝑀)
183	167	zcnd 12634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℂ)
184		pncan 11399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
185	183, 180, 184	sylancl 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑚 + 1) − 1) = 𝑚)
186	182, 185	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑚 ∈ 𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
187	186	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
188	178, 187	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚))
189		ffvelcdm 7033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
190	188, 189	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
191	190	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
192	191	ancom1s 654	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
193	163, 192	eqeltrd 2836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
194	193	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
195	194	adantll 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
196	152, 195	jaod 860	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
197	148, 196	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
198	197	ralrimiv 3128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
199		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))
200	199	fmpt 7062	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
201	198, 200	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
202	201	adantlll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
203	202	3ad2antr1 1190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
204		eluzfz1 13485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
205	144, 204	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
206	205, 5	eleq2s 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ (𝑀...(𝑚 + 1)))
207		vex 3433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑐 ∈ V
208	149, 199, 207	fvmpt 6947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
209	206, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
210	209	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
211		eluzfz2 13486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
212	144, 211	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
213	212, 5	eleq2s 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
214		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀))
215		fvoveq1 7390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1)))
216	214, 215	ifbieq2d 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
217		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑔‘((𝑚 + 1) − 1)) ∈ V
218	207, 217	ifex 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V
219	216, 199, 218	fvmpt 6947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ ((𝑚 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
220	213, 219	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
221		eluzle 12801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑚)
222	221, 5	eleq2s 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ≤ 𝑚)
223		zleltp1 12578	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ≤ 𝑚 ↔ 𝑀 < (𝑚 + 1)))
224	2, 167, 223	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑚 ∈ 𝑍 → (𝑀 ≤ 𝑚 ↔ 𝑀 < (𝑚 + 1)))
225	222, 224	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑚 ∈ 𝑍 → 𝑀 < (𝑚 + 1))
226		ltne 11243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀)
227	46, 225, 226	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ≠ 𝑀)
228	227	neneqd 2937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → ¬ (𝑚 + 1) = 𝑀)
229	228	iffalsed 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ 𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1)))
230	185	fveq2d 6844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ 𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔‘𝑚))
231	220, 229, 230	3eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔‘𝑚))
232	231	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 ∈ 𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃 ↔ [(𝑔‘𝑚) / 𝑎]𝜃))
233	232	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ 𝑍 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
234	233	ad2ant2l 747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
235	234	3ad2antr2 1191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
236		eluzp1p1 12816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
237	236, 5	eleq2s 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
238	44	fveq2i 6843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (ℤ≥‘𝑁) = (ℤ≥‘(𝑀 + 1))
239	237, 238	eleqtrrdi 2847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘𝑁))
240		elfzp12 13557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑁) → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑚 ∈ 𝑍 → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
242	241	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
243	242	adantll 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
244	243	adantlr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
245		oveq1 7374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1))
246	44	oveq1i 7377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 − 1) = ((𝑀 + 1) − 1)
247	246, 181	eqtri 2759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑁 − 1) = 𝑀
248	245, 247	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀)
249	248	fveq2d 6844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
250	249	ad2antll 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
251	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
252	250, 251	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = 𝑐)
253	44	eqeq2i 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 = 𝑁 ↔ 𝑗 = (𝑀 + 1))
254		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 = (𝑀 + 1) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
255	253, 254	sylbi 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
256	255	ad2antll 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
257	46, 154, 47	ltleii 11269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑀 ≤ (𝑀 + 1)
258		eluz2 12794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)))
259	2, 49, 257, 258	mpbir3an 1343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 + 1) ∈ (ℤ≥‘𝑀)
260		fzss1 13517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
261	259, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
262		eluzfz1 13485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑚))
263	262, 5	eleq2s 2854	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ (𝑀...𝑚))
264		fzaddel 13512	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
265	2, 169, 264	mpanr12 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
266	2, 167, 265	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ 𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
267	263, 266	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑚 ∈ 𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))
268	261, 267	sselid 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑚 ∈ 𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1)))
269		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀))
270		oveq1 7374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1))
271	270, 181	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀)
272	271	fveq2d 6844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘𝑀))
273	269, 272	ifbieq2d 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)))
274		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑔‘𝑀) ∈ V
275	207, 274	ifex 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) ∈ V
276	273, 199, 275	fvmpt 6947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑀 + 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)))
277	268, 276	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)))
278	46, 47	gtneii 11258	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑀 + 1) ≠ 𝑀
279		ifnefalse 4478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑀 + 1) ≠ 𝑀 → if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) = (𝑔‘𝑀))
280	278, 279	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) = (𝑔‘𝑀)
281	277, 280	eqtrdi 2787	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔‘𝑀))
282	281	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔‘𝑀))
283		simprl 771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → (𝑔‘𝑀) = 𝑑)
284	256, 282, 283	3eqtrd 2775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑)
285	284	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑))
286	252, 285	sbceqbid 3735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
287	286	biimparc 479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ (𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
288	287	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
289	288	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ (𝑔‘𝑀) = 𝑑) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
290	289	adantlrr 722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
291		elfzelz 13478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ)
292	291	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ)
293	44, 49	eqeltri 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ 𝑁 ∈ ℤ
294		peano2z 12568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
295	293, 294	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 + 1) ∈ ℤ
296		fzsubel 13514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
297	296	biimpd 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
298	169, 297	mpanr2 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
299	298	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
300	295, 168, 299	sylancr 588	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑚 ∈ 𝑍 → (𝑗 ∈ ℤ → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
301	300	com23 86	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))))
302	301	imp 406	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
303	292, 302	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))
304	293	zrei 12530	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ 𝑁 ∈ ℝ
305	304	recni 11159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑁 ∈ ℂ
306	305, 180	pncan3oi 11409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑁 + 1) − 1) = 𝑁
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑁 + 1) − 1) = 𝑁)
308	307, 185	oveq12d 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑚 ∈ 𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
309	308	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
310	303, 309	eleqtrd 2838	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚))
311		fvoveq1 7390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
312		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑘 = (𝑗 − 1) → (𝑔‘𝑘) = (𝑔‘(𝑗 − 1)))
313	312	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = (𝑗 − 1) → ([(𝑔‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
314	311, 313	sbceqbid 3735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
315	314	rspcva 3562	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
316	310, 315	sylan 581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
317	44, 259	eqeltri 2832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑁 ∈ (ℤ≥‘𝑀)
318		fzss1 13517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
319	317, 318	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
320		fzssp1 13521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1))
321	320, 310	sselid 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1)))
322	319, 321	sselid 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1)))
323		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀))
324		fvoveq1 7390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
325	323, 324	ifbieq2d 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
326		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑔‘((𝑗 − 1) − 1)) ∈ V
327	207, 326	ifex 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈ V
328	325, 199, 327	fvmpt 6947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑗 − 1) ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
329	322, 328	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
330	154	ltp1i 12060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 + 1) < ((𝑀 + 1) + 1)
331	44	oveq1i 7377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑁 + 1) = ((𝑀 + 1) + 1)
332	330, 331	breqtrri 5112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑀 + 1) < (𝑁 + 1)
333	304, 153	readdcli 11160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑁 + 1) ∈ ℝ
334	154, 333	ltnlei 11267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1))
335	332, 334	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ¬ (𝑁 + 1) ≤ (𝑀 + 1)
336	291	zcnd 12634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ)
337		subadd 11396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
338	180, 179, 337	mp3an23 1456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
339	336, 338	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
340		eqcom 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((1 + 𝑀) = 𝑗 ↔ 𝑗 = (1 + 𝑀))
341	180, 179	addcomi 11337	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (1 + 𝑀) = (𝑀 + 1)
342	341	eqeq2i 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1))
343	340, 342	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((1 + 𝑀) = 𝑗 ↔ 𝑗 = (𝑀 + 1))
344		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1))))
345		elfzle1 13481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1))
346	344, 345	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1)))
347	346	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = (𝑀 + 1) → (𝑁 + 1) ≤ (𝑀 + 1)))
348	343, 347	biimtrid 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((1 + 𝑀) = 𝑗 → (𝑁 + 1) ≤ (𝑀 + 1)))
349	339, 348	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 → (𝑁 + 1) ≤ (𝑀 + 1)))
350	335, 349	mtoi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ (𝑗 − 1) = 𝑀)
351	350	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ (𝑗 − 1) = 𝑀)
352	351	iffalsed 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1)))
353	329, 352	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
354		peano2uz 12851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
355		fzss1 13517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
356	317, 354, 355	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
357		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))
358	356, 357	sselid 3919	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1)))
359		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = 𝑗 → (𝑥 = 𝑀 ↔ 𝑗 = 𝑀))
360		fvoveq1 7390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1)))
361	359, 360	ifbieq2d 4493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
362		fvex 6853	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑔‘(𝑗 − 1)) ∈ V
363	207, 362	ifex 4517	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V
364	361, 199, 363	fvmpt 6947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
365	358, 364	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
366	47, 44	breqtrri 5112	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑀 < 𝑁
367	304	ltp1i 12060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑁 < (𝑁 + 1)
368	46, 304, 333	lttri 11272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1))
369	366, 367, 368	mp2an 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ 𝑀 < (𝑁 + 1)
370	46, 333	ltnlei 11267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀)
371	369, 370	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ¬ (𝑁 + 1) ≤ 𝑀
372		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1))))
373		elfzle1 13481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀)
374	372, 373	biimtrdi 253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀))
375	374	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = 𝑀 → (𝑁 + 1) ≤ 𝑀))
376	371, 375	mtoi 199	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ 𝑗 = 𝑀)
377	376	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ 𝑗 = 𝑀)
378	377	iffalsed 4477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1)))
379	365, 378	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1)))
380	379	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
381	353, 380	sbceqbid 3735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
382	381	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
383	316, 382	syldan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
384	383	an32s 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
385	384	adantlrl 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
386	385	adantlll 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
387	290, 386	jaodan 960	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
388	244, 387	syldan 592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
389	388	ralrimiva 3129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
390		fvoveq1 7390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
391		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
392	391	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
393	390, 392	sbceqbid 3735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
394	393	cbvralvw 3215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
395	389, 394	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
396	395	adantllr 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
397	396	adantrlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
398	397	3adantr1 1171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
399		ovex 7400	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀...(𝑚 + 1)) ∈ V
400	399	mptex 7178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V
401		feq1 6646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴))
402		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
403	402	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓‘𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐))
404		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)))
405	404	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑚 + 1)) / 𝑎]𝜃 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃))
406	403, 405	anbi12d 633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐 ∧ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)))
407		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
408		fveq1 6839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
409	408	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
410	407, 409	sbceqbid 3735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
411	113, 410	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝜒 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
412	411	ralbidv 3160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
413	401, 406, 412	3anbi123d 1439	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴 ∧ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐 ∧ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)))
414	400, 413	spcev 3548	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴 ∧ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐 ∧ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
415	203, 210, 235, 398, 414	syl121anc 1378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
416	415	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
417	143, 416	chvarvv 1991	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
418	133, 417	chvarvv 1991	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
419	418	adantlrr 722	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
420	419	adantlll 719	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
421	420	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
422		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1)))
423	422	feq2d 6652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...(𝑚 + 1))⟶𝐴))
424		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = (𝑚 + 1) → (𝑓‘𝑛) = (𝑓‘(𝑚 + 1)))
425	424	sbceq1d 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = (𝑚 + 1) → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
426	38, 425	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝜏 ↔ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
427	426	anbi2d 631	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
428		oveq2 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1)))
429	428	raleqdv 3295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
430	423, 427, 429	3anbi123d 1439	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
431	430	exbidv 1923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
432	431	rspcev 3564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
433	125, 421, 432	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
434	433	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
435	434	exlimdv 1935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
436	435	rexlimdva 3138	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
437	123, 436	biimtrid 242	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
438	73, 88, 437	3syld 60	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
439	438	an42s 662	. . . . . . . . . . . . . . . 16 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
440	439	rexlimdvaa 3139	. . . . . . . . . . . . . . 15 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))))
441	440	imp 406	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ ∃𝑏 ∈ 𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
442		fdc.10	. . . . . . . . . . . . . 14 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑))
443	65, 441, 442	mpjaodan 961	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
444	138	anbi1d 632	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏)))
445	444	3anbi2d 1444	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
446	445	exbidv 1923	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
447	446	rexbidv 3161	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑎 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
448	447	elrab3 3635	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝐴 → (𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
449	448	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
450	443, 449	sylibrd 259	. . . . . . . . . . . 12 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
451	450	ex 412	. . . . . . . . . . 11 ⊢ (𝜂 → (𝑎 ∈ 𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
452	451	com23 86	. . . . . . . . . 10 ⊢ (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
453		eldif 3899	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
454	453	notbii 320	. . . . . . . . . . 11 ⊢ (¬ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
455		iman 401	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
456	454, 455	bitr4i 278	. . . . . . . . . 10 ⊢ (¬ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
457	452, 456	imbitrrdi 252	. . . . . . . . 9 ⊢ (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
458	457	con2d 134	. . . . . . . 8 ⊢ (𝜂 → (𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
459	458	imp 406	. . . . . . 7 ⊢ ((𝜂 ∧ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
460	459	nrexdv 3132	. . . . . 6 ⊢ (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
461		df-ne 2933	. . . . . . 7 ⊢ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
462		fdc.9	. . . . . . . 8 ⊢ (𝜂 → 𝑅 Fr 𝐴)
463		difss 4076	. . . . . . . 8 ⊢ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴
464		fdc.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ V
465		difexg 5270	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V)
466	464, 465	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V
467		fri 5589	. . . . . . . . . 10 ⊢ ((((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
468	466, 467	mpanl1 701	. . . . . . . . 9 ⊢ ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
469	468	expr 456	. . . . . . . 8 ⊢ ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
470	462, 463, 469	sylancl 587	. . . . . . 7 ⊢ (𝜂 → ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
471	461, 470	biimtrrid 243	. . . . . 6 ⊢ (𝜂 → (¬ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
472	460, 471	mt3d 148	. . . . 5 ⊢ (𝜂 → (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
473		ssdif0 4306	. . . . 5 ⊢ (𝐴 ⊆ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
474	472, 473	sylibr 234	. . . 4 ⊢ (𝜂 → 𝐴 ⊆ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
475	76	a1i 11	. . . 4 ⊢ (𝜂 → {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴)
476	474, 475	eqssd 3939	. . 3 ⊢ (𝜂 → 𝐴 = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
477		rabid2 3422	. . 3 ⊢ (𝐴 = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
478	476, 477	sylib 218	. 2 ⊢ (𝜂 → ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
479		eqeq2 2748	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝐶))
480	479	anbi1d 632	. . . . . 6 ⊢ (𝑐 = 𝐶 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏)))
481	480	3anbi2d 1444	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
482	481	exbidv 1923	. . . 4 ⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
483	482	rexbidv 3161	. . 3 ⊢ (𝑐 = 𝐶 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
484	483	rspcva 3562	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
485	1, 478, 484	syl2anc 585	1 ⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2932  ∀wral 3051  ∃wrex 3061  {crab 3389  Vcvv 3429  [wsbc 3728   ∖ cdif 3886   ⊆ wss 3889  ∅c0 4273  ifcif 4466  {csn 4567  ⟨cop 4573   class class class wbr 5085   ↦ cmpt 5166   Fr wfr 5581  ⟶wf 6494  ‘cfv 6498  (class class class)co 7367  ℂcc 11036  ℝcr 11037  1c1 11039   + caddc 11041   < clt 11179   ≤ cle 11180   − cmin 11377  ℤcz 12524  ℤ_≥cuz 12788  ...cfz 13461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-1st 7942  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525  df-uz 12789  df-fz 13462

This theorem is referenced by:  fdc1  38067