Theorem fdc 37805

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 12753	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
4	2, 3	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ∈ (ℤ≥‘𝑀)
5		fdc.3	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑍 = (ℤ≥‘𝑀)
6	4, 5	eleqtrri 2832	. . . . . . . . . . . . . . . . 17 ⊢ 𝑀 ∈ 𝑍
7		eqid 2733	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩}
8	2	elexi 3460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑀 ∈ V
9		vex 3441	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑎 ∈ V
10	8, 9	fsn 7074	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ↔ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩})
11	7, 10	mpbir 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎}
12		snssi 4759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
13		fss 6672	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
14	11, 12, 13	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ 𝐴 → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
15		fzsn 13468	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
16	2, 15	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀...𝑀) = {𝑀}
17	16	feq2i 6648	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
18	14, 17	sylibr 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ 𝐴 → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
19	18	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
20	8, 9	fvsn 7121	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎
21	20	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎)
22		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → 𝜃)
23		snex 5376	. . . . . . . . . . . . . . . . . . 19 ⊢ {⟨𝑀, 𝑎⟩} ∈ V
24		feq1 6634	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴))
25		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓‘𝑀) = ({⟨𝑀, 𝑎⟩}‘𝑀))
26	25	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓‘𝑀) = 𝑎 ↔ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎))
27	25, 20	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓‘𝑀) = 𝑎)
28		sbceq2a 3749	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑀) = 𝑎 → ([(𝑓‘𝑀) / 𝑎]𝜃 ↔ 𝜃))
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ([(𝑓‘𝑀) / 𝑎]𝜃 ↔ 𝜃))
30	26, 29	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ↔ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃)))
31	24, 30	anbi12d 632	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)) ↔ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃))))
32	23, 31	spcev 3557	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
33	19, 21, 22, 32	syl12anc 836	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
34		oveq2 7360	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
35	34	feq2d 6640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...𝑀)⟶𝐴))
36		fvex 6841	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓‘𝑛) ∈ V
37		fdc.7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏))
38	36, 37	sbcie 3779	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ 𝜏)
39		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑀 → (𝑓‘𝑛) = (𝑓‘𝑀))
40	39	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑀 → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘𝑀) / 𝑎]𝜃))
41	38, 40	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝜏 ↔ [(𝑓‘𝑀) / 𝑎]𝜃))
42	41	anbi2d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
43		oveq2 7360	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀))
44		fdc.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑁 = (𝑀 + 1)
45	44	oveq1i 7362	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁...𝑀) = ((𝑀 + 1)...𝑀)
46	2	zrei 12481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑀 ∈ ℝ
47	46	ltp1i 12033	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑀 < (𝑀 + 1)
48		peano2z 12519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
49	2, 48	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑀 + 1) ∈ ℤ
50		fzn 13442	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅))
51	49, 2, 50	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)
52	47, 51	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 + 1)...𝑀) = ∅
53	45, 52	eqtri 2756	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁...𝑀) = ∅
54	43, 53	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝑁...𝑛) = ∅)
55	54	raleqdv 3293	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒))
56	35, 42, 55	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒)))
57		ral0 4462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑘 ∈ ∅ 𝜒
58		df-3an 1088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒))
59	57, 58	mpbiran2 710	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
60	56, 59	bitrdi 287	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))))
61	60	exbidv 1922	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))))
62	61	rspcev 3573	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
63	6, 33, 62	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
64	63	adantll 714	. . . . . . . . . . . . . . 15 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜃) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
65	64	a1d 25	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
66		fdc.11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎)
67		breq1 5096	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = 𝑏 → (𝑑𝑅𝑎 ↔ 𝑏𝑅𝑎))
68	67	rspcev 3573	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)
69	68	expcom 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
70	66, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
71		dfrex2 3060	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
72	70, 71	imbitrdi 251	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
73	72	con2d 134	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
74		eldif 3908	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
75	74	simplbi2 500	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))))
76		ssrab2 4029	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴
77		dfss4 4218	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
78	76, 77	mpbi 230	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}
79	78	eleq2i 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
80		eqeq2 2745	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑏 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝑏))
81	80	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑏 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏)))
82	81	3anbi2d 1443	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
83	82	exbidv 1922	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
84	83	rexbidv 3157	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑏 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
85	84	elrab3 3644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ 𝐴 → (𝑏 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
86	79, 85	bitrid 283	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
87	75, 86	sylibd 239	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
88	87	ad2antll 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
89		oveq2 7360	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚))
90	89	feq2d 6640	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...𝑚)⟶𝐴))
91		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
92	91	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘𝑚) / 𝑎]𝜃))
93	38, 92	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝜏 ↔ [(𝑓‘𝑚) / 𝑎]𝜃))
94	93	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃)))
95		oveq2 7360	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚))
96	95	raleqdv 3293	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
97	90, 94, 96	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
98	97	exbidv 1922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
99	98	cbvrexvw 3212	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
100		feq1 6634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴 ↔ 𝑔:(𝑀...𝑚)⟶𝐴))
101		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑀) = (𝑔‘𝑀))
102	101	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑀) = 𝑏 ↔ (𝑔‘𝑀) = 𝑏))
103		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑚) = (𝑔‘𝑚))
104	103	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑚) / 𝑎]𝜃 ↔ [(𝑔‘𝑚) / 𝑎]𝜃))
105	102, 104	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ↔ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)))
106		fvex 6841	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘(𝑘 − 1)) ∈ V
107		fdc.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓))
108	107	sbcbidv 3793	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑓‘𝑘) / 𝑏]𝜓))
109	106, 108	sbcie 3779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑓‘𝑘) / 𝑏]𝜓)
110		fvex 6841	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘𝑘) ∈ V
111		fdc.6	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒))
112	110, 111	sbcie 3779	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([(𝑓‘𝑘) / 𝑏]𝜓 ↔ 𝜒)
113	109, 112	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ 𝜒)
114		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1)))
115		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑘) = (𝑔‘𝑘))
116	115	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘𝑘) / 𝑏]𝜑))
117	114, 116	sbceqbid 3744	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
118	113, 117	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → (𝜒 ↔ [(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
119	118	ralbidv 3156	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
120	100, 105, 119	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)))
121	120	cbvexvw 2038	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
122	121	rexbii 3080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑚 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
123	99, 122	bitri 275	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
124	5	peano2uzs 12802	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ 𝑍)
125	124	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍)
126		sbceq2a 3749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑 ↔ 𝜑))
127	126	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ↔ (𝜑 ∧ 𝑎 ∈ 𝐴)))
128	127	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ↔ ((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍)))
129		eqeq2 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑑 = 𝑏 → ((𝑔‘𝑀) = 𝑑 ↔ (𝑔‘𝑀) = 𝑏))
130	129	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 = 𝑏 → (((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ↔ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)))
131	130	3anbi2d 1443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑))
135		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑎 → (𝑐 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
136	134, 135	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ↔ ([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴)))
137	136	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ↔ (([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍)))
138		eqeq2 2745	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑎 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝑎))
139	138	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑎 → (((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
140	139	3anbi2d 1443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑎 → ((𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
141	140	exbidv 1922	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (ℤ≥‘𝑀))
145	144, 5	eleq2s 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘𝑀))
146		elfzp12 13505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
147	145, 146	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
148	147	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
149		iftrue 4480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐)
150	149	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ 𝑐 ∈ 𝐴))
151	150	biimprcd 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑐 ∈ 𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
152	151	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
153		1re 11119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 1 ∈ ℝ
154	46, 153	readdcli 11134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑀 + 1) ∈ ℝ
155	46, 154	ltnlei 11241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)
156	47, 155	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ¬ (𝑀 + 1) ≤ 𝑀
157		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1))))
158		elfzle1 13429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1)))
164		elfzelz 13426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ)
165	164	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ)
166		eluzelz 12748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑚 ∈ ℤ)
167	166, 5	eleq2s 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ)
168	167	peano2zd 12586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ ℤ)
169		1z 12508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 1 ∈ ℤ
170		fzsubel 13462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
173	49, 172	mpanl1 700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑀 ∈ ℂ
180		ax-1cn 11071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 1 ∈ ℂ
181	179, 180	pncan3oi 11383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑀 + 1) − 1) = 𝑀
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑀 + 1) − 1) = 𝑀)
183	167	zcnd 12584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℂ)
184		pncan 11373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
185	183, 180, 184	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑚 + 1) − 1) = 𝑚)
186	182, 185	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑚 ∈ 𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
187	186	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
188	178, 187	eleqtrd 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚))
189		ffvelcdm 7020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
190	188, 189	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
191	190	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
192	191	ancom1s 653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
193	163, 192	eqeltrd 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
194	193	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
195	194	adantll 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
196	152, 195	jaod 859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
197	148, 196	sylbid 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
198	197	ralrimiv 3124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
199		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))
200	199	fmpt 7049	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
201	198, 200	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
202	201	adantlll 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
203	202	3ad2antr1 1189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
204		eluzfz1 13433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
205	144, 204	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
206	205, 5	eleq2s 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ (𝑀...(𝑚 + 1)))
207		vex 3441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑐 ∈ V
208	149, 199, 207	fvmpt 6935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
209	206, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
210	209	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
211		eluzfz2 13434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
212	144, 211	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
213	212, 5	eleq2s 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
214		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀))
215		fvoveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1)))
216	214, 215	ifbieq2d 4501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
217		fvex 6841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑔‘((𝑚 + 1) − 1)) ∈ V
218	207, 217	ifex 4525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V
219	216, 199, 218	fvmpt 6935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑚)
222	221, 5	eleq2s 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ≤ 𝑚)
223		zleltp1 12529	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ≤ 𝑚 ↔ 𝑀 < (𝑚 + 1)))
224	2, 167, 223	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑚 ∈ 𝑍 → (𝑀 ≤ 𝑚 ↔ 𝑀 < (𝑚 + 1)))
225	222, 224	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑚 ∈ 𝑍 → 𝑀 < (𝑚 + 1))
226		ltne 11217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀)
227	46, 225, 226	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ≠ 𝑀)
228	227	neneqd 2934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → ¬ (𝑚 + 1) = 𝑀)
229	228	iffalsed 4485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ 𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1)))
230	185	fveq2d 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ 𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔‘𝑚))
231	220, 229, 230	3eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔‘𝑚))
232	231	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 ∈ 𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃 ↔ [(𝑔‘𝑚) / 𝑎]𝜃))
233	232	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ 𝑍 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
234	233	ad2ant2l 746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
235	234	3ad2antr2 1190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
236		eluzp1p1 12766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
237	236, 5	eleq2s 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
238	44	fveq2i 6831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (ℤ≥‘𝑁) = (ℤ≥‘(𝑀 + 1))
239	237, 238	eleqtrrdi 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘𝑁))
240		elfzp12 13505	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
244	243	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
245		oveq1 7359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1))
246	44	oveq1i 7362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 − 1) = ((𝑀 + 1) − 1)
247	246, 181	eqtri 2756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑁 − 1) = 𝑀
248	245, 247	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀)
249	248	fveq2d 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
250	249	ad2antll 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
251	209	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
252	250, 251	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = 𝑐)
253	44	eqeq2i 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 = 𝑁 ↔ 𝑗 = (𝑀 + 1))
254		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
257	46, 154, 47	ltleii 11243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑀 ≤ (𝑀 + 1)
258		eluz2 12744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)))
259	2, 49, 257, 258	mpbir3an 1342	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 + 1) ∈ (ℤ≥‘𝑀)
260		fzss1 13465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
261	259, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
262		eluzfz1 13433	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑚))
263	262, 5	eleq2s 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ (𝑀...𝑚))
264		fzaddel 13460	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
265	2, 169, 264	mpanr12 705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
266	2, 167, 265	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ 𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
267	263, 266	mpbid 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑚 ∈ 𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))
268	261, 267	sselid 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑚 ∈ 𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1)))
269		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀))
270		oveq1 7359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1))
271	270, 181	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀)
272	271	fveq2d 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘𝑀))
273	269, 272	ifbieq2d 4501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)))
274		fvex 6841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑔‘𝑀) ∈ V
275	207, 274	ifex 4525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) ∈ V
276	273, 199, 275	fvmpt 6935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑀 + 1) ≠ 𝑀
279		ifnefalse 4486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑀 + 1) ≠ 𝑀 → if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) = (𝑔‘𝑀))
280	278, 279	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) = (𝑔‘𝑀)
281	277, 280	eqtrdi 2784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔‘𝑀))
282	281	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔‘𝑀))
283		simprl 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → (𝑔‘𝑀) = 𝑑)
284	256, 282, 283	3eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑)
285	284	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑))
286	252, 285	sbceqbid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
291		elfzelz 13426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ)
292	291	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ)
293	44, 49	eqeltri 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ 𝑁 ∈ ℤ
294		peano2z 12519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
295	293, 294	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 + 1) ∈ ℤ
296		fzsubel 13462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ 𝑁 ∈ ℝ
305	304	recni 11133	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑁 ∈ ℂ
306	305, 180	pncan3oi 11383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑁 + 1) − 1) = 𝑁
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑁 + 1) − 1) = 𝑁)
308	307, 185	oveq12d 7370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑚 ∈ 𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
309	308	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
310	303, 309	eleqtrd 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚))
311		fvoveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
312		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑘 = (𝑗 − 1) → (𝑔‘𝑘) = (𝑔‘(𝑗 − 1)))
313	312	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = (𝑗 − 1) → ([(𝑔‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
314	311, 313	sbceqbid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
315	314	rspcva 3571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
316	310, 315	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
317	44, 259	eqeltri 2829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑁 ∈ (ℤ≥‘𝑀)
318		fzss1 13465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
319	317, 318	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
320		fzssp1 13469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1))
321	320, 310	sselid 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1)))
322	319, 321	sselid 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1)))
323		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀))
324		fvoveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
325	323, 324	ifbieq2d 4501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
326		fvex 6841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑔‘((𝑗 − 1) − 1)) ∈ V
327	207, 326	ifex 4525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈ V
328	325, 199, 327	fvmpt 6935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 + 1) < ((𝑀 + 1) + 1)
331	44	oveq1i 7362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑁 + 1) = ((𝑀 + 1) + 1)
332	330, 331	breqtrri 5120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑀 + 1) < (𝑁 + 1)
333	304, 153	readdcli 11134	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑁 + 1) ∈ ℝ
334	154, 333	ltnlei 11241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1))
335	332, 334	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ¬ (𝑁 + 1) ≤ (𝑀 + 1)
336	291	zcnd 12584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ)
337		subadd 11370	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
338	180, 179, 337	mp3an23 1455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
339	336, 338	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
340		eqcom 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((1 + 𝑀) = 𝑗 ↔ 𝑗 = (1 + 𝑀))
341	180, 179	addcomi 11311	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (1 + 𝑀) = (𝑀 + 1)
342	341	eqeq2i 2746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1))
343	340, 342	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((1 + 𝑀) = 𝑗 ↔ 𝑗 = (𝑀 + 1))
344		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1))))
345		elfzle1 13429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1)))
353	329, 352	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
354		peano2uz 12801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
355		fzss1 13465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1)))
359		eqeq1 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = 𝑗 → (𝑥 = 𝑀 ↔ 𝑗 = 𝑀))
360		fvoveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1)))
361	359, 360	ifbieq2d 4501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
362		fvex 6841	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑔‘(𝑗 − 1)) ∈ V
363	207, 362	ifex 4525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V
364	361, 199, 363	fvmpt 6935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
365	358, 364	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
366	47, 44	breqtrri 5120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑀 < 𝑁
367	304	ltp1i 12033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑁 < (𝑁 + 1)
368	46, 304, 333	lttri 11246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1))
369	366, 367, 368	mp2an 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ 𝑀 < (𝑁 + 1)
370	46, 333	ltnlei 11241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀)
371	369, 370	mpbi 230	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ¬ (𝑁 + 1) ≤ 𝑀
372		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1))))
373		elfzle1 13429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1)))
379	365, 378	eqtrd 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1)))
380	379	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
381	353, 380	sbceqbid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
384	383	an32s 652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
385	384	adantlrl 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
386	385	adantlll 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
387	290, 386	jaodan 959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
388	244, 387	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
389	388	ralrimiva 3125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
390		fvoveq1 7375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
391		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
392	391	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
393	390, 392	sbceqbid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
394	393	cbvralvw 3211	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 719	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
397	396	adantrlr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
398	397	3adantr1 1170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
399		ovex 7385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀...(𝑚 + 1)) ∈ V
400	399	mptex 7163	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V
401		feq1 6634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴))
402		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
403	402	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓‘𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐))
404		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)))
405	404	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑚 + 1)) / 𝑎]𝜃 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃))
406	403, 405	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐 ∧ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)))
407		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
408		fveq1 6827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
409	408	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
410	407, 409	sbceqbid 3744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3156	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
413	401, 406, 412	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
416	415	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
417	143, 416	chvarvv 1990	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
418	133, 417	chvarvv 1990	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
419	418	adantlrr 721	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
420	419	adantlll 718	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
421	420	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
422		oveq2 7360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1)))
423	422	feq2d 6640	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...(𝑚 + 1))⟶𝐴))
424		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = (𝑚 + 1) → (𝑓‘𝑛) = (𝑓‘(𝑚 + 1)))
425	424	sbceq1d 3742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = (𝑚 + 1) → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
426	38, 425	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝜏 ↔ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
427	426	anbi2d 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
428		oveq2 7360	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1)))
429	428	raleqdv 3293	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
430	423, 427, 429	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
431	430	exbidv 1922	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
432	431	rspcev 3573	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
433	125, 421, 432	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
434	433	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
435	434	exlimdv 1934	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
436	435	rexlimdva 3134	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
437	123, 436	biimtrid 242	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
438	73, 88, 437	3syld 60	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
439	438	an42s 661	. . . . . . . . . . . . . . . 16 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
440	439	rexlimdvaa 3135	. . . . . . . . . . . . . . 15 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))))
441	440	imp 406	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ ∃𝑏 ∈ 𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
442		fdc.10	. . . . . . . . . . . . . 14 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑))
443	65, 441, 442	mpjaodan 960	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
444	138	anbi1d 631	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏)))
445	444	3anbi2d 1443	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
446	445	exbidv 1922	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
447	446	rexbidv 3157	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑎 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
448	447	elrab3 3644	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝐴 → (𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
449	448	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
450	443, 449	sylibrd 259	. . . . . . . . . . . 12 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
451	450	ex 412	. . . . . . . . . . 11 ⊢ (𝜂 → (𝑎 ∈ 𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
452	451	com23 86	. . . . . . . . . 10 ⊢ (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
453		eldif 3908	. . . . . . . . . . . 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 3128	. . . . . 6 ⊢ (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
461		df-ne 2930	. . . . . . 7 ⊢ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
462		fdc.9	. . . . . . . 8 ⊢ (𝜂 → 𝑅 Fr 𝐴)
463		difss 4085	. . . . . . . 8 ⊢ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴
464		fdc.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ V
465		difexg 5269	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V)
466	464, 465	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V
467		fri 5577	. . . . . . . . . 10 ⊢ ((((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
468	466, 467	mpanl1 700	. . . . . . . . 9 ⊢ ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
469	468	expr 456	. . . . . . . 8 ⊢ ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
470	462, 463, 469	sylancl 586	. . . . . . 7 ⊢ (𝜂 → ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
471	461, 470	biimtrrid 243	. . . . . 6 ⊢ (𝜂 → (¬ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
472	460, 471	mt3d 148	. . . . 5 ⊢ (𝜂 → (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
473		ssdif0 4315	. . . . 5 ⊢ (𝐴 ⊆ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
474	472, 473	sylibr 234	. . . 4 ⊢ (𝜂 → 𝐴 ⊆ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
475	76	a1i 11	. . . 4 ⊢ (𝜂 → {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴)
476	474, 475	eqssd 3948	. . 3 ⊢ (𝜂 → 𝐴 = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
477		rabid2 3429	. . 3 ⊢ (𝐴 = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
478	476, 477	sylib 218	. 2 ⊢ (𝜂 → ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
479		eqeq2 2745	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝐶))
480	479	anbi1d 631	. . . . . 6 ⊢ (𝑐 = 𝐶 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏)))
481	480	3anbi2d 1443	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
482	481	exbidv 1922	. . . 4 ⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
483	482	rexbidv 3157	. . 3 ⊢ (𝑐 = 𝐶 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
484	483	rspcva 3571	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
485	1, 478, 484	syl2anc 584	1 ⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2929  ∀wral 3048  ∃wrex 3057  {crab 3396  Vcvv 3437  [wsbc 3737   ∖ cdif 3895   ⊆ wss 3898  ∅c0 4282  ifcif 4474  {csn 4575  ⟨cop 4581   class class class wbr 5093   ↦ cmpt 5174   Fr wfr 5569  ⟶wf 6482  ‘cfv 6486  (class class class)co 7352  ℂcc 11011  ℝcr 11012  1c1 11014   + caddc 11016   < clt 11153   ≤ cle 11154   − cmin 11351  ℤcz 12475  ℤ_≥cuz 12738  ...cfz 13409

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674  ax-cnex 11069  ax-resscn 11070  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-mulcom 11077  ax-addass 11078  ax-mulass 11079  ax-distr 11080  ax-i2m1 11081  ax-1ne0 11082  ax-1rid 11083  ax-rnegex 11084  ax-rrecex 11085  ax-cnre 11086  ax-pre-lttri 11087  ax-pre-lttrn 11088  ax-pre-ltadd 11089  ax-pre-mulgt0 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-mpo 7357  df-om 7803  df-1st 7927  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-rdg 8335  df-er 8628  df-en 8876  df-dom 8877  df-sdom 8878  df-pnf 11155  df-mnf 11156  df-xr 11157  df-ltxr 11158  df-le 11159  df-sub 11353  df-neg 11354  df-nn 12133  df-n0 12389  df-z 12476  df-uz 12739  df-fz 13410

This theorem is referenced by:  fdc1  37806