fdc

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)

	Ref	Expression
Hypotheses	fdc.1	$⊢ A \in V$
	fdc.2	$⊢ M \in ℤ$
	fdc.3	$⊢ Z = ℤ_{\geq M}$
	fdc.4	$⊢ N = M + 1$
	fdc.5	$⊢ a = f (k - 1) \to (φ \leftrightarrow ψ)$
	fdc.6	$⊢ b = f (k) \to (ψ \leftrightarrow χ)$
	fdc.7	$⊢ a = f (n) \to (θ \leftrightarrow τ)$
	fdc.8	$⊢ η \to C \in A$
	fdc.9	$⊢ η \to R Fr A$
	fdc.10	$⊢ (η \land a \in A) \to (θ \lor \exists b \in A φ)$
	fdc.11	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to b R a$
Assertion	fdc	$⊢ η \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = C \land τ) \land \forall k \in (N \dots n) χ)$

Proof

Step	Hyp	Ref	Expression
1		fdc.1	$⊢ A \in V$
2		fdc.2	$⊢ M \in ℤ$
3		fdc.3	$⊢ Z = ℤ_{\geq M}$
4		fdc.4	$⊢ N = M + 1$
5		fdc.5	$⊢ a = f (k - 1) \to (φ \leftrightarrow ψ)$
6		fdc.6	$⊢ b = f (k) \to (ψ \leftrightarrow χ)$
7		fdc.7	$⊢ a = f (n) \to (θ \leftrightarrow τ)$
8		fdc.8	$⊢ η \to C \in A$
9		fdc.9	$⊢ η \to R Fr A$
10		fdc.10	$⊢ (η \land a \in A) \to (θ \lor \exists b \in A φ)$
11		fdc.11	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to b R a$
12		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
13	2 12	ax-mp	$⊢ M \in ℤ_{\geq M}$
14	13 3	eleqtrri	$⊢ M \in Z$
15		eqid	$⊢ \{⟨M, a⟩\} = \{⟨M, a⟩\}$
16	2	elexi	$⊢ M \in V$
17		vex	$⊢ a \in V$
18	16 17	fsn	$⊢ \{⟨M, a⟩\} : \{M\} ⟶ \{a\} \leftrightarrow \{⟨M, a⟩\} = \{⟨M, a⟩\}$
19	15 18	mpbir	$⊢ \{⟨M, a⟩\} : \{M\} ⟶ \{a\}$
20		snssi	$⊢ a \in A \to \{a\} \subseteq A$
21		fss	$⊢ (\{⟨M, a⟩\} : \{M\} ⟶ \{a\} \land \{a\} \subseteq A) \to \{⟨M, a⟩\} : \{M\} ⟶ A$
22	19 20 21	sylancr	$⊢ a \in A \to \{⟨M, a⟩\} : \{M\} ⟶ A$
23		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
24	2 23	ax-mp	$⊢ (M \dots M) = \{M\}$
25	24	feq2i	$⊢ \{⟨M, a⟩\} : (M \dots M) ⟶ A \leftrightarrow \{⟨M, a⟩\} : \{M\} ⟶ A$
26	22 25	sylibr	$⊢ a \in A \to \{⟨M, a⟩\} : (M \dots M) ⟶ A$
27	26	adantr	$⊢ (a \in A \land θ) \to \{⟨M, a⟩\} : (M \dots M) ⟶ A$
28	16 17	fvsn	$⊢ \{⟨M, a⟩\} (M) = a$
29	28	a1i	$⊢ (a \in A \land θ) \to \{⟨M, a⟩\} (M) = a$
30		simpr	$⊢ (a \in A \land θ) \to θ$
31		snex	$⊢ \{⟨M, a⟩\} \in V$
32		feq1	$⊢ f = \{⟨M, a⟩\} \to (f : (M \dots M) ⟶ A \leftrightarrow \{⟨M, a⟩\} : (M \dots M) ⟶ A)$
33		fveq1	$⊢ f = \{⟨M, a⟩\} \to f (M) = \{⟨M, a⟩\} (M)$
34	33	eqeq1d	$⊢ f = \{⟨M, a⟩\} \to (f (M) = a \leftrightarrow \{⟨M, a⟩\} (M) = a)$
35	33 28	eqtrdi	$⊢ f = \{⟨M, a⟩\} \to f (M) = a$
36		sbceq2a	$⊢ f (M) = a \to (\underset{˙}{[} f (M) / a \underset{˙}{]} θ \leftrightarrow θ)$
37	35 36	syl	$⊢ f = \{⟨M, a⟩\} \to (\underset{˙}{[} f (M) / a \underset{˙}{]} θ \leftrightarrow θ)$
38	34 37	anbi12d	$⊢ f = \{⟨M, a⟩\} \to ((f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ) \leftrightarrow (\{⟨M, a⟩\} (M) = a \land θ))$
39	32 38	anbi12d	$⊢ f = \{⟨M, a⟩\} \to ((f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ)) \leftrightarrow (\{⟨M, a⟩\} : (M \dots M) ⟶ A \land (\{⟨M, a⟩\} (M) = a \land θ)))$
40	31 39	spcev	$⊢ (\{⟨M, a⟩\} : (M \dots M) ⟶ A \land (\{⟨M, a⟩\} (M) = a \land θ)) \to \exists f (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ))$
41	27 29 30 40	syl12anc	$⊢ (a \in A \land θ) \to \exists f (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ))$
42		oveq2	$⊢ n = M \to (M \dots n) = (M \dots M)$
43	42	feq2d	$⊢ n = M \to (f : (M \dots n) ⟶ A \leftrightarrow f : (M \dots M) ⟶ A)$
44		fvex	$⊢ f (n) \in V$
45	44 7	sbcie	$⊢ \underset{˙}{[} f (n) / a \underset{˙}{]} θ \leftrightarrow τ$
46		fveq2	$⊢ n = M \to f (n) = f (M)$
47	46	sbceq1d	$⊢ n = M \to (\underset{˙}{[} f (n) / a \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} f (M) / a \underset{˙}{]} θ)$
48	45 47	bitr3id	$⊢ n = M \to (τ \leftrightarrow \underset{˙}{[} f (M) / a \underset{˙}{]} θ)$
49	48	anbi2d	$⊢ n = M \to ((f (M) = a \land τ) \leftrightarrow (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ))$
50		oveq2	$⊢ n = M \to (N \dots n) = (N \dots M)$
51	4	oveq1i	$⊢ (N \dots M) = (M + 1 \dots M)$
52	2	zrei	$⊢ M \in ℝ$
53	52	ltp1i	$⊢ M < M + 1$
54		peano2z	$⊢ M \in ℤ \to M + 1 \in ℤ$
55	2 54	ax-mp	$⊢ M + 1 \in ℤ$
56		fzn	$⊢ (M + 1 \in ℤ \land M \in ℤ) \to (M < M + 1 \leftrightarrow (M + 1 \dots M) = \emptyset)$
57	55 2 56	mp2an	$⊢ M < M + 1 \leftrightarrow (M + 1 \dots M) = \emptyset$
58	53 57	mpbi	$⊢ (M + 1 \dots M) = \emptyset$
59	51 58	eqtri	$⊢ (N \dots M) = \emptyset$
60	50 59	eqtrdi	$⊢ n = M \to (N \dots n) = \emptyset$
61	60	raleqdv	$⊢ n = M \to (\forall k \in (N \dots n) χ \leftrightarrow \forall k \in \emptyset χ)$
62	43 49 61	3anbi123d	$⊢ n = M \to ((f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ) \land \forall k \in \emptyset χ))$
63		ral0	$⊢ \forall k \in \emptyset χ$
64		df-3an	$⊢ (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ) \land \forall k \in \emptyset χ) \leftrightarrow ((f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ)) \land \forall k \in \emptyset χ)$
65	63 64	mpbiran2	$⊢ (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ) \land \forall k \in \emptyset χ) \leftrightarrow (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ))$
66	62 65	bitrdi	$⊢ n = M \to ((f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ)))$
67	66	exbidv	$⊢ n = M \to (\exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists f (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ)))$
68	67	rspcev	$⊢ (M \in Z \land \exists f (f : (M \dots M) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (M) / a \underset{˙}{]} θ))) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ)$
69	14 41 68	sylancr	$⊢ (a \in A \land θ) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ)$
70	69	adantll	$⊢ ((η \land a \in A) \land θ) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ)$
71	70	a1d	$⊢ ((η \land a \in A) \land θ) \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
72		breq1	$⊢ d = b \to (d R a \leftrightarrow b R a)$
73	72	rspcev	$⊢ (b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \land b R a) \to \exists d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) d R a$
74	73	expcom	$⊢ b R a \to (b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \to \exists d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) d R a)$
75	11 74	syl	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to (b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \to \exists d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) d R a)$
76		dfrex2	$⊢ \exists d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) d R a \leftrightarrow \neg \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a$
77	75 76	imbitrdi	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to (b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \to \neg \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a)$
78	77	con2d	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to \neg b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}))$
79		eldif	$⊢ b \in (A ∖ (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})) \leftrightarrow (b \in A \land \neg b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}))$
80	79	simplbi2	$⊢ b \in A \to (\neg b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \to b \in (A ∖ (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})))$
81		ssrab2	$⊢ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \subseteq A$
82		dfss4	$⊢ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \subseteq A \leftrightarrow A ∖ (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) = \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}$
83	81 82	mpbi	$⊢ A ∖ (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) = \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}$
84	83	eleq2i	$⊢ b \in (A ∖ (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})) \leftrightarrow b \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}$
85		eqeq2	$⊢ c = b \to (f (M) = c \leftrightarrow f (M) = b)$
86	85	anbi1d	$⊢ c = b \to ((f (M) = c \land τ) \leftrightarrow (f (M) = b \land τ))$
87	86	3anbi2d	$⊢ c = b \to ((f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ))$
88	87	exbidv	$⊢ c = b \to (\exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ))$
89	88	rexbidv	$⊢ c = b \to (\exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ))$
90	89	elrab3	$⊢ b \in A \to (b \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \leftrightarrow \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ))$
91	84 90	bitrid	$⊢ b \in A \to (b \in (A ∖ (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})) \leftrightarrow \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ))$
92	80 91	sylibd	$⊢ b \in A \to (\neg b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ))$
93	92	ad2antll	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to (\neg b \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ))$
94		oveq2	$⊢ n = m \to (M \dots n) = (M \dots m)$
95	94	feq2d	$⊢ n = m \to (f : (M \dots n) ⟶ A \leftrightarrow f : (M \dots m) ⟶ A)$
96		fveq2	$⊢ n = m \to f (n) = f (m)$
97	96	sbceq1d	$⊢ n = m \to (\underset{˙}{[} f (n) / a \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} f (m) / a \underset{˙}{]} θ)$
98	45 97	bitr3id	$⊢ n = m \to (τ \leftrightarrow \underset{˙}{[} f (m) / a \underset{˙}{]} θ)$
99	98	anbi2d	$⊢ n = m \to ((f (M) = b \land τ) \leftrightarrow (f (M) = b \land \underset{˙}{[} f (m) / a \underset{˙}{]} θ))$
100		oveq2	$⊢ n = m \to (N \dots n) = (N \dots m)$
101	100	raleqdv	$⊢ n = m \to (\forall k \in (N \dots n) χ \leftrightarrow \forall k \in (N \dots m) χ)$
102	95 99 101	3anbi123d	$⊢ n = m \to ((f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow (f : (M \dots m) ⟶ A \land (f (M) = b \land \underset{˙}{[} f (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) χ))$
103	102	exbidv	$⊢ n = m \to (\exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists f (f : (M \dots m) ⟶ A \land (f (M) = b \land \underset{˙}{[} f (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) χ))$
104	103	cbvrexvw	$⊢ \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists m \in Z \exists f (f : (M \dots m) ⟶ A \land (f (M) = b \land \underset{˙}{[} f (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) χ)$
105		feq1	$⊢ f = g \to (f : (M \dots m) ⟶ A \leftrightarrow g : (M \dots m) ⟶ A)$
106		fveq1	$⊢ f = g \to f (M) = g (M)$
107	106	eqeq1d	$⊢ f = g \to (f (M) = b \leftrightarrow g (M) = b)$
108		fveq1	$⊢ f = g \to f (m) = g (m)$
109	108	sbceq1d	$⊢ f = g \to (\underset{˙}{[} f (m) / a \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} g (m) / a \underset{˙}{]} θ)$
110	107 109	anbi12d	$⊢ f = g \to ((f (M) = b \land \underset{˙}{[} f (m) / a \underset{˙}{]} θ) \leftrightarrow (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ))$
111		fvex	$⊢ f (k - 1) \in V$
112	5	sbcbidv	$⊢ a = f (k - 1) \to (\underset{˙}{[} f (k) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} f (k) / b \underset{˙}{]} ψ)$
113	111 112	sbcie	$⊢ \underset{˙}{[} f (k - 1) / a \underset{˙}{]} \underset{˙}{[} f (k) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} f (k) / b \underset{˙}{]} ψ$
114		fvex	$⊢ f (k) \in V$
115	114 6	sbcie	$⊢ \underset{˙}{[} f (k) / b \underset{˙}{]} ψ \leftrightarrow χ$
116	113 115	bitri	$⊢ \underset{˙}{[} f (k - 1) / a \underset{˙}{]} \underset{˙}{[} f (k) / b \underset{˙}{]} φ \leftrightarrow χ$
117		fveq1	$⊢ f = g \to f (k - 1) = g (k - 1)$
118		fveq1	$⊢ f = g \to f (k) = g (k)$
119	118	sbceq1d	$⊢ f = g \to (\underset{˙}{[} f (k) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} g (k) / b \underset{˙}{]} φ)$
120	117 119	sbceqbid	$⊢ f = g \to (\underset{˙}{[} f (k - 1) / a \underset{˙}{]} \underset{˙}{[} f (k) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)$
121	116 120	bitr3id	$⊢ f = g \to (χ \leftrightarrow \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)$
122	121	ralbidv	$⊢ f = g \to (\forall k \in (N \dots m) χ \leftrightarrow \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)$
123	105 110 122	3anbi123d	$⊢ f = g \to ((f : (M \dots m) ⟶ A \land (f (M) = b \land \underset{˙}{[} f (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) χ) \leftrightarrow (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ))$
124	123	cbvexvw	$⊢ \exists f (f : (M \dots m) ⟶ A \land (f (M) = b \land \underset{˙}{[} f (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) χ) \leftrightarrow \exists g (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)$
125	124	rexbii	$⊢ \exists m \in Z \exists f (f : (M \dots m) ⟶ A \land (f (M) = b \land \underset{˙}{[} f (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) χ) \leftrightarrow \exists m \in Z \exists g (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)$
126	104 125	bitri	$⊢ \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists m \in Z \exists g (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)$
127	3	peano2uzs	$⊢ m \in Z \to m + 1 \in Z$
128	127	ad2antlr	$⊢ ((((η \land φ) \land (a \in A \land b \in A)) \land m \in Z) \land (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to m + 1 \in Z$
129		sbceq2a	$⊢ d = b \to (\underset{˙}{[} d / b \underset{˙}{]} φ \leftrightarrow φ)$
130	129	anbi1d	$⊢ d = b \to ((\underset{˙}{[} d / b \underset{˙}{]} φ \land a \in A) \leftrightarrow (φ \land a \in A))$
131	130	anbi1d	$⊢ d = b \to (((\underset{˙}{[} d / b \underset{˙}{]} φ \land a \in A) \land m \in Z) \leftrightarrow ((φ \land a \in A) \land m \in Z))$
132		eqeq2	$⊢ d = b \to (g (M) = d \leftrightarrow g (M) = b)$
133	132	anbi1d	$⊢ d = b \to ((g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \leftrightarrow (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ))$
134	133	3anbi2d	$⊢ d = b \to ((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \leftrightarrow (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ))$
135	134	imbi1d	$⊢ d = b \to (((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ)) \leftrightarrow ((g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ)))$
136	131 135	imbi12d	$⊢ d = b \to ((((\underset{˙}{[} d / b \underset{˙}{]} φ \land a \in A) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))) \leftrightarrow (((φ \land a \in A) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))))$
137		sbceq2a	$⊢ c = a \to (\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} d / b \underset{˙}{]} φ)$
138		eleq1	$⊢ c = a \to (c \in A \leftrightarrow a \in A)$
139	137 138	anbi12d	$⊢ c = a \to ((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \leftrightarrow (\underset{˙}{[} d / b \underset{˙}{]} φ \land a \in A))$
140	139	anbi1d	$⊢ c = a \to (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \leftrightarrow ((\underset{˙}{[} d / b \underset{˙}{]} φ \land a \in A) \land m \in Z))$
141		eqeq2	$⊢ c = a \to (f (M) = c \leftrightarrow f (M) = a)$
142	141	anbi1d	$⊢ c = a \to ((f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \leftrightarrow (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ))$
143	142	3anbi2d	$⊢ c = a \to ((f : (M \dots m + 1) ⟶ A \land (f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ) \leftrightarrow (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
144	143	exbidv	$⊢ c = a \to (\exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ) \leftrightarrow \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
145	144	imbi2d	$⊢ c = a \to (((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ)) \leftrightarrow ((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ)))$
146	140 145	imbi12d	$⊢ c = a \to ((((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))) \leftrightarrow (((\underset{˙}{[} d / b \underset{˙}{]} φ \land a \in A) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))))$
147		peano2uz	$⊢ m \in ℤ_{\geq M} \to m + 1 \in ℤ_{\geq M}$
148	147 3	eleq2s	$⊢ m \in Z \to m + 1 \in ℤ_{\geq M}$
149		elfzp12	$⊢ m + 1 \in ℤ_{\geq M} \to (x \in (M \dots m + 1) \leftrightarrow (x = M \lor x \in (M + 1 \dots m + 1)))$
150	148 149	syl	$⊢ m \in Z \to (x \in (M \dots m + 1) \leftrightarrow (x = M \lor x \in (M + 1 \dots m + 1)))$
151	150	ad2antlr	$⊢ ((c \in A \land m \in Z) \land g : (M \dots m) ⟶ A) \to (x \in (M \dots m + 1) \leftrightarrow (x = M \lor x \in (M + 1 \dots m + 1)))$
152		iftrue	$⊢ x = M \to if (x = M, c, g (x - 1)) = c$
153	152	eleq1d	$⊢ x = M \to (if (x = M, c, g (x - 1)) \in A \leftrightarrow c \in A)$
154	153	biimprcd	$⊢ c \in A \to (x = M \to if (x = M, c, g (x - 1)) \in A)$
155	154	ad2antrr	$⊢ ((c \in A \land m \in Z) \land g : (M \dots m) ⟶ A) \to (x = M \to if (x = M, c, g (x - 1)) \in A)$
156		1re	$⊢ 1 \in ℝ$
157	52 156	readdcli	$⊢ M + 1 \in ℝ$
158	52 157	ltnlei	$⊢ M < M + 1 \leftrightarrow \neg M + 1 \leq M$
159	53 158	mpbi	$⊢ \neg M + 1 \leq M$
160		eleq1	$⊢ x = M \to (x \in (M + 1 \dots m + 1) \leftrightarrow M \in (M + 1 \dots m + 1))$
161		elfzle1	$⊢ M \in (M + 1 \dots m + 1) \to M + 1 \leq M$
162	160 161	biimtrdi	$⊢ x = M \to (x \in (M + 1 \dots m + 1) \to M + 1 \leq M)$
163	162	com12	$⊢ x \in (M + 1 \dots m + 1) \to (x = M \to M + 1 \leq M)$
164	159 163	mtoi	$⊢ x \in (M + 1 \dots m + 1) \to \neg x = M$
165	164	adantl	$⊢ ((m \in Z \land g : (M \dots m) ⟶ A) \land x \in (M + 1 \dots m + 1)) \to \neg x = M$
166	165	iffalsed	$⊢ ((m \in Z \land g : (M \dots m) ⟶ A) \land x \in (M + 1 \dots m + 1)) \to if (x = M, c, g (x - 1)) = g (x - 1)$
167		elfzelz	$⊢ x \in (M + 1 \dots m + 1) \to x \in ℤ$
168	167	adantl	$⊢ (m \in Z \land x \in (M + 1 \dots m + 1)) \to x \in ℤ$
169		eluzelz	$⊢ m \in ℤ_{\geq M} \to m \in ℤ$
170	169 3	eleq2s	$⊢ m \in Z \to m \in ℤ$
171	170	peano2zd	$⊢ m \in Z \to m + 1 \in ℤ$
172		1z	$⊢ 1 \in ℤ$
173		fzsubel	$⊢ ((M + 1 \in ℤ \land m + 1 \in ℤ) \land (x \in ℤ \land 1 \in ℤ)) \to (x \in (M + 1 \dots m + 1) \leftrightarrow x - 1 \in (M + 1 - 1 \dots m + 1 - 1))$
174	173	biimpd	$⊢ ((M + 1 \in ℤ \land m + 1 \in ℤ) \land (x \in ℤ \land 1 \in ℤ)) \to (x \in (M + 1 \dots m + 1) \to x - 1 \in (M + 1 - 1 \dots m + 1 - 1))$
175	172 174	mpanr2	$⊢ ((M + 1 \in ℤ \land m + 1 \in ℤ) \land x \in ℤ) \to (x \in (M + 1 \dots m + 1) \to x - 1 \in (M + 1 - 1 \dots m + 1 - 1))$
176	55 175	mpanl1	$⊢ (m + 1 \in ℤ \land x \in ℤ) \to (x \in (M + 1 \dots m + 1) \to x - 1 \in (M + 1 - 1 \dots m + 1 - 1))$
177	176	ex	$⊢ m + 1 \in ℤ \to (x \in ℤ \to (x \in (M + 1 \dots m + 1) \to x - 1 \in (M + 1 - 1 \dots m + 1 - 1)))$
178	171 177	syl	$⊢ m \in Z \to (x \in ℤ \to (x \in (M + 1 \dots m + 1) \to x - 1 \in (M + 1 - 1 \dots m + 1 - 1)))$
179	178	com23	$⊢ m \in Z \to (x \in (M + 1 \dots m + 1) \to (x \in ℤ \to x - 1 \in (M + 1 - 1 \dots m + 1 - 1)))$
180	179	imp	$⊢ (m \in Z \land x \in (M + 1 \dots m + 1)) \to (x \in ℤ \to x - 1 \in (M + 1 - 1 \dots m + 1 - 1))$
181	168 180	mpd	$⊢ (m \in Z \land x \in (M + 1 \dots m + 1)) \to x - 1 \in (M + 1 - 1 \dots m + 1 - 1)$
182	52	recni	$⊢ M \in ℂ$
183		ax-1cn	$⊢ 1 \in ℂ$
184	182 183	pncan3oi	$⊢ M + 1 - 1 = M$
185	184	a1i	$⊢ m \in Z \to M + 1 - 1 = M$
186	170	zcnd	$⊢ m \in Z \to m \in ℂ$
187		pncan	$⊢ (m \in ℂ \land 1 \in ℂ) \to m + 1 - 1 = m$
188	186 183 187	sylancl	$⊢ m \in Z \to m + 1 - 1 = m$
189	185 188	oveq12d	$⊢ m \in Z \to (M + 1 - 1 \dots m + 1 - 1) = (M \dots m)$
190	189	adantr	$⊢ (m \in Z \land x \in (M + 1 \dots m + 1)) \to (M + 1 - 1 \dots m + 1 - 1) = (M \dots m)$
191	181 190	eleqtrd	$⊢ (m \in Z \land x \in (M + 1 \dots m + 1)) \to x - 1 \in (M \dots m)$
192		ffvelcdm	$⊢ (g : (M \dots m) ⟶ A \land x - 1 \in (M \dots m)) \to g (x - 1) \in A$
193	191 192	sylan2	$⊢ (g : (M \dots m) ⟶ A \land (m \in Z \land x \in (M + 1 \dots m + 1))) \to g (x - 1) \in A$
194	193	anassrs	$⊢ ((g : (M \dots m) ⟶ A \land m \in Z) \land x \in (M + 1 \dots m + 1)) \to g (x - 1) \in A$
195	194	ancom1s	$⊢ ((m \in Z \land g : (M \dots m) ⟶ A) \land x \in (M + 1 \dots m + 1)) \to g (x - 1) \in A$
196	166 195	eqeltrd	$⊢ ((m \in Z \land g : (M \dots m) ⟶ A) \land x \in (M + 1 \dots m + 1)) \to if (x = M, c, g (x - 1)) \in A$
197	196	ex	$⊢ (m \in Z \land g : (M \dots m) ⟶ A) \to (x \in (M + 1 \dots m + 1) \to if (x = M, c, g (x - 1)) \in A)$
198	197	adantll	$⊢ ((c \in A \land m \in Z) \land g : (M \dots m) ⟶ A) \to (x \in (M + 1 \dots m + 1) \to if (x = M, c, g (x - 1)) \in A)$
199	155 198	jaod	$⊢ ((c \in A \land m \in Z) \land g : (M \dots m) ⟶ A) \to ((x = M \lor x \in (M + 1 \dots m + 1)) \to if (x = M, c, g (x - 1)) \in A)$
200	151 199	sylbid	$⊢ ((c \in A \land m \in Z) \land g : (M \dots m) ⟶ A) \to (x \in (M \dots m + 1) \to if (x = M, c, g (x - 1)) \in A)$
201	200	ralrimiv	$⊢ ((c \in A \land m \in Z) \land g : (M \dots m) ⟶ A) \to \forall x \in (M \dots m + 1) if (x = M, c, g (x - 1)) \in A$
202		eqid	$⊢ (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1)))$
203	202	fmpt	$⊢ \forall x \in (M \dots m + 1) if (x = M, c, g (x - 1)) \in A \leftrightarrow (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) : (M \dots m + 1) ⟶ A$
204	201 203	sylib	$⊢ ((c \in A \land m \in Z) \land g : (M \dots m) ⟶ A) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) : (M \dots m + 1) ⟶ A$
205	204	adantlll	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land g : (M \dots m) ⟶ A) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) : (M \dots m + 1) ⟶ A$
206	205	3ad2antr1	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land (g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) : (M \dots m + 1) ⟶ A$
207		eluzfz1	$⊢ m + 1 \in ℤ_{\geq M} \to M \in (M \dots m + 1)$
208	147 207	syl	$⊢ m \in ℤ_{\geq M} \to M \in (M \dots m + 1)$
209	208 3	eleq2s	$⊢ m \in Z \to M \in (M \dots m + 1)$
210		vex	$⊢ c \in V$
211	152 202 210	fvmpt	$⊢ M \in (M \dots m + 1) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M) = c$
212	209 211	syl	$⊢ m \in Z \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M) = c$
213	212	ad2antlr	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land (g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M) = c$
214		eluzfz2	$⊢ m + 1 \in ℤ_{\geq M} \to m + 1 \in (M \dots m + 1)$
215	147 214	syl	$⊢ m \in ℤ_{\geq M} \to m + 1 \in (M \dots m + 1)$
216	215 3	eleq2s	$⊢ m \in Z \to m + 1 \in (M \dots m + 1)$
217		eqeq1	$⊢ x = m + 1 \to (x = M \leftrightarrow m + 1 = M)$
218		fvoveq1	$⊢ x = m + 1 \to g (x - 1) = g (m + 1 - 1)$
219	217 218	ifbieq2d	$⊢ x = m + 1 \to if (x = M, c, g (x - 1)) = if (m + 1 = M, c, g (m + 1 - 1))$
220		fvex	$⊢ g (m + 1 - 1) \in V$
221	210 220	ifex	$⊢ if (m + 1 = M, c, g (m + 1 - 1)) \in V$
222	219 202 221	fvmpt	$⊢ m + 1 \in (M \dots m + 1) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) = if (m + 1 = M, c, g (m + 1 - 1))$
223	216 222	syl	$⊢ m \in Z \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) = if (m + 1 = M, c, g (m + 1 - 1))$
224		eluzle	$⊢ m \in ℤ_{\geq M} \to M \leq m$
225	224 3	eleq2s	$⊢ m \in Z \to M \leq m$
226		zleltp1	$⊢ (M \in ℤ \land m \in ℤ) \to (M \leq m \leftrightarrow M < m + 1)$
227	2 170 226	sylancr	$⊢ m \in Z \to (M \leq m \leftrightarrow M < m + 1)$
228	225 227	mpbid	$⊢ m \in Z \to M < m + 1$
229		ltne	$⊢ (M \in ℝ \land M < m + 1) \to m + 1 \neq M$
230	52 228 229	sylancr	$⊢ m \in Z \to m + 1 \neq M$
231	230	neneqd	$⊢ m \in Z \to \neg m + 1 = M$
232	231	iffalsed	$⊢ m \in Z \to if (m + 1 = M, c, g (m + 1 - 1)) = g (m + 1 - 1)$
233	188	fveq2d	$⊢ m \in Z \to g (m + 1 - 1) = g (m)$
234	223 232 233	3eqtrd	$⊢ m \in Z \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) = g (m)$
235	234	sbceq1d	$⊢ m \in Z \to (\underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) / a \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} g (m) / a \underset{˙}{]} θ)$
236	235	biimpar	$⊢ (m \in Z \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) / a \underset{˙}{]} θ$
237	236	ad2ant2l	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ)) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) / a \underset{˙}{]} θ$
238	237	3ad2antr2	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land (g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) / a \underset{˙}{]} θ$
239		eluzp1p1	$⊢ m \in ℤ_{\geq M} \to m + 1 \in ℤ_{\geq (M + 1)}$
240	239 3	eleq2s	$⊢ m \in Z \to m + 1 \in ℤ_{\geq (M + 1)}$
241	4	fveq2i	$⊢ ℤ_{\geq N} = ℤ_{\geq (M + 1)}$
242	240 241	eleqtrrdi	$⊢ m \in Z \to m + 1 \in ℤ_{\geq N}$
243		elfzp12	$⊢ m + 1 \in ℤ_{\geq N} \to (j \in (N \dots m + 1) \leftrightarrow (j = N \lor j \in (N + 1 \dots m + 1)))$
244	242 243	syl	$⊢ m \in Z \to (j \in (N \dots m + 1) \leftrightarrow (j = N \lor j \in (N + 1 \dots m + 1)))$
245	244	biimpa	$⊢ (m \in Z \land j \in (N \dots m + 1)) \to (j = N \lor j \in (N + 1 \dots m + 1))$
246	245	adantll	$⊢ ((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land j \in (N \dots m + 1)) \to (j = N \lor j \in (N + 1 \dots m + 1))$
247	246	adantlr	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \land j \in (N \dots m + 1)) \to (j = N \lor j \in (N + 1 \dots m + 1))$
248		oveq1	$⊢ j = N \to j - 1 = N - 1$
249	4	oveq1i	$⊢ N - 1 = M + 1 - 1$
250	249 184	eqtri	$⊢ N - 1 = M$
251	248 250	eqtrdi	$⊢ j = N \to j - 1 = M$
252	251	fveq2d	$⊢ j = N \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M)$
253	252	ad2antll	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M)$
254	212	adantr	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M) = c$
255	253 254	eqtrd	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) = c$
256	4	eqeq2i	$⊢ j = N \leftrightarrow j = M + 1$
257		fveq2	$⊢ j = M + 1 \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M + 1)$
258	256 257	sylbi	$⊢ j = N \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M + 1)$
259	258	ad2antll	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M + 1)$
260	52 157 53	ltleii	$⊢ M \leq M + 1$
261		eluz2	$⊢ M + 1 \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land M + 1 \in ℤ \land M \leq M + 1)$
262	2 55 260 261	mpbir3an	$⊢ M + 1 \in ℤ_{\geq M}$
263		fzss1	$⊢ M + 1 \in ℤ_{\geq M} \to (M + 1 \dots m + 1) \subseteq (M \dots m + 1)$
264	262 263	ax-mp	$⊢ (M + 1 \dots m + 1) \subseteq (M \dots m + 1)$
265		eluzfz1	$⊢ m \in ℤ_{\geq M} \to M \in (M \dots m)$
266	265 3	eleq2s	$⊢ m \in Z \to M \in (M \dots m)$
267		fzaddel	$⊢ ((M \in ℤ \land m \in ℤ) \land (M \in ℤ \land 1 \in ℤ)) \to (M \in (M \dots m) \leftrightarrow M + 1 \in (M + 1 \dots m + 1))$
268	2 172 267	mpanr12	$⊢ (M \in ℤ \land m \in ℤ) \to (M \in (M \dots m) \leftrightarrow M + 1 \in (M + 1 \dots m + 1))$
269	2 170 268	sylancr	$⊢ m \in Z \to (M \in (M \dots m) \leftrightarrow M + 1 \in (M + 1 \dots m + 1))$
270	266 269	mpbid	$⊢ m \in Z \to M + 1 \in (M + 1 \dots m + 1)$
271	264 270	sselid	$⊢ m \in Z \to M + 1 \in (M \dots m + 1)$
272		eqeq1	$⊢ x = M + 1 \to (x = M \leftrightarrow M + 1 = M)$
273		oveq1	$⊢ x = M + 1 \to x - 1 = M + 1 - 1$
274	273 184	eqtrdi	$⊢ x = M + 1 \to x - 1 = M$
275	274	fveq2d	$⊢ x = M + 1 \to g (x - 1) = g (M)$
276	272 275	ifbieq2d	$⊢ x = M + 1 \to if (x = M, c, g (x - 1)) = if (M + 1 = M, c, g (M))$
277		fvex	$⊢ g (M) \in V$
278	210 277	ifex	$⊢ if (M + 1 = M, c, g (M)) \in V$
279	276 202 278	fvmpt	$⊢ M + 1 \in (M \dots m + 1) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M + 1) = if (M + 1 = M, c, g (M))$
280	271 279	syl	$⊢ m \in Z \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M + 1) = if (M + 1 = M, c, g (M))$
281	52 53	gtneii	$⊢ M + 1 \neq M$
282		ifnefalse	$⊢ M + 1 \neq M \to if (M + 1 = M, c, g (M)) = g (M)$
283	281 282	ax-mp	$⊢ if (M + 1 = M, c, g (M)) = g (M)$
284	280 283	eqtrdi	$⊢ m \in Z \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M + 1) = g (M)$
285	284	adantr	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M + 1) = g (M)$
286		simprl	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to g (M) = d$
287	259 285 286	3eqtrd	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) = d$
288	287	sbceq1d	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to (\underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} d / b \underset{˙}{]} φ)$
289	255 288	sbceqbid	$⊢ (m \in Z \land (g (M) = d \land j = N)) \to (\underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ)$
290	289	biimparc	$⊢ (\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land (m \in Z \land (g (M) = d \land j = N))) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
291	290	anassrs	$⊢ ((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land (g (M) = d \land j = N)) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
292	291	anassrs	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land g (M) = d) \land j = N) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
293	292	adantlrr	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \land j = N) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
294		elfzelz	$⊢ j \in (N + 1 \dots m + 1) \to j \in ℤ$
295	294	adantl	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to j \in ℤ$
296	4 55	eqeltri	$⊢ N \in ℤ$
297		peano2z	$⊢ N \in ℤ \to N + 1 \in ℤ$
298	296 297	ax-mp	$⊢ N + 1 \in ℤ$
299		fzsubel	$⊢ ((N + 1 \in ℤ \land m + 1 \in ℤ) \land (j \in ℤ \land 1 \in ℤ)) \to (j \in (N + 1 \dots m + 1) \leftrightarrow j - 1 \in (N + 1 - 1 \dots m + 1 - 1))$
300	299	biimpd	$⊢ ((N + 1 \in ℤ \land m + 1 \in ℤ) \land (j \in ℤ \land 1 \in ℤ)) \to (j \in (N + 1 \dots m + 1) \to j - 1 \in (N + 1 - 1 \dots m + 1 - 1))$
301	172 300	mpanr2	$⊢ ((N + 1 \in ℤ \land m + 1 \in ℤ) \land j \in ℤ) \to (j \in (N + 1 \dots m + 1) \to j - 1 \in (N + 1 - 1 \dots m + 1 - 1))$
302	301	ex	$⊢ (N + 1 \in ℤ \land m + 1 \in ℤ) \to (j \in ℤ \to (j \in (N + 1 \dots m + 1) \to j - 1 \in (N + 1 - 1 \dots m + 1 - 1)))$
303	298 171 302	sylancr	$⊢ m \in Z \to (j \in ℤ \to (j \in (N + 1 \dots m + 1) \to j - 1 \in (N + 1 - 1 \dots m + 1 - 1)))$
304	303	com23	$⊢ m \in Z \to (j \in (N + 1 \dots m + 1) \to (j \in ℤ \to j - 1 \in (N + 1 - 1 \dots m + 1 - 1)))$
305	304	imp	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to (j \in ℤ \to j - 1 \in (N + 1 - 1 \dots m + 1 - 1))$
306	295 305	mpd	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to j - 1 \in (N + 1 - 1 \dots m + 1 - 1)$
307	296	zrei	$⊢ N \in ℝ$
308	307	recni	$⊢ N \in ℂ$
309	308 183	pncan3oi	$⊢ N + 1 - 1 = N$
310	309	a1i	$⊢ m \in Z \to N + 1 - 1 = N$
311	310 188	oveq12d	$⊢ m \in Z \to (N + 1 - 1 \dots m + 1 - 1) = (N \dots m)$
312	311	adantr	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to (N + 1 - 1 \dots m + 1 - 1) = (N \dots m)$
313	306 312	eleqtrd	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to j - 1 \in (N \dots m)$
314		fvoveq1	$⊢ k = j - 1 \to g (k - 1) = g (j - 1 - 1)$
315		fveq2	$⊢ k = j - 1 \to g (k) = g (j - 1)$
316	315	sbceq1d	$⊢ k = j - 1 \to (\underset{˙}{[} g (k) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} g (j - 1) / b \underset{˙}{]} φ)$
317	314 316	sbceqbid	$⊢ k = j - 1 \to (\underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} g (j - 1 - 1) / a \underset{˙}{]} \underset{˙}{[} g (j - 1) / b \underset{˙}{]} φ)$
318	317	rspcva	$⊢ (j - 1 \in (N \dots m) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \underset{˙}{[} g (j - 1 - 1) / a \underset{˙}{]} \underset{˙}{[} g (j - 1) / b \underset{˙}{]} φ$
319	313 318	sylan	$⊢ ((m \in Z \land j \in (N + 1 \dots m + 1)) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \underset{˙}{[} g (j - 1 - 1) / a \underset{˙}{]} \underset{˙}{[} g (j - 1) / b \underset{˙}{]} φ$
320	4 262	eqeltri	$⊢ N \in ℤ_{\geq M}$
321		fzss1	$⊢ N \in ℤ_{\geq M} \to (N \dots m + 1) \subseteq (M \dots m + 1)$
322	320 321	ax-mp	$⊢ (N \dots m + 1) \subseteq (M \dots m + 1)$
323		fzssp1	$⊢ (N \dots m) \subseteq (N \dots m + 1)$
324	323 313	sselid	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to j - 1 \in (N \dots m + 1)$
325	322 324	sselid	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to j - 1 \in (M \dots m + 1)$
326		eqeq1	$⊢ x = j - 1 \to (x = M \leftrightarrow j - 1 = M)$
327		fvoveq1	$⊢ x = j - 1 \to g (x - 1) = g (j - 1 - 1)$
328	326 327	ifbieq2d	$⊢ x = j - 1 \to if (x = M, c, g (x - 1)) = if (j - 1 = M, c, g (j - 1 - 1))$
329		fvex	$⊢ g (j - 1 - 1) \in V$
330	210 329	ifex	$⊢ if (j - 1 = M, c, g (j - 1 - 1)) \in V$
331	328 202 330	fvmpt	$⊢ j - 1 \in (M \dots m + 1) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) = if (j - 1 = M, c, g (j - 1 - 1))$
332	325 331	syl	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) = if (j - 1 = M, c, g (j - 1 - 1))$
333	157	ltp1i	$⊢ M + 1 < M + 1 + 1$
334	4	oveq1i	$⊢ N + 1 = M + 1 + 1$
335	333 334	breqtrri	$⊢ M + 1 < N + 1$
336	307 156	readdcli	$⊢ N + 1 \in ℝ$
337	157 336	ltnlei	$⊢ M + 1 < N + 1 \leftrightarrow \neg N + 1 \leq M + 1$
338	335 337	mpbi	$⊢ \neg N + 1 \leq M + 1$
339	294	zcnd	$⊢ j \in (N + 1 \dots m + 1) \to j \in ℂ$
340		subadd	$⊢ (j \in ℂ \land 1 \in ℂ \land M \in ℂ) \to (j - 1 = M \leftrightarrow 1 + M = j)$
341	183 182 340	mp3an23	$⊢ j \in ℂ \to (j - 1 = M \leftrightarrow 1 + M = j)$
342	339 341	syl	$⊢ j \in (N + 1 \dots m + 1) \to (j - 1 = M \leftrightarrow 1 + M = j)$
343		eqcom	$⊢ 1 + M = j \leftrightarrow j = 1 + M$
344	183 182	addcomi	$⊢ 1 + M = M + 1$
345	344	eqeq2i	$⊢ j = 1 + M \leftrightarrow j = M + 1$
346	343 345	bitri	$⊢ 1 + M = j \leftrightarrow j = M + 1$
347		eleq1	$⊢ j = M + 1 \to (j \in (N + 1 \dots m + 1) \leftrightarrow M + 1 \in (N + 1 \dots m + 1))$
348		elfzle1	$⊢ M + 1 \in (N + 1 \dots m + 1) \to N + 1 \leq M + 1$
349	347 348	biimtrdi	$⊢ j = M + 1 \to (j \in (N + 1 \dots m + 1) \to N + 1 \leq M + 1)$
350	349	com12	$⊢ j \in (N + 1 \dots m + 1) \to (j = M + 1 \to N + 1 \leq M + 1)$
351	346 350	biimtrid	$⊢ j \in (N + 1 \dots m + 1) \to (1 + M = j \to N + 1 \leq M + 1)$
352	342 351	sylbid	$⊢ j \in (N + 1 \dots m + 1) \to (j - 1 = M \to N + 1 \leq M + 1)$
353	338 352	mtoi	$⊢ j \in (N + 1 \dots m + 1) \to \neg j - 1 = M$
354	353	adantl	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to \neg j - 1 = M$
355	354	iffalsed	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to if (j - 1 = M, c, g (j - 1 - 1)) = g (j - 1 - 1)$
356	332 355	eqtrd	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) = g (j - 1 - 1)$
357		peano2uz	$⊢ N \in ℤ_{\geq M} \to N + 1 \in ℤ_{\geq M}$
358		fzss1	$⊢ N + 1 \in ℤ_{\geq M} \to (N + 1 \dots m + 1) \subseteq (M \dots m + 1)$
359	320 357 358	mp2b	$⊢ (N + 1 \dots m + 1) \subseteq (M \dots m + 1)$
360		simpr	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to j \in (N + 1 \dots m + 1)$
361	359 360	sselid	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to j \in (M \dots m + 1)$
362		eqeq1	$⊢ x = j \to (x = M \leftrightarrow j = M)$
363		fvoveq1	$⊢ x = j \to g (x - 1) = g (j - 1)$
364	362 363	ifbieq2d	$⊢ x = j \to if (x = M, c, g (x - 1)) = if (j = M, c, g (j - 1))$
365		fvex	$⊢ g (j - 1) \in V$
366	210 365	ifex	$⊢ if (j = M, c, g (j - 1)) \in V$
367	364 202 366	fvmpt	$⊢ j \in (M \dots m + 1) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) = if (j = M, c, g (j - 1))$
368	361 367	syl	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) = if (j = M, c, g (j - 1))$
369	53 4	breqtrri	$⊢ M < N$
370	307	ltp1i	$⊢ N < N + 1$
371	52 307 336	lttri	$⊢ (M < N \land N < N + 1) \to M < N + 1$
372	369 370 371	mp2an	$⊢ M < N + 1$
373	52 336	ltnlei	$⊢ M < N + 1 \leftrightarrow \neg N + 1 \leq M$
374	372 373	mpbi	$⊢ \neg N + 1 \leq M$
375		eleq1	$⊢ j = M \to (j \in (N + 1 \dots m + 1) \leftrightarrow M \in (N + 1 \dots m + 1))$
376		elfzle1	$⊢ M \in (N + 1 \dots m + 1) \to N + 1 \leq M$
377	375 376	biimtrdi	$⊢ j = M \to (j \in (N + 1 \dots m + 1) \to N + 1 \leq M)$
378	377	com12	$⊢ j \in (N + 1 \dots m + 1) \to (j = M \to N + 1 \leq M)$
379	374 378	mtoi	$⊢ j \in (N + 1 \dots m + 1) \to \neg j = M$
380	379	adantl	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to \neg j = M$
381	380	iffalsed	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to if (j = M, c, g (j - 1)) = g (j - 1)$
382	368 381	eqtrd	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) = g (j - 1)$
383	382	sbceq1d	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to (\underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} g (j - 1) / b \underset{˙}{]} φ)$
384	356 383	sbceqbid	$⊢ (m \in Z \land j \in (N + 1 \dots m + 1)) \to (\underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} g (j - 1 - 1) / a \underset{˙}{]} \underset{˙}{[} g (j - 1) / b \underset{˙}{]} φ)$
385	384	biimpar	$⊢ ((m \in Z \land j \in (N + 1 \dots m + 1)) \land \underset{˙}{[} g (j - 1 - 1) / a \underset{˙}{]} \underset{˙}{[} g (j - 1) / b \underset{˙}{]} φ) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
386	319 385	syldan	$⊢ ((m \in Z \land j \in (N + 1 \dots m + 1)) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
387	386	an32s	$⊢ ((m \in Z \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \land j \in (N + 1 \dots m + 1)) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
388	387	adantlrl	$⊢ ((m \in Z \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \land j \in (N + 1 \dots m + 1)) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
389	388	adantlll	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \land j \in (N + 1 \dots m + 1)) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
390	293 389	jaodan	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \land (j = N \lor j \in (N + 1 \dots m + 1))) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
391	247 390	syldan	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \land j \in (N \dots m + 1)) \to \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
392	391	ralrimiva	$⊢ ((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \forall j \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ$
393		fvoveq1	$⊢ j = k \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1)$
394		fveq2	$⊢ j = k \to (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k)$
395	394	sbceq1d	$⊢ j = k \to (\underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ)$
396	393 395	sbceqbid	$⊢ j = k \to (\underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ)$
397	396	cbvralvw	$⊢ \forall j \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (j) / b \underset{˙}{]} φ \leftrightarrow \forall k \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ$
398	392 397	sylib	$⊢ ((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land m \in Z) \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \forall k \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ$
399	398	adantllr	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land (g (M) = d \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \forall k \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ$
400	399	adantrlr	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land ((g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \forall k \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ$
401	400	3adantr1	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land (g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \forall k \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ$
402		ovex	$⊢ (M \dots m + 1) \in V$
403	402	mptex	$⊢ (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \in V$
404		feq1	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to (f : (M \dots m + 1) ⟶ A \leftrightarrow (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) : (M \dots m + 1) ⟶ A)$
405		fveq1	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to f (M) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M)$
406	405	eqeq1d	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to (f (M) = c \leftrightarrow (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M) = c)$
407		fveq1	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to f (m + 1) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1)$
408	407	sbceq1d	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to (\underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) / a \underset{˙}{]} θ)$
409	406 408	anbi12d	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to ((f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \leftrightarrow ((x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M) = c \land \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) / a \underset{˙}{]} θ))$
410		fveq1	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to f (k - 1) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1)$
411		fveq1	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to f (k) = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k)$
412	411	sbceq1d	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to (\underset{˙}{[} f (k) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ)$
413	410 412	sbceqbid	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to (\underset{˙}{[} f (k - 1) / a \underset{˙}{]} \underset{˙}{[} f (k) / b \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ)$
414	116 413	bitr3id	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to (χ \leftrightarrow \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ)$
415	414	ralbidv	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to (\forall k \in (N \dots m + 1) χ \leftrightarrow \forall k \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ)$
416	404 409 415	3anbi123d	$⊢ f = (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) \to ((f : (M \dots m + 1) ⟶ A \land (f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ) \leftrightarrow ((x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) : (M \dots m + 1) ⟶ A \land ((x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M) = c \land \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ))$
417	403 416	spcev	$⊢ ((x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) : (M \dots m + 1) ⟶ A \land ((x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (M) = c \land \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k - 1) / a \underset{˙}{]} \underset{˙}{[} (x \in (M \dots m + 1) ⟼ if (x = M, c, g (x - 1))) (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ)$
418	206 213 238 401 417	syl121anc	$⊢ (((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \land (g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ)$
419	418	ex	$⊢ ((\underset{˙}{[} c / a \underset{˙}{]} \underset{˙}{[} d / b \underset{˙}{]} φ \land c \in A) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = c \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
420	146 419	chvarvv	$⊢ ((\underset{˙}{[} d / b \underset{˙}{]} φ \land a \in A) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = d \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
421	136 420	chvarvv	$⊢ ((φ \land a \in A) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
422	421	adantlrr	$⊢ ((φ \land (a \in A \land b \in A)) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
423	422	adantlll	$⊢ (((η \land φ) \land (a \in A \land b \in A)) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
424	423	imp	$⊢ ((((η \land φ) \land (a \in A \land b \in A)) \land m \in Z) \land (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ)$
425		oveq2	$⊢ n = m + 1 \to (M \dots n) = (M \dots m + 1)$
426	425	feq2d	$⊢ n = m + 1 \to (f : (M \dots n) ⟶ A \leftrightarrow f : (M \dots m + 1) ⟶ A)$
427		fveq2	$⊢ n = m + 1 \to f (n) = f (m + 1)$
428	427	sbceq1d	$⊢ n = m + 1 \to (\underset{˙}{[} f (n) / a \underset{˙}{]} θ \leftrightarrow \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ)$
429	45 428	bitr3id	$⊢ n = m + 1 \to (τ \leftrightarrow \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ)$
430	429	anbi2d	$⊢ n = m + 1 \to ((f (M) = a \land τ) \leftrightarrow (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ))$
431		oveq2	$⊢ n = m + 1 \to (N \dots n) = (N \dots m + 1)$
432	431	raleqdv	$⊢ n = m + 1 \to (\forall k \in (N \dots n) χ \leftrightarrow \forall k \in (N \dots m + 1) χ)$
433	426 430 432	3anbi123d	$⊢ n = m + 1 \to ((f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
434	433	exbidv	$⊢ n = m + 1 \to (\exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ))$
435	434	rspcev	$⊢ (m + 1 \in Z \land \exists f (f : (M \dots m + 1) ⟶ A \land (f (M) = a \land \underset{˙}{[} f (m + 1) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m + 1) χ)) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ)$
436	128 424 435	syl2anc	$⊢ ((((η \land φ) \land (a \in A \land b \in A)) \land m \in Z) \land (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ)) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ)$
437	436	ex	$⊢ (((η \land φ) \land (a \in A \land b \in A)) \land m \in Z) \to ((g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
438	437	exlimdv	$⊢ (((η \land φ) \land (a \in A \land b \in A)) \land m \in Z) \to (\exists g (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
439	438	rexlimdva	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to (\exists m \in Z \exists g (g : (M \dots m) ⟶ A \land (g (M) = b \land \underset{˙}{[} g (m) / a \underset{˙}{]} θ) \land \forall k \in (N \dots m) \underset{˙}{[} g (k - 1) / a \underset{˙}{]} \underset{˙}{[} g (k) / b \underset{˙}{]} φ) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
440	126 439	biimtrid	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to (\exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = b \land τ) \land \forall k \in (N \dots n) χ) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
441	78 93 440	3syld	$⊢ ((η \land φ) \land (a \in A \land b \in A)) \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
442	441	an42s	$⊢ ((η \land a \in A) \land (b \in A \land φ)) \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
443	442	rexlimdvaa	$⊢ (η \land a \in A) \to (\exists b \in A φ \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ)))$
444	443	imp	$⊢ ((η \land a \in A) \land \exists b \in A φ) \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
445	71 444 10	mpjaodan	$⊢ (η \land a \in A) \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
446	141	anbi1d	$⊢ c = a \to ((f (M) = c \land τ) \leftrightarrow (f (M) = a \land τ))$
447	446	3anbi2d	$⊢ c = a \to ((f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
448	447	exbidv	$⊢ c = a \to (\exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
449	448	rexbidv	$⊢ c = a \to (\exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
450	449	elrab3	$⊢ a \in A \to (a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \leftrightarrow \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
451	450	adantl	$⊢ (η \land a \in A) \to (a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \leftrightarrow \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = a \land τ) \land \forall k \in (N \dots n) χ))$
452	445 451	sylibrd	$⊢ (η \land a \in A) \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})$
453	452	ex	$⊢ η \to (a \in A \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}))$
454	453	com23	$⊢ η \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to (a \in A \to a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}))$
455		eldif	$⊢ a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \leftrightarrow (a \in A \land \neg a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})$
456	455	notbii	$⊢ \neg a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \leftrightarrow \neg (a \in A \land \neg a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})$
457		iman	$⊢ (a \in A \to a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \leftrightarrow \neg (a \in A \land \neg a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})$
458	456 457	bitr4i	$⊢ \neg a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \leftrightarrow (a \in A \to a \in \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})$
459	454 458	imbitrrdi	$⊢ η \to (\forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a \to \neg a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}))$
460	459	con2d	$⊢ η \to (a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \to \neg \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a)$
461	460	imp	$⊢ (η \land a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\})) \to \neg \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a$
462	461	nrexdv	$⊢ η \to \neg \exists a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a$
463		df-ne	$⊢ A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \neq \emptyset \leftrightarrow \neg A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} = \emptyset$
464		difss	$⊢ A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \subseteq A$
465		difexg	$⊢ A \in V \to A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \in V$
466	1 465	ax-mp	$⊢ A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \in V$
467		fri	$⊢ ((A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \in V \land R Fr A) \land (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \subseteq A \land A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \neq \emptyset)) \to \exists a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a$
468	466 467	mpanl1	$⊢ (R Fr A \land (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \subseteq A \land A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \neq \emptyset)) \to \exists a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a$
469	468	expr	$⊢ (R Fr A \land A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \subseteq A) \to (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \neq \emptyset \to \exists a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a)$
470	9 464 469	sylancl	$⊢ η \to (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \neq \emptyset \to \exists a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a)$
471	463 470	biimtrrid	$⊢ η \to (\neg A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} = \emptyset \to \exists a \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \forall d \in (A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}) \neg d R a)$
472	462 471	mt3d	$⊢ η \to A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} = \emptyset$
473		ssdif0	$⊢ A \subseteq \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \leftrightarrow A ∖ \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} = \emptyset$
474	472 473	sylibr	$⊢ η \to A \subseteq \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}$
475	81	a1i	$⊢ η \to \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \subseteq A$
476	474 475	eqssd	$⊢ η \to A = \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\}$
477		rabid2	$⊢ A = \{c \in A \| \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)\} \leftrightarrow \forall c \in A \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)$
478	476 477	sylib	$⊢ η \to \forall c \in A \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)$
479		eqeq2	$⊢ c = C \to (f (M) = c \leftrightarrow f (M) = C)$
480	479	anbi1d	$⊢ c = C \to ((f (M) = c \land τ) \leftrightarrow (f (M) = C \land τ))$
481	480	3anbi2d	$⊢ c = C \to ((f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow (f : (M \dots n) ⟶ A \land (f (M) = C \land τ) \land \forall k \in (N \dots n) χ))$
482	481	exbidv	$⊢ c = C \to (\exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists f (f : (M \dots n) ⟶ A \land (f (M) = C \land τ) \land \forall k \in (N \dots n) χ))$
483	482	rexbidv	$⊢ c = C \to (\exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ) \leftrightarrow \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = C \land τ) \land \forall k \in (N \dots n) χ))$
484	483	rspcva	$⊢ (C \in A \land \forall c \in A \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = c \land τ) \land \forall k \in (N \dots n) χ)) \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = C \land τ) \land \forall k \in (N \dots n) χ)$
485	8 478 484	syl2anc	$⊢ η \to \exists n \in Z \exists f (f : (M \dots n) ⟶ A \land (f (M) = C \land τ) \land \forall k \in (N \dots n) χ)$

Metamath Proof Explorer

Theorem fdc

Proof