Theorem fdc 36001

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 12690	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
4	2, 3	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑀 ∈ (ℤ≥‘𝑀)
5		fdc.3	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑍 = (ℤ≥‘𝑀)
6	4, 5	eleqtrri 2836	. . . . . . . . . . . . . . . . 17 ⊢ 𝑀 ∈ 𝑍
7		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩}
8	2	elexi 3460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑀 ∈ V
9		vex 3445	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝑎 ∈ V
10	8, 9	fsn 7057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ↔ {⟨𝑀, 𝑎⟩} = {⟨𝑀, 𝑎⟩})
11	7, 10	mpbir 230	. . . . . . . . . . . . . . . . . . . . 21 ⊢ {⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎}
12		snssi 4754	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
13		fss 6662	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({⟨𝑀, 𝑎⟩}:{𝑀}⟶{𝑎} ∧ {𝑎} ⊆ 𝐴) → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
14	11, 12, 13	sylancr 587	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 ∈ 𝐴 → {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
15		fzsn 13391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀})
16	2, 15	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀...𝑀) = {𝑀}
17	16	feq2i 6637	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:{𝑀}⟶𝐴)
18	14, 17	sylibr 233	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ 𝐴 → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
19	18	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴)
20	8, 9	fvsn 7103	. . . . . . . . . . . . . . . . . . 19 ⊢ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎
21	20	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎)
22		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → 𝜃)
23		snex 5373	. . . . . . . . . . . . . . . . . . 19 ⊢ {⟨𝑀, 𝑎⟩} ∈ V
24		feq1 6626	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓:(𝑀...𝑀)⟶𝐴 ↔ {⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴))
25		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓‘𝑀) = ({⟨𝑀, 𝑎⟩}‘𝑀))
26	25	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓‘𝑀) = 𝑎 ↔ ({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎))
27	25, 20	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (𝑓‘𝑀) = 𝑎)
28		sbceq2a 3738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓‘𝑀) = 𝑎 → ([(𝑓‘𝑀) / 𝑎]𝜃 ↔ 𝜃))
29	27, 28	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ([(𝑓‘𝑀) / 𝑎]𝜃 ↔ 𝜃))
30	26, 29	anbi12d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → (((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ↔ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃)))
31	24, 30	anbi12d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 = {⟨𝑀, 𝑎⟩} → ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)) ↔ ({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃))))
32	23, 31	spcev 3554	. . . . . . . . . . . . . . . . . 18 ⊢ (({⟨𝑀, 𝑎⟩}:(𝑀...𝑀)⟶𝐴 ∧ (({⟨𝑀, 𝑎⟩}‘𝑀) = 𝑎 ∧ 𝜃)) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
33	19, 21, 22, 32	syl12anc 834	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
34		oveq2 7337	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀))
35	34	feq2d 6631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...𝑀)⟶𝐴))
36		fvex 6832	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓‘𝑛) ∈ V
37		fdc.7	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (𝑓‘𝑛) → (𝜃 ↔ 𝜏))
38	36, 37	sbcie 3769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ 𝜏)
39		fveq2 6819	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑀 → (𝑓‘𝑛) = (𝑓‘𝑀))
40	39	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑀 → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘𝑀) / 𝑎]𝜃))
41	38, 40	bitr3id 284	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝜏 ↔ [(𝑓‘𝑀) / 𝑎]𝜃))
42	41	anbi2d 629	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
43		oveq2 7337	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑀 → (𝑁...𝑛) = (𝑁...𝑀))
44		fdc.4	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑁 = (𝑀 + 1)
45	44	oveq1i 7339	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑁...𝑀) = ((𝑀 + 1)...𝑀)
46	2	zrei 12418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ 𝑀 ∈ ℝ
47	46	ltp1i 11972	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑀 < (𝑀 + 1)
48		peano2z 12454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑀 ∈ ℤ → (𝑀 + 1) ∈ ℤ)
49	2, 48	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑀 + 1) ∈ ℤ
50		fzn 13365	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑀 + 1) ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅))
51	49, 2, 50	mp2an 689	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑀 < (𝑀 + 1) ↔ ((𝑀 + 1)...𝑀) = ∅)
52	47, 51	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑀 + 1)...𝑀) = ∅
53	45, 52	eqtri 2764	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑁...𝑀) = ∅
54	43, 53	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑀 → (𝑁...𝑛) = ∅)
55	54	raleqdv 3309	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑀 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ ∅ 𝜒))
56	35, 42, 55	3anbi123d 1435	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒)))
57		ral0 4456	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑘 ∈ ∅ 𝜒
58		df-3an 1088	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)) ∧ ∀𝑘 ∈ ∅ 𝜒))
59	57, 58	mpbiran2 707	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃) ∧ ∀𝑘 ∈ ∅ 𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃)))
60	56, 59	bitrdi 286	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑀 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))))
61	60	exbidv 1923	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑀 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))))
62	61	rspcev 3570	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑀 ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...𝑀)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘𝑀) / 𝑎]𝜃))) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
63	6, 33, 62	sylancr 587	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝜃) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
64	63	adantll 711	. . . . . . . . . . . . . . 15 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜃) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
65	64	a1d 25	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ 𝜃) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
66		fdc.11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → 𝑏𝑅𝑎)
67		breq1 5092	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = 𝑏 → (𝑑𝑅𝑎 ↔ 𝑏𝑅𝑎))
68	67	rspcev 3570	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∧ 𝑏𝑅𝑎) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎)
69	68	expcom 414	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏𝑅𝑎 → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
70	66, 69	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎))
71		dfrex2 3073	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})𝑑𝑅𝑎 ↔ ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
72	70, 71	syl6ib 250	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
73	72	con2d 134	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
74		eldif 3907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ (𝑏 ∈ 𝐴 ∧ ¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
75	74	simplbi2 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → 𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))))
76		ssrab2 4024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴
77		dfss4 4204	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ({𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴 ↔ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
78	76, 77	mpbi 229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}
79	78	eleq2i 2828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ 𝑏 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
80		eqeq2 2748	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑏 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝑏))
81	80	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑏 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏)))
82	81	3anbi2d 1440	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑏 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
83	82	exbidv 1923	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑏 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
84	83	rexbidv 3171	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑏 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
85	84	elrab3 3635	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑏 ∈ 𝐴 → (𝑏 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
86	79, 85	bitrid 282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∈ 𝐴 → (𝑏 ∈ (𝐴 ∖ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
87	75, 86	sylibd 238	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ 𝐴 → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
88	87	ad2antll 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (¬ 𝑏 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
89		oveq2 7337	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑀...𝑛) = (𝑀...𝑚))
90	89	feq2d 6631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...𝑚)⟶𝐴))
91		fveq2 6819	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝑓‘𝑛) = (𝑓‘𝑚))
92	91	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘𝑚) / 𝑎]𝜃))
93	38, 92	bitr3id 284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝜏 ↔ [(𝑓‘𝑚) / 𝑎]𝜃))
94	93	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃)))
95		oveq2 7337	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑚 → (𝑁...𝑛) = (𝑁...𝑚))
96	95	raleqdv 3309	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑚 → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
97	90, 94, 96	3anbi123d 1435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑚 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
98	97	exbidv 1923	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑚 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒)))
99	98	cbvrexvw 3222	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒))
100		feq1 6626	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (𝑓:(𝑀...𝑚)⟶𝐴 ↔ 𝑔:(𝑀...𝑚)⟶𝐴))
101		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑀) = (𝑔‘𝑀))
102	101	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → ((𝑓‘𝑀) = 𝑏 ↔ (𝑔‘𝑀) = 𝑏))
103		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑚) = (𝑔‘𝑚))
104	103	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑚) / 𝑎]𝜃 ↔ [(𝑔‘𝑚) / 𝑎]𝜃))
105	102, 104	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ↔ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)))
106		fvex 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘(𝑘 − 1)) ∈ V
107		fdc.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → (𝜑 ↔ 𝜓))
108	107	sbcbidv 3785	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓‘(𝑘 − 1)) → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑓‘𝑘) / 𝑏]𝜓))
109	106, 108	sbcie 3769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑓‘𝑘) / 𝑏]𝜓)
110		fvex 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓‘𝑘) ∈ V
111		fdc.6	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 = (𝑓‘𝑘) → (𝜓 ↔ 𝜒))
112	110, 111	sbcie 3769	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ([(𝑓‘𝑘) / 𝑏]𝜓 ↔ 𝜒)
113	109, 112	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ 𝜒)
114		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑔 → (𝑓‘(𝑘 − 1)) = (𝑔‘(𝑘 − 1)))
115		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑔 → (𝑓‘𝑘) = (𝑔‘𝑘))
116	115	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑔 → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘𝑘) / 𝑏]𝜑))
117	114, 116	sbceqbid 3733	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑓 = 𝑔 → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
118	113, 117	bitr3id 284	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 = 𝑔 → (𝜒 ↔ [(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
119	118	ralbidv 3170	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 = 𝑔 → (∀𝑘 ∈ (𝑁...𝑚)𝜒 ↔ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
120	100, 105, 119	3anbi123d 1435	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑔 → ((𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)))
121	120	cbvexvw 2039	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
122	121	rexbii 3093	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑚 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑚)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ [(𝑓‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
123	99, 122	bitri 274	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑))
124	5	peano2uzs 12735	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ 𝑍)
125	124	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → (𝑚 + 1) ∈ 𝑍)
126		sbceq2a 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 = 𝑏 → ([𝑑 / 𝑏]𝜑 ↔ 𝜑))
127	126	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑑 = 𝑏 → (([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ↔ (𝜑 ∧ 𝑎 ∈ 𝐴)))
128	127	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 = 𝑏 → ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ↔ ((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍)))
129		eqeq2 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑑 = 𝑏 → ((𝑔‘𝑀) = 𝑑 ↔ (𝑔‘𝑀) = 𝑏))
130	129	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑑 = 𝑏 → (((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ↔ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)))
131	130	3anbi2d 1440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑎 → ([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑))
135		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑐 = 𝑎 → (𝑐 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴))
136	134, 135	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = 𝑎 → (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ↔ ([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴)))
137	136	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = 𝑎 → ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ↔ (([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍)))
138		eqeq2 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑐 = 𝑎 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝑎))
139	138	anbi1d 630	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑐 = 𝑎 → (((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
140	139	3anbi2d 1440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (ℤ≥‘𝑀))
145	144, 5	eleq2s 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘𝑀))
146		elfzp12 13428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
147	145, 146	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
148	147	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↔ (𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))))
149		iftrue 4478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = 𝑐)
150	149	eleq1d 2821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = 𝑀 → (if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ 𝑐 ∈ 𝐴))
151	150	biimprcd 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑐 ∈ 𝐴 → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
152	151	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 = 𝑀 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
153		1re 11068	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ 1 ∈ ℝ
154	46, 153	readdcli 11083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑀 + 1) ∈ ℝ
155	46, 154	ltnlei 11189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑀 < (𝑀 + 1) ↔ ¬ (𝑀 + 1) ≤ 𝑀)
156	47, 155	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ¬ (𝑀 + 1) ≤ 𝑀
157		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1))))
158		elfzle1 13352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑀 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀)
159	157, 158	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑥 = 𝑀 → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑀 + 1) ≤ 𝑀))
160	159	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 = 𝑀 → (𝑀 + 1) ≤ 𝑀))
161	156, 160	mtoi 198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → ¬ 𝑥 = 𝑀)
162	161	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → ¬ 𝑥 = 𝑀)
163	162	iffalsed 4483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = (𝑔‘(𝑥 − 1)))
164		elfzelz 13349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → 𝑥 ∈ ℤ)
165	164	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → 𝑥 ∈ ℤ)
166		eluzelz 12685	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑚 ∈ ℤ)
167	166, 5	eleq2s 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℤ)
168	167	peano2zd 12522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ ℤ)
169		1z 12443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 1 ∈ ℤ
170		fzsubel 13385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) ↔ (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
171	170	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑥 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
172	169, 171	mpanr2 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝑀 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
173	49, 172	mpanl1 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (((𝑚 + 1) ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
174	173	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 ∈ ℤ → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1))))
178	165, 177	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)))
179	46	recni 11082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑀 ∈ ℂ
180		ax-1cn 11022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 1 ∈ ℂ
181	179, 180	pncan3oi 11330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑀 + 1) − 1) = 𝑀
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑀 + 1) − 1) = 𝑀)
183	167	zcnd 12520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑚 ∈ 𝑍 → 𝑚 ∈ ℂ)
184		pncan 11320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) − 1) = 𝑚)
185	183, 180, 184	sylancl 586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑚 + 1) − 1) = 𝑚)
186	182, 185	oveq12d 7347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑚 ∈ 𝑍 → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
187	186	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (((𝑀 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑀...𝑚))
188	178, 187	eleqtrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑥 − 1) ∈ (𝑀...𝑚))
189		ffvelcdm 7009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑥 − 1) ∈ (𝑀...𝑚)) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
190	188, 189	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ (𝑚 ∈ 𝑍 ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
191	190	anassrs 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (((𝑔:(𝑀...𝑚)⟶𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
192	191	ancom1s 650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → (𝑔‘(𝑥 − 1)) ∈ 𝐴)
193	163, 192	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) ∧ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
194	193	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
195	194	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
196	152, 195	jaod 856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ((𝑥 = 𝑀 ∨ 𝑥 ∈ ((𝑀 + 1)...(𝑚 + 1))) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
197	148, 196	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴))
198	197	ralrimiv 3138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → ∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴)
199		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))
200	199	fmpt 7034	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (∀𝑥 ∈ (𝑀...(𝑚 + 1))if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) ∈ 𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
201	198, 200	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
202	201	adantlll 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ 𝑔:(𝑀...𝑚)⟶𝐴) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
203	202	3ad2antr1 1187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴)
204		eluzfz1 13356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
205	144, 204	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...(𝑚 + 1)))
206	205, 5	eleq2s 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ (𝑀...(𝑚 + 1)))
207		vex 3445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑐 ∈ V
208	149, 199, 207	fvmpt 6925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
209	206, 208	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
210	209	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
211		eluzfz2 13357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
212	144, 211	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
213	212, 5	eleq2s 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (𝑀...(𝑚 + 1)))
214		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = (𝑚 + 1) → (𝑥 = 𝑀 ↔ (𝑚 + 1) = 𝑀))
215		fvoveq1 7352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑥 = (𝑚 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑚 + 1) − 1)))
216	214, 215	ifbieq2d 4498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑥 = (𝑚 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))))
217		fvex 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑔‘((𝑚 + 1) − 1)) ∈ V
218	207, 217	ifex 4522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) ∈ V
219	216, 199, 218	fvmpt 6925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 12688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ≤ 𝑚)
222	221, 5	eleq2s 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ≤ 𝑚)
223		zleltp1 12464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ≤ 𝑚 ↔ 𝑀 < (𝑚 + 1)))
224	2, 167, 223	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑚 ∈ 𝑍 → (𝑀 ≤ 𝑚 ↔ 𝑀 < (𝑚 + 1)))
225	222, 224	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (𝑚 ∈ 𝑍 → 𝑀 < (𝑚 + 1))
226		ltne 11165	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑀 ∈ ℝ ∧ 𝑀 < (𝑚 + 1)) → (𝑚 + 1) ≠ 𝑀)
227	46, 225, 226	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ≠ 𝑀)
228	227	neneqd 2945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑚 ∈ 𝑍 → ¬ (𝑚 + 1) = 𝑀)
229	228	iffalsed 4483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ 𝑍 → if((𝑚 + 1) = 𝑀, 𝑐, (𝑔‘((𝑚 + 1) − 1))) = (𝑔‘((𝑚 + 1) − 1)))
230	185	fveq2d 6823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑚 ∈ 𝑍 → (𝑔‘((𝑚 + 1) − 1)) = (𝑔‘𝑚))
231	220, 229, 230	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) = (𝑔‘𝑚))
232	231	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑚 ∈ 𝑍 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃 ↔ [(𝑔‘𝑚) / 𝑎]𝜃))
233	232	biimpar 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑚 ∈ 𝑍 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
234	233	ad2ant2l 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
235	234	3ad2antr2 1188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)
236		eluzp1p1 12703	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → (𝑚 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
237	236, 5	eleq2s 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘(𝑀 + 1)))
238	44	fveq2i 6822	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (ℤ≥‘𝑁) = (ℤ≥‘(𝑀 + 1))
239	237, 238	eleqtrrdi 2848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (𝑚 ∈ 𝑍 → (𝑚 + 1) ∈ (ℤ≥‘𝑁))
240		elfzp12 13428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ ((𝑚 + 1) ∈ (ℤ≥‘𝑁) → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
241	239, 240	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (𝑚 ∈ 𝑍 → (𝑗 ∈ (𝑁...(𝑚 + 1)) ↔ (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))))
242	241	biimpa 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
243	242	adantll 711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
244	243	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ (𝑁...(𝑚 + 1))) → (𝑗 = 𝑁 ∨ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))))
245		oveq1 7336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 = 𝑁 → (𝑗 − 1) = (𝑁 − 1))
246	44	oveq1i 7339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 − 1) = ((𝑀 + 1) − 1)
247	246, 181	eqtri 2764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑁 − 1) = 𝑀
248	245, 247	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑗 = 𝑁 → (𝑗 − 1) = 𝑀)
249	248	fveq2d 6823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
250	249	ad2antll 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
251	209	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐)
252	250, 251	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = 𝑐)
253	44	eqeq2i 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 = 𝑁 ↔ 𝑗 = (𝑀 + 1))
254		fveq2 6819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 = (𝑀 + 1) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
255	253, 254	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑗 = 𝑁 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
256	255	ad2antll 726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)))
257	46, 154, 47	ltleii 11191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑀 ≤ (𝑀 + 1)
258		eluz2 12681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑀 + 1) ∈ ℤ ∧ 𝑀 ≤ (𝑀 + 1)))
259	2, 49, 257, 258	mpbir3an 1340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 + 1) ∈ (ℤ≥‘𝑀)
260		fzss1 13388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((𝑀 + 1) ∈ (ℤ≥‘𝑀) → ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
261	259, 260	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑀 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
262		eluzfz1 13356	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑚 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑚))
263	262, 5	eleq2s 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ 𝑍 → 𝑀 ∈ (𝑀...𝑚))
264		fzaddel 13383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ (𝑀 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
265	2, 169, 264	mpanr12 702	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
266	2, 167, 265	sylancr 587	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑚 ∈ 𝑍 → (𝑀 ∈ (𝑀...𝑚) ↔ (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1))))
267	263, 266	mpbid 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑚 ∈ 𝑍 → (𝑀 + 1) ∈ ((𝑀 + 1)...(𝑚 + 1)))
268	261, 267	sselid 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑚 ∈ 𝑍 → (𝑀 + 1) ∈ (𝑀...(𝑚 + 1)))
269		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 = 𝑀 ↔ (𝑀 + 1) = 𝑀))
270		oveq1 7336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 − 1) = ((𝑀 + 1) − 1))
271	270, 181	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑥 = (𝑀 + 1) → (𝑥 − 1) = 𝑀)
272	271	fveq2d 6823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑥 = (𝑀 + 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘𝑀))
273	269, 272	ifbieq2d 4498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = (𝑀 + 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)))
274		fvex 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑔‘𝑀) ∈ V
275	207, 274	ifex 4522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) ∈ V
276	273, 199, 275	fvmpt 6925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑀 + 1) ≠ 𝑀
279		ifnefalse 4484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑀 + 1) ≠ 𝑀 → if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) = (𝑔‘𝑀))
280	278, 279	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ if((𝑀 + 1) = 𝑀, 𝑐, (𝑔‘𝑀)) = (𝑔‘𝑀)
281	277, 280	eqtrdi 2792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔‘𝑀))
282	281	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑀 + 1)) = (𝑔‘𝑀))
283		simprl 768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → (𝑔‘𝑀) = 𝑑)
284	256, 282, 283	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = 𝑑)
285	284	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [𝑑 / 𝑏]𝜑))
286	252, 285	sbceqbid 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ ((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [𝑐 / 𝑎][𝑑 / 𝑏]𝜑))
287	286	biimparc 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ⊢ (([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ (𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
288	287	anassrs 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ 𝑗 = 𝑁)) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
289	288	anassrs 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ (𝑔‘𝑀) = 𝑑) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
290	289	adantlrr 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 = 𝑁) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
291		elfzelz 13349	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℤ)
292	291	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ℤ)
293	44, 49	eqeltri 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ 𝑁 ∈ ℤ
294		peano2z 12454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑁 ∈ ℤ → (𝑁 + 1) ∈ ℤ)
295	293, 294	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 + 1) ∈ ℤ
296		fzsubel 13385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
297	296	biimpd 228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ (𝑗 ∈ ℤ ∧ 1 ∈ ℤ)) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
298	169, 297	mpanr2 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((((𝑁 + 1) ∈ ℤ ∧ (𝑚 + 1) ∈ ℤ) ∧ 𝑗 ∈ ℤ) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
299	298	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 407	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 ∈ ℤ → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1))))
303	292, 302	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)))
304	293	zrei 12418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ 𝑁 ∈ ℝ
305	304	recni 11082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑁 ∈ ℂ
306	305, 180	pncan3oi 11330	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑁 + 1) − 1) = 𝑁
307	306	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑚 ∈ 𝑍 → ((𝑁 + 1) − 1) = 𝑁)
308	307, 185	oveq12d 7347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑚 ∈ 𝑍 → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
309	308	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (((𝑁 + 1) − 1)...((𝑚 + 1) − 1)) = (𝑁...𝑚))
310	303, 309	eleqtrd 2839	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...𝑚))
311		fvoveq1 7352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = (𝑗 − 1) → (𝑔‘(𝑘 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
312		fveq2 6819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ (𝑘 = (𝑗 − 1) → (𝑔‘𝑘) = (𝑔‘(𝑗 − 1)))
313	312	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ (𝑘 = (𝑗 − 1) → ([(𝑔‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
314	311, 313	sbceqbid 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ (𝑘 = (𝑗 − 1) → ([(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑 ↔ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
315	314	rspcva 3568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ (((𝑗 − 1) ∈ (𝑁...𝑚) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
316	310, 315	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ⊢ (((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑)
317	44, 259	eqeltri 2833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ 𝑁 ∈ (ℤ≥‘𝑀)
318		fzss1 13388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
319	317, 318	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑁...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
320		fzssp1 13392	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑁...𝑚) ⊆ (𝑁...(𝑚 + 1))
321	320, 310	sselid 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑁...(𝑚 + 1)))
322	319, 321	sselid 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → (𝑗 − 1) ∈ (𝑀...(𝑚 + 1)))
323		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = (𝑗 − 1) → (𝑥 = 𝑀 ↔ (𝑗 − 1) = 𝑀))
324		fvoveq1 7352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = (𝑗 − 1) → (𝑔‘(𝑥 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
325	323, 324	ifbieq2d 4498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑥 = (𝑗 − 1) → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))))
326		fvex 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑔‘((𝑗 − 1) − 1)) ∈ V
327	207, 326	ifex 4522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) ∈ V
328	325, 199, 327	fvmpt 6925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 + 1) < ((𝑀 + 1) + 1)
331	44	oveq1i 7339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑁 + 1) = ((𝑀 + 1) + 1)
332	330, 331	breqtrri 5116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑀 + 1) < (𝑁 + 1)
333	304, 153	readdcli 11083	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑁 + 1) ∈ ℝ
334	154, 333	ltnlei 11189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑀 + 1) < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ (𝑀 + 1))
335	332, 334	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ¬ (𝑁 + 1) ≤ (𝑀 + 1)
336	291	zcnd 12520	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → 𝑗 ∈ ℂ)
337		subadd 11317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ ∧ 𝑀 ∈ ℂ) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
338	180, 179, 337	mp3an23 1452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 ∈ ℂ → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
339	336, 338	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 ↔ (1 + 𝑀) = 𝑗))
340		eqcom 2743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((1 + 𝑀) = 𝑗 ↔ 𝑗 = (1 + 𝑀))
341	180, 179	addcomi 11259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (1 + 𝑀) = (𝑀 + 1)
342	341	eqeq2i 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑗 = (1 + 𝑀) ↔ 𝑗 = (𝑀 + 1))
343	340, 342	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ ((1 + 𝑀) = 𝑗 ↔ 𝑗 = (𝑀 + 1))
344		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ (𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1))))
345		elfzle1 13352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 ⊢ ((𝑀 + 1) ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1))
346	344, 345	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑗 = (𝑀 + 1) → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ (𝑀 + 1)))
347	346	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = (𝑀 + 1) → (𝑁 + 1) ≤ (𝑀 + 1)))
348	343, 347	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((1 + 𝑀) = 𝑗 → (𝑁 + 1) ≤ (𝑀 + 1)))
349	339, 348	sylbid 239	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ((𝑗 − 1) = 𝑀 → (𝑁 + 1) ≤ (𝑀 + 1)))
350	335, 349	mtoi 198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ (𝑗 − 1) = 𝑀)
351	350	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ (𝑗 − 1) = 𝑀)
352	351	iffalsed 4483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if((𝑗 − 1) = 𝑀, 𝑐, (𝑔‘((𝑗 − 1) − 1))) = (𝑔‘((𝑗 − 1) − 1)))
353	329, 352	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = (𝑔‘((𝑗 − 1) − 1)))
354		peano2uz 12734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → (𝑁 + 1) ∈ (ℤ≥‘𝑀))
355		fzss1 13388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ((𝑁 + 1) ∈ (ℤ≥‘𝑀) → ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1)))
356	317, 354, 355	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑁 + 1)...(𝑚 + 1)) ⊆ (𝑀...(𝑚 + 1))
357		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)))
358	356, 357	sselid 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → 𝑗 ∈ (𝑀...(𝑚 + 1)))
359		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = 𝑗 → (𝑥 = 𝑀 ↔ 𝑗 = 𝑀))
360		fvoveq1 7352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑥 = 𝑗 → (𝑔‘(𝑥 − 1)) = (𝑔‘(𝑗 − 1)))
361	359, 360	ifbieq2d 4498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑥 = 𝑗 → if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
362		fvex 6832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑔‘(𝑗 − 1)) ∈ V
363	207, 362	ifex 4522	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) ∈ V
364	361, 199, 363	fvmpt 6925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ (𝑗 ∈ (𝑀...(𝑚 + 1)) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
365	358, 364	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))))
366	47, 44	breqtrri 5116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑀 < 𝑁
367	304	ltp1i 11972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ 𝑁 < (𝑁 + 1)
368	46, 304, 333	lttri 11194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ ((𝑀 < 𝑁 ∧ 𝑁 < (𝑁 + 1)) → 𝑀 < (𝑁 + 1))
369	366, 367, 368	mp2an 689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ 𝑀 < (𝑁 + 1)
370	46, 333	ltnlei 11189	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑀 < (𝑁 + 1) ↔ ¬ (𝑁 + 1) ≤ 𝑀)
371	369, 370	mpbi 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ ¬ (𝑁 + 1) ≤ 𝑀
372		eleq1 2824	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) ↔ 𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1))))
373		elfzle1 13352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 ⊢ (𝑀 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀)
374	372, 373	syl6bi 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 ⊢ (𝑗 = 𝑀 → (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑁 + 1) ≤ 𝑀))
375	374	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → (𝑗 = 𝑀 → (𝑁 + 1) ≤ 𝑀))
376	371, 375	mtoi 198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ⊢ (𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1)) → ¬ 𝑗 = 𝑀)
377	376	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ¬ 𝑗 = 𝑀)
378	377	iffalsed 4483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → if(𝑗 = 𝑀, 𝑐, (𝑔‘(𝑗 − 1))) = (𝑔‘(𝑗 − 1)))
379	365, 378	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = (𝑔‘(𝑗 − 1)))
380	379	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
381	353, 380	sbceqbid 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 ⊢ ((𝑚 ∈ 𝑍 ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [(𝑔‘((𝑗 − 1) − 1)) / 𝑎][(𝑔‘(𝑗 − 1)) / 𝑏]𝜑))
382	381	biimpar 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ⊢ (((𝑚 ∈ 𝑍 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
385	384	adantlrl 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ⊢ (((𝑚 ∈ 𝑍 ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
386	385	adantlll 715	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) ∧ 𝑗 ∈ ((𝑁 + 1)...(𝑚 + 1))) → [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
387	290, 386	jaodan 955	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑)
390		fvoveq1 7352	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
391		fveq2 6819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ⊢ (𝑗 = 𝑘 → ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
392	391	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
393	390, 392	sbceqbid 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑗 = 𝑘 → ([((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
394	393	cbvralvw 3221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (∀𝑗 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑗 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑗) / 𝑏]𝜑 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
395	389, 394	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
396	395	adantllr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ ((𝑔‘𝑀) = 𝑑 ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
397	396	adantrlr 720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
398	397	3adantr1 1168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑)
399		ovex 7362	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑀...(𝑚 + 1)) ∈ V
400	399	mptex 7149	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) ∈ V
401		feq1 6626	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ↔ (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))):(𝑀...(𝑚 + 1))⟶𝐴))
402		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘𝑀) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀))
403	402	eqeq1d 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ((𝑓‘𝑀) = 𝑐 ↔ ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐))
404		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑚 + 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)))
405	404	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑚 + 1)) / 𝑎]𝜃 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃))
406	403, 405	anbi12d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ↔ (((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑀) = 𝑐 ∧ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑚 + 1)) / 𝑎]𝜃)))
407		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘(𝑘 − 1)) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)))
408		fveq1 6818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝑓‘𝑘) = ((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘))
409	408	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘𝑘) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
410	407, 409	sbceqbid 3733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → ([(𝑓‘(𝑘 − 1)) / 𝑎][(𝑓‘𝑘) / 𝑏]𝜑 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
411	113, 410	bitr3id 284	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (𝜒 ↔ [((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
412	411	ralbidv 3170	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑓 = (𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1)))) → (∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))[((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘(𝑘 − 1)) / 𝑎][((𝑥 ∈ (𝑀...(𝑚 + 1)) ↦ if(𝑥 = 𝑀, 𝑐, (𝑔‘(𝑥 − 1))))‘𝑘) / 𝑏]𝜑))
413	401, 406, 412	3anbi123d 1435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
416	415	ex 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((([𝑐 / 𝑎][𝑑 / 𝑏]𝜑 ∧ 𝑐 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
417	143, 416	chvarvv 2001	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((([𝑑 / 𝑏]𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑑 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
418	133, 417	chvarvv 2001	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
419	418	adantlrr 718	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
420	419	adantlll 715	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
421	420	imp 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
422		oveq2 7337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝑀...𝑛) = (𝑀...(𝑚 + 1)))
423	422	feq2d 6631	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (𝑓:(𝑀...𝑛)⟶𝐴 ↔ 𝑓:(𝑀...(𝑚 + 1))⟶𝐴))
424		fveq2 6819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = (𝑚 + 1) → (𝑓‘𝑛) = (𝑓‘(𝑚 + 1)))
425	424	sbceq1d 3731	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = (𝑚 + 1) → ([(𝑓‘𝑛) / 𝑎]𝜃 ↔ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
426	38, 425	bitr3id 284	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝜏 ↔ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃))
427	426	anbi2d 629	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃)))
428		oveq2 7337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = (𝑚 + 1) → (𝑁...𝑛) = (𝑁...(𝑚 + 1)))
429	428	raleqdv 3309	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = (𝑚 + 1) → (∀𝑘 ∈ (𝑁...𝑛)𝜒 ↔ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒))
430	423, 427, 429	3anbi123d 1435	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = (𝑚 + 1) → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
431	430	exbidv 1923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = (𝑚 + 1) → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)))
432	431	rspcev 3570	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑚 + 1) ∈ 𝑍 ∧ ∃𝑓(𝑓:(𝑀...(𝑚 + 1))⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ [(𝑓‘(𝑚 + 1)) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...(𝑚 + 1))𝜒)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
433	125, 421, 432	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) ∧ (𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
434	433	ex 413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → ((𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
435	434	exlimdv 1935	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑚 ∈ 𝑍) → (∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
436	435	rexlimdva 3148	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∃𝑚 ∈ 𝑍 ∃𝑔(𝑔:(𝑀...𝑚)⟶𝐴 ∧ ((𝑔‘𝑀) = 𝑏 ∧ [(𝑔‘𝑚) / 𝑎]𝜃) ∧ ∀𝑘 ∈ (𝑁...𝑚)[(𝑔‘(𝑘 − 1)) / 𝑎][(𝑔‘𝑘) / 𝑏]𝜑) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
437	123, 436	biimtrid 241	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑏 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
438	73, 88, 437	3syld 60	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜂 ∧ 𝜑) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
439	438	an42s 658	. . . . . . . . . . . . . . . 16 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐴 ∧ 𝜑)) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
440	439	rexlimdvaa 3149	. . . . . . . . . . . . . . 15 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐴 𝜑 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))))
441	440	imp 407	. . . . . . . . . . . . . 14 ⊢ (((𝜂 ∧ 𝑎 ∈ 𝐴) ∧ ∃𝑏 ∈ 𝐴 𝜑) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
442		fdc.10	. . . . . . . . . . . . . 14 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝜃 ∨ ∃𝑏 ∈ 𝐴 𝜑))
443	65, 441, 442	mpjaodan 956	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
444	138	anbi1d 630	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = 𝑎 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏)))
445	444	3anbi2d 1440	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝑎 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
446	445	exbidv 1923	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 = 𝑎 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
447	446	rexbidv 3171	. . . . . . . . . . . . . . 15 ⊢ (𝑐 = 𝑎 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
448	447	elrab3 3635	. . . . . . . . . . . . . 14 ⊢ (𝑎 ∈ 𝐴 → (𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
449	448	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑎 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
450	443, 449	sylibrd 258	. . . . . . . . . . . 12 ⊢ ((𝜂 ∧ 𝑎 ∈ 𝐴) → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
451	450	ex 413	. . . . . . . . . . 11 ⊢ (𝜂 → (𝑎 ∈ 𝐴 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
452	451	com23 86	. . . . . . . . . 10 ⊢ (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → (𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
453		eldif 3907	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
454	453	notbii 319	. . . . . . . . . . 11 ⊢ (¬ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
455		iman 402	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ ¬ (𝑎 ∈ 𝐴 ∧ ¬ 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
456	454, 455	bitr4i 277	. . . . . . . . . 10 ⊢ (¬ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ↔ (𝑎 ∈ 𝐴 → 𝑎 ∈ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}))
457	452, 456	syl6ibr 251	. . . . . . . . 9 ⊢ (𝜂 → (∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎 → ¬ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})))
458	457	con2d 134	. . . . . . . 8 ⊢ (𝜂 → (𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
459	458	imp 407	. . . . . . 7 ⊢ ((𝜂 ∧ 𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})) → ¬ ∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
460	459	nrexdv 3142	. . . . . 6 ⊢ (𝜂 → ¬ ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
461		df-ne 2941	. . . . . . 7 ⊢ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ ↔ ¬ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
462		fdc.9	. . . . . . . 8 ⊢ (𝜂 → 𝑅 Fr 𝐴)
463		difss 4077	. . . . . . . 8 ⊢ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴
464		fdc.1	. . . . . . . . . . 11 ⊢ 𝐴 ∈ V
465		difexg 5268	. . . . . . . . . . 11 ⊢ (𝐴 ∈ V → (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V)
466	464, 465	ax-mp 5	. . . . . . . . . 10 ⊢ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V
467		fri 5574	. . . . . . . . . 10 ⊢ ((((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ∈ V ∧ 𝑅 Fr 𝐴) ∧ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
468	466, 467	mpanl1 697	. . . . . . . . 9 ⊢ ((𝑅 Fr 𝐴 ∧ ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅)) → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎)
469	468	expr 457	. . . . . . . 8 ⊢ ((𝑅 Fr 𝐴 ∧ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ⊆ 𝐴) → ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
470	462, 463, 469	sylancl 586	. . . . . . 7 ⊢ (𝜂 → ((𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ≠ ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
471	461, 470	syl5bir 242	. . . . . 6 ⊢ (𝜂 → (¬ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅ → ∃𝑎 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})∀𝑑 ∈ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) ¬ 𝑑𝑅𝑎))
472	460, 471	mt3d 148	. . . . 5 ⊢ (𝜂 → (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
473		ssdif0 4309	. . . . 5 ⊢ (𝐴 ⊆ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ (𝐴 ∖ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)}) = ∅)
474	472, 473	sylibr 233	. . . 4 ⊢ (𝜂 → 𝐴 ⊆ {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
475	76	a1i 11	. . . 4 ⊢ (𝜂 → {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ⊆ 𝐴)
476	474, 475	eqssd 3948	. . 3 ⊢ (𝜂 → 𝐴 = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)})
477		rabid2 3432	. . 3 ⊢ (𝐴 = {𝑐 ∈ 𝐴 ∣ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)} ↔ ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
478	476, 477	sylib 217	. 2 ⊢ (𝜂 → ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
479		eqeq2 2748	. . . . . . 7 ⊢ (𝑐 = 𝐶 → ((𝑓‘𝑀) = 𝑐 ↔ (𝑓‘𝑀) = 𝐶))
480	479	anbi1d 630	. . . . . 6 ⊢ (𝑐 = 𝐶 → (((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ↔ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏)))
481	480	3anbi2d 1440	. . . . 5 ⊢ (𝑐 = 𝐶 → ((𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ (𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
482	481	exbidv 1923	. . . 4 ⊢ (𝑐 = 𝐶 → (∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
483	482	rexbidv 3171	. . 3 ⊢ (𝑐 = 𝐶 → (∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒) ↔ ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)))
484	483	rspcva 3568	. 2 ⊢ ((𝐶 ∈ 𝐴 ∧ ∀𝑐 ∈ 𝐴 ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝑐 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒)) → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))
485	1, 478, 484	syl2anc 584	1 ⊢ (𝜂 → ∃𝑛 ∈ 𝑍 ∃𝑓(𝑓:(𝑀...𝑛)⟶𝐴 ∧ ((𝑓‘𝑀) = 𝐶 ∧ 𝜏) ∧ ∀𝑘 ∈ (𝑁...𝑛)𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1540  ∃wex 1780   ∈ wcel 2105   ≠ wne 2940  ∀wral 3061  ∃wrex 3070  {crab 3403  Vcvv 3441  [wsbc 3726   ∖ cdif 3894   ⊆ wss 3897  ∅c0 4268  ifcif 4472  {csn 4572  ⟨cop 4578   class class class wbr 5089   ↦ cmpt 5172   Fr wfr 5566  ⟶wf 6469  ‘cfv 6473  (class class class)co 7329  ℂcc 10962  ℝcr 10963  1c1 10965   + caddc 10967   < clt 11102   ≤ cle 11103   − cmin 11298  ℤcz 12412  ℤ_≥cuz 12675  ...cfz 13332

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-cnex 11020  ax-resscn 11021  ax-1cn 11022  ax-icn 11023  ax-addcl 11024  ax-addrcl 11025  ax-mulcl 11026  ax-mulrcl 11027  ax-mulcom 11028  ax-addass 11029  ax-mulass 11030  ax-distr 11031  ax-i2m1 11032  ax-1ne0 11033  ax-1rid 11034  ax-rnegex 11035  ax-rrecex 11036  ax-cnre 11037  ax-pre-lttri 11038  ax-pre-lttrn 11039  ax-pre-ltadd 11040  ax-pre-mulgt0 11041

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-1st 7891  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-rdg 8303  df-er 8561  df-en 8797  df-dom 8798  df-sdom 8799  df-pnf 11104  df-mnf 11105  df-xr 11106  df-ltxr 11107  df-le 11108  df-sub 11300  df-neg 11301  df-nn 12067  df-n0 12327  df-z 12413  df-uz 12676  df-fz 13333

This theorem is referenced by:  fdc1  36002