sdclem2

	Ref	Expression
Hypotheses	sdc.1	$⊢ Z = ℤ_{\geq M}$
	sdc.2	$⊢ g = {f ↾}_{(M \dots n)} \to (ψ \leftrightarrow χ)$
	sdc.3	$⊢ n = M \to (ψ \leftrightarrow τ)$
	sdc.4	$⊢ n = k \to (ψ \leftrightarrow θ)$
	sdc.5	$⊢ (g = h \land n = k + 1) \to (ψ \leftrightarrow σ)$
	sdc.6	$⊢ φ \to A \in V$
	sdc.7	$⊢ φ \to M \in ℤ$
	sdc.8	$⊢ φ \to \exists g (g : \{M\} ⟶ A \land τ)$
	sdc.9	$⊢ (φ \land k \in Z) \to ((g : (M \dots k) ⟶ A \land θ) \to \exists h (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ))$
	sdc.10	$⊢ J = \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\}$
	sdc.11	$⊢ F = (w \in Z, x \in J ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\})$
	sdc.12	$⊢ Ⅎ k φ$
	sdc.13	$⊢ φ \to G : Z ⟶ J$
	sdc.14	$⊢ φ \to G (M) : (M \dots M) ⟶ A$
	sdc.15	$⊢ (φ \land w \in Z) \to G (w + 1) \in (w F G (w))$
Assertion	sdclem2	$⊢ φ \to \exists f (f : Z ⟶ A \land \forall n \in Z χ)$

Proof

Step	Hyp	Ref	Expression
1		sdc.1	$⊢ Z = ℤ_{\geq M}$
2		sdc.2	$⊢ g = {f ↾}_{(M \dots n)} \to (ψ \leftrightarrow χ)$
3		sdc.3	$⊢ n = M \to (ψ \leftrightarrow τ)$
4		sdc.4	$⊢ n = k \to (ψ \leftrightarrow θ)$
5		sdc.5	$⊢ (g = h \land n = k + 1) \to (ψ \leftrightarrow σ)$
6		sdc.6	$⊢ φ \to A \in V$
7		sdc.7	$⊢ φ \to M \in ℤ$
8		sdc.8	$⊢ φ \to \exists g (g : \{M\} ⟶ A \land τ)$
9		sdc.9	$⊢ (φ \land k \in Z) \to ((g : (M \dots k) ⟶ A \land θ) \to \exists h (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ))$
10		sdc.10	$⊢ J = \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\}$
11		sdc.11	$⊢ F = (w \in Z, x \in J ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\})$
12		sdc.12	$⊢ Ⅎ k φ$
13		sdc.13	$⊢ φ \to G : Z ⟶ J$
14		sdc.14	$⊢ φ \to G (M) : (M \dots M) ⟶ A$
15		sdc.15	$⊢ (φ \land w \in Z) \to G (w + 1) \in (w F G (w))$
16	13	ffvelrnda	$⊢ (φ \land k \in Z) \to G (k) \in J$
17	10	eleq2i	$⊢ G (k) \in J \leftrightarrow G (k) \in \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\}$
18		nfcv	$⊢ \underline{Ⅎ} g Z$
19		nfv	$⊢ Ⅎ g G (k) : (M \dots n) ⟶ A$
20		nfsbc1v	$⊢ Ⅎ g \underset{˙}{[} G (k) / g \underset{˙}{]} ψ$
21	19 20	nfan	$⊢ Ⅎ g (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ)$
22	18 21	nfrex	$⊢ Ⅎ g \exists n \in Z (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ)$
23		fvex	$⊢ G (k) \in V$
24		feq1	$⊢ g = G (k) \to (g : (M \dots n) ⟶ A \leftrightarrow G (k) : (M \dots n) ⟶ A)$
25		sbceq1a	$⊢ g = G (k) \to (ψ \leftrightarrow \underset{˙}{[} G (k) / g \underset{˙}{]} ψ)$
26	24 25	anbi12d	$⊢ g = G (k) \to ((g : (M \dots n) ⟶ A \land ψ) \leftrightarrow (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ))$
27	26	rexbidv	$⊢ g = G (k) \to (\exists n \in Z (g : (M \dots n) ⟶ A \land ψ) \leftrightarrow \exists n \in Z (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ))$
28	22 23 27	elabf	$⊢ G (k) \in \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} \leftrightarrow \exists n \in Z (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ)$
29	17 28	bitri	$⊢ G (k) \in J \leftrightarrow \exists n \in Z (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ)$
30	16 29	sylib	$⊢ (φ \land k \in Z) \to \exists n \in Z (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ)$
31		fdm	$⊢ G (k) : (M \dots n) ⟶ A \to dom G (k) = (M \dots n)$
32	31	adantr	$⊢ (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ) \to dom G (k) = (M \dots n)$
33		fveq2	$⊢ x = M \to G (x) = G (M)$
34		oveq2	$⊢ x = M \to (M \dots x) = (M \dots M)$
35	34	mpteq1d	$⊢ x = M \to (m \in (M \dots x) ⟼ G (m) (m)) = (m \in (M \dots M) ⟼ G (m) (m))$
36	33 35	eqeq12d	$⊢ x = M \to (G (x) = (m \in (M \dots x) ⟼ G (m) (m)) \leftrightarrow G (M) = (m \in (M \dots M) ⟼ G (m) (m)))$
37	36	imbi2d	$⊢ x = M \to ((φ \to G (x) = (m \in (M \dots x) ⟼ G (m) (m))) \leftrightarrow (φ \to G (M) = (m \in (M \dots M) ⟼ G (m) (m))))$
38		fveq2	$⊢ x = w \to G (x) = G (w)$
39		oveq2	$⊢ x = w \to (M \dots x) = (M \dots w)$
40	39	mpteq1d	$⊢ x = w \to (m \in (M \dots x) ⟼ G (m) (m)) = (m \in (M \dots w) ⟼ G (m) (m))$
41	38 40	eqeq12d	$⊢ x = w \to (G (x) = (m \in (M \dots x) ⟼ G (m) (m)) \leftrightarrow G (w) = (m \in (M \dots w) ⟼ G (m) (m)))$
42	41	imbi2d	$⊢ x = w \to ((φ \to G (x) = (m \in (M \dots x) ⟼ G (m) (m))) \leftrightarrow (φ \to G (w) = (m \in (M \dots w) ⟼ G (m) (m))))$
43		fveq2	$⊢ x = w + 1 \to G (x) = G (w + 1)$
44		oveq2	$⊢ x = w + 1 \to (M \dots x) = (M \dots w + 1)$
45	44	mpteq1d	$⊢ x = w + 1 \to (m \in (M \dots x) ⟼ G (m) (m)) = (m \in (M \dots w + 1) ⟼ G (m) (m))$
46	43 45	eqeq12d	$⊢ x = w + 1 \to (G (x) = (m \in (M \dots x) ⟼ G (m) (m)) \leftrightarrow G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)))$
47	46	imbi2d	$⊢ x = w + 1 \to ((φ \to G (x) = (m \in (M \dots x) ⟼ G (m) (m))) \leftrightarrow (φ \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))))$
48		fveq2	$⊢ x = k \to G (x) = G (k)$
49		oveq2	$⊢ x = k \to (M \dots x) = (M \dots k)$
50	49	mpteq1d	$⊢ x = k \to (m \in (M \dots x) ⟼ G (m) (m)) = (m \in (M \dots k) ⟼ G (m) (m))$
51	48 50	eqeq12d	$⊢ x = k \to (G (x) = (m \in (M \dots x) ⟼ G (m) (m)) \leftrightarrow G (k) = (m \in (M \dots k) ⟼ G (m) (m)))$
52	51	imbi2d	$⊢ x = k \to ((φ \to G (x) = (m \in (M \dots x) ⟼ G (m) (m))) \leftrightarrow (φ \to G (k) = (m \in (M \dots k) ⟼ G (m) (m))))$
53		fveq2	$⊢ m = k \to G (m) = G (k)$
54		id	$⊢ m = k \to m = k$
55	53 54	fveq12d	$⊢ m = k \to G (m) (m) = G (k) (k)$
56		eqid	$⊢ (m \in (M \dots M) ⟼ G (m) (m)) = (m \in (M \dots M) ⟼ G (m) (m))$
57		fvex	$⊢ G (k) (k) \in V$
58	55 56 57	fvmpt	$⊢ k \in (M \dots M) \to (m \in (M \dots M) ⟼ G (m) (m)) (k) = G (k) (k)$
59	58	adantl	$⊢ (φ \land k \in (M \dots M)) \to (m \in (M \dots M) ⟼ G (m) (m)) (k) = G (k) (k)$
60		elfz1eq	$⊢ k \in (M \dots M) \to k = M$
61	60	adantl	$⊢ (φ \land k \in (M \dots M)) \to k = M$
62	61	fveq2d	$⊢ (φ \land k \in (M \dots M)) \to G (k) = G (M)$
63	62	fveq1d	$⊢ (φ \land k \in (M \dots M)) \to G (k) (k) = G (M) (k)$
64	59 63	eqtr2d	$⊢ (φ \land k \in (M \dots M)) \to G (M) (k) = (m \in (M \dots M) ⟼ G (m) (m)) (k)$
65	64	ex	$⊢ φ \to (k \in (M \dots M) \to G (M) (k) = (m \in (M \dots M) ⟼ G (m) (m)) (k))$
66	12 65	ralrimi	$⊢ φ \to \forall k \in (M \dots M) G (M) (k) = (m \in (M \dots M) ⟼ G (m) (m)) (k)$
67	14	ffnd	$⊢ φ \to G (M) Fn (M \dots M)$
68		fvex	$⊢ G (m) (m) \in V$
69	68 56	fnmpti	$⊢ (m \in (M \dots M) ⟼ G (m) (m)) Fn (M \dots M)$
70		eqfnfv	$⊢ (G (M) Fn (M \dots M) \land (m \in (M \dots M) ⟼ G (m) (m)) Fn (M \dots M)) \to (G (M) = (m \in (M \dots M) ⟼ G (m) (m)) \leftrightarrow \forall k \in (M \dots M) G (M) (k) = (m \in (M \dots M) ⟼ G (m) (m)) (k))$
71	67 69 70	sylancl	$⊢ φ \to (G (M) = (m \in (M \dots M) ⟼ G (m) (m)) \leftrightarrow \forall k \in (M \dots M) G (M) (k) = (m \in (M \dots M) ⟼ G (m) (m)) (k))$
72	66 71	mpbird	$⊢ φ \to G (M) = (m \in (M \dots M) ⟼ G (m) (m))$
73	72	a1i	$⊢ M \in ℤ \to (φ \to G (M) = (m \in (M \dots M) ⟼ G (m) (m)))$
74	1	eleq2i	$⊢ w \in Z \leftrightarrow w \in ℤ_{\geq M}$
75	13	ffvelrnda	$⊢ (φ \land w \in Z) \to G (w) \in J$
76		simpr	$⊢ (φ \land w \in Z) \to w \in Z$
77		3simpa	$⊢ (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ) \to (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})$
78	77	reximi	$⊢ \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ) \to \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})$
79	78	ss2abi	$⊢ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\} \subseteq \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\}$
80	1	fvexi	$⊢ Z \in V$
81		nfv	$⊢ Ⅎ k w \in Z$
82	12 81	nfan	$⊢ Ⅎ k (φ \land w \in Z)$
83	6	adantr	$⊢ (φ \land w \in Z) \to A \in V$
84		simpl	$⊢ (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)}) \to h : (M \dots k + 1) ⟶ A$
85		ovex	$⊢ (M \dots k + 1) \in V$
86		elmapg	$⊢ (A \in V \land (M \dots k + 1) \in V) \to (h \in (A^{(M \dots k + 1)}) \leftrightarrow h : (M \dots k + 1) ⟶ A)$
87	85 86	mpan2	$⊢ A \in V \to (h \in (A^{(M \dots k + 1)}) \leftrightarrow h : (M \dots k + 1) ⟶ A)$
88	84 87	syl5ibr	$⊢ A \in V \to ((h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)}) \to h \in (A^{(M \dots k + 1)}))$
89	88	abssdv	$⊢ A \in V \to \{h \| (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \subseteq A^{(M \dots k + 1)}$
90	83 89	syl	$⊢ (φ \land w \in Z) \to \{h \| (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \subseteq A^{(M \dots k + 1)}$
91		ovex	$⊢ A^{(M \dots k + 1)} \in V$
92		ssexg	$⊢ (\{h \| (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \subseteq A^{(M \dots k + 1)} \land A^{(M \dots k + 1)} \in V) \to \{h \| (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \in V$
93	90 91 92	sylancl	$⊢ (φ \land w \in Z) \to \{h \| (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \in V$
94	93	a1d	$⊢ (φ \land w \in Z) \to (k \in Z \to \{h \| (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \in V)$
95	82 94	ralrimi	$⊢ (φ \land w \in Z) \to \forall k \in Z \{h \| (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \in V$
96		abrexex2g	$⊢ (Z \in V \land \forall k \in Z \{h \| (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \in V) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \in V$
97	80 95 96	sylancr	$⊢ (φ \land w \in Z) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \in V$
98		ssexg	$⊢ (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\} \subseteq \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \land \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \in V) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\} \in V$
99	79 97 98	sylancr	$⊢ (φ \land w \in Z) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\} \in V$
100		eqeq1	$⊢ x = G (w) \to (x = {h ↾}_{(M \dots k)} \leftrightarrow G (w) = {h ↾}_{(M \dots k)})$
101	100	3anbi2d	$⊢ x = G (w) \to ((h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ) \leftrightarrow (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ))$
102	101	rexbidv	$⊢ x = G (w) \to (\exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ) \leftrightarrow \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ))$
103	102	abbidv	$⊢ x = G (w) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\}$
104	103	eleq1d	$⊢ x = G (w) \to (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in V \leftrightarrow \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\} \in V)$
105		oveq2	$⊢ x = G (w) \to w F x = w F G (w)$
106	105 103	eqeq12d	$⊢ x = G (w) \to (w F x = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \leftrightarrow w F G (w) = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\})$
107	104 106	imbi12d	$⊢ x = G (w) \to ((\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in V \to w F x = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\}) \leftrightarrow (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\} \in V \to w F G (w) = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\}))$
108	107	imbi2d	$⊢ x = G (w) \to ((w \in Z \to (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in V \to w F x = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\})) \leftrightarrow (w \in Z \to (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\} \in V \to w F G (w) = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\})))$
109	11	ovmpt4g	$⊢ (w \in Z \land x \in J \land \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in V) \to w F x = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\}$
110	109	3com12	$⊢ (x \in J \land w \in Z \land \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in V) \to w F x = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\}$
111	110	3exp	$⊢ x \in J \to (w \in Z \to (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in V \to w F x = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\}))$
112	108 111	vtoclga	$⊢ G (w) \in J \to (w \in Z \to (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\} \in V \to w F G (w) = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\}))$
113	75 76 99 112	syl3c	$⊢ (φ \land w \in Z) \to w F G (w) = \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)} \land σ)\}$
114	113 79	eqsstrdi	$⊢ (φ \land w \in Z) \to w F G (w) \subseteq \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\}$
115	114 15	sseldd	$⊢ (φ \land w \in Z) \to G (w + 1) \in \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\}$
116		fvex	$⊢ G (w + 1) \in V$
117		feq1	$⊢ h = G (w + 1) \to (h : (M \dots k + 1) ⟶ A \leftrightarrow G (w + 1) : (M \dots k + 1) ⟶ A)$
118		reseq1	$⊢ h = G (w + 1) \to {h ↾}_{(M \dots k)} = {G (w + 1) ↾}_{(M \dots k)}$
119	118	eqeq2d	$⊢ h = G (w + 1) \to (G (w) = {h ↾}_{(M \dots k)} \leftrightarrow G (w) = {G (w + 1) ↾}_{(M \dots k)})$
120	117 119	anbi12d	$⊢ h = G (w + 1) \to ((h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)}) \leftrightarrow (G (w + 1) : (M \dots k + 1) ⟶ A \land G (w) = {G (w + 1) ↾}_{(M \dots k)}))$
121	120	rexbidv	$⊢ h = G (w + 1) \to (\exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)}) \leftrightarrow \exists k \in Z (G (w + 1) : (M \dots k + 1) ⟶ A \land G (w) = {G (w + 1) ↾}_{(M \dots k)}))$
122	116 121	elab	$⊢ G (w + 1) \in \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land G (w) = {h ↾}_{(M \dots k)})\} \leftrightarrow \exists k \in Z (G (w + 1) : (M \dots k + 1) ⟶ A \land G (w) = {G (w + 1) ↾}_{(M \dots k)})$
123	115 122	sylib	$⊢ (φ \land w \in Z) \to \exists k \in Z (G (w + 1) : (M \dots k + 1) ⟶ A \land G (w) = {G (w + 1) ↾}_{(M \dots k)})$
124		nfv	$⊢ Ⅎ k (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)))$
125		simprl	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to G (w + 1) : (M \dots k + 1) ⟶ A$
126		fzssp1	$⊢ (M \dots k) \subseteq (M \dots k + 1)$
127		fssres	$⊢ (G (w + 1) : (M \dots k + 1) ⟶ A \land (M \dots k) \subseteq (M \dots k + 1)) \to ({G (w + 1) ↾}_{(M \dots k)}) : (M \dots k) ⟶ A$
128	125 126 127	sylancl	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to ({G (w + 1) ↾}_{(M \dots k)}) : (M \dots k) ⟶ A$
129	128	fdmd	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to dom ({G (w + 1) ↾}_{(M \dots k)}) = (M \dots k)$
130		eqid	$⊢ (m \in (M \dots w) ⟼ G (m) (m)) = (m \in (M \dots w) ⟼ G (m) (m))$
131	68 130	fnmpti	$⊢ (m \in (M \dots w) ⟼ G (m) (m)) Fn (M \dots w)$
132		simprr	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m))$
133	132	fneq1d	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (({G (w + 1) ↾}_{(M \dots k)}) Fn (M \dots w) \leftrightarrow (m \in (M \dots w) ⟼ G (m) (m)) Fn (M \dots w))$
134	131 133	mpbiri	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to ({G (w + 1) ↾}_{(M \dots k)}) Fn (M \dots w)$
135	134	fndmd	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to dom ({G (w + 1) ↾}_{(M \dots k)}) = (M \dots w)$
136	129 135	eqtr3d	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (M \dots k) = (M \dots w)$
137		simplr	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to k \in Z$
138	137 1	eleqtrdi	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to k \in ℤ_{\geq M}$
139		fzopth	$⊢ k \in ℤ_{\geq M} \to ((M \dots k) = (M \dots w) \leftrightarrow (M = M \land k = w))$
140	138 139	syl	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to ((M \dots k) = (M \dots w) \leftrightarrow (M = M \land k = w))$
141	136 140	mpbid	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (M = M \land k = w)$
142	141	simprd	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to k = w$
143	142	oveq1d	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to k + 1 = w + 1$
144	143	oveq2d	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (M \dots k + 1) = (M \dots w + 1)$
145		elfzp1	$⊢ k \in ℤ_{\geq M} \to (x \in (M \dots k + 1) \leftrightarrow (x \in (M \dots k) \lor x = k + 1))$
146	138 145	syl	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (x \in (M \dots k + 1) \leftrightarrow (x \in (M \dots k) \lor x = k + 1))$
147	136	reseq2d	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to {(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots k)} = {(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots w)}$
148		fzssp1	$⊢ (M \dots w) \subseteq (M \dots w + 1)$
149		resmpt	$⊢ (M \dots w) \subseteq (M \dots w + 1) \to {(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots w)} = (m \in (M \dots w) ⟼ G (m) (m))$
150	148 149	ax-mp	$⊢ {(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots w)} = (m \in (M \dots w) ⟼ G (m) (m))$
151	147 150	eqtr2di	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (m \in (M \dots w) ⟼ G (m) (m)) = {(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots k)}$
152	132 151	eqtrd	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to {G (w + 1) ↾}_{(M \dots k)} = {(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots k)}$
153	152	fveq1d	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to ({G (w + 1) ↾}_{(M \dots k)}) (x) = ({(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots k)}) (x)$
154		fvres	$⊢ x \in (M \dots k) \to ({G (w + 1) ↾}_{(M \dots k)}) (x) = G (w + 1) (x)$
155		fvres	$⊢ x \in (M \dots k) \to ({(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots k)}) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x)$
156	154 155	eqeq12d	$⊢ x \in (M \dots k) \to (({G (w + 1) ↾}_{(M \dots k)}) (x) = ({(m \in (M \dots w + 1) ⟼ G (m) (m)) ↾}_{(M \dots k)}) (x) \leftrightarrow G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x))$
157	153 156	syl5ibcom	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (x \in (M \dots k) \to G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x))$
158	143	eqeq2d	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (x = k + 1 \leftrightarrow x = w + 1)$
159	142 138	eqeltrrd	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to w \in ℤ_{\geq M}$
160		peano2uz	$⊢ w \in ℤ_{\geq M} \to w + 1 \in ℤ_{\geq M}$
161		eluzfz2	$⊢ w + 1 \in ℤ_{\geq M} \to w + 1 \in (M \dots w + 1)$
162		fveq2	$⊢ m = w + 1 \to G (m) = G (w + 1)$
163		id	$⊢ m = w + 1 \to m = w + 1$
164	162 163	fveq12d	$⊢ m = w + 1 \to G (m) (m) = G (w + 1) (w + 1)$
165		eqid	$⊢ (m \in (M \dots w + 1) ⟼ G (m) (m)) = (m \in (M \dots w + 1) ⟼ G (m) (m))$
166		fvex	$⊢ G (w + 1) (w + 1) \in V$
167	164 165 166	fvmpt	$⊢ w + 1 \in (M \dots w + 1) \to (m \in (M \dots w + 1) ⟼ G (m) (m)) (w + 1) = G (w + 1) (w + 1)$
168	159 160 161 167	4syl	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (m \in (M \dots w + 1) ⟼ G (m) (m)) (w + 1) = G (w + 1) (w + 1)$
169	168	eqcomd	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to G (w + 1) (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (w + 1)$
170		fveq2	$⊢ x = w + 1 \to G (w + 1) (x) = G (w + 1) (w + 1)$
171		fveq2	$⊢ x = w + 1 \to (m \in (M \dots w + 1) ⟼ G (m) (m)) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (w + 1)$
172	170 171	eqeq12d	$⊢ x = w + 1 \to (G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x) \leftrightarrow G (w + 1) (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (w + 1))$
173	169 172	syl5ibrcom	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (x = w + 1 \to G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x))$
174	158 173	sylbid	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (x = k + 1 \to G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x))$
175	157 174	jaod	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to ((x \in (M \dots k) \lor x = k + 1) \to G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x))$
176	146 175	sylbid	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (x \in (M \dots k + 1) \to G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x))$
177	176	ralrimiv	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to \forall x \in (M \dots k + 1) G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x)$
178		ffn	$⊢ G (w + 1) : (M \dots k + 1) ⟶ A \to G (w + 1) Fn (M \dots k + 1)$
179	178	ad2antrl	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to G (w + 1) Fn (M \dots k + 1)$
180	68 165	fnmpti	$⊢ (m \in (M \dots w + 1) ⟼ G (m) (m)) Fn (M \dots w + 1)$
181		eqfnfv2	$⊢ (G (w + 1) Fn (M \dots k + 1) \land (m \in (M \dots w + 1) ⟼ G (m) (m)) Fn (M \dots w + 1)) \to (G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)) \leftrightarrow ((M \dots k + 1) = (M \dots w + 1) \land \forall x \in (M \dots k + 1) G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x)))$
182	179 180 181	sylancl	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to (G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)) \leftrightarrow ((M \dots k + 1) = (M \dots w + 1) \land \forall x \in (M \dots k + 1) G (w + 1) (x) = (m \in (M \dots w + 1) ⟼ G (m) (m)) (x)))$
183	144 177 182	mpbir2and	$⊢ (((φ \land w \in Z) \land k \in Z) \land (G (w + 1) : (M \dots k + 1) ⟶ A \land {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))$
184	183	expr	$⊢ (((φ \land w \in Z) \land k \in Z) \land G (w + 1) : (M \dots k + 1) ⟶ A) \to ({G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)))$
185		eqeq1	$⊢ G (w) = {G (w + 1) ↾}_{(M \dots k)} \to (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \leftrightarrow {G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)))$
186	185	imbi1d	$⊢ G (w) = {G (w + 1) ↾}_{(M \dots k)} \to ((G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))) \leftrightarrow ({G (w + 1) ↾}_{(M \dots k)} = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))))$
187	184 186	syl5ibrcom	$⊢ (((φ \land w \in Z) \land k \in Z) \land G (w + 1) : (M \dots k + 1) ⟶ A) \to (G (w) = {G (w + 1) ↾}_{(M \dots k)} \to (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))))$
188	187	expimpd	$⊢ ((φ \land w \in Z) \land k \in Z) \to ((G (w + 1) : (M \dots k + 1) ⟶ A \land G (w) = {G (w + 1) ↾}_{(M \dots k)}) \to (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))))$
189	188	ex	$⊢ (φ \land w \in Z) \to (k \in Z \to ((G (w + 1) : (M \dots k + 1) ⟶ A \land G (w) = {G (w + 1) ↾}_{(M \dots k)}) \to (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)))))$
190	82 124 189	rexlimd	$⊢ (φ \land w \in Z) \to (\exists k \in Z (G (w + 1) : (M \dots k + 1) ⟶ A \land G (w) = {G (w + 1) ↾}_{(M \dots k)}) \to (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))))$
191	123 190	mpd	$⊢ (φ \land w \in Z) \to (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m)))$
192	191	expcom	$⊢ w \in Z \to (φ \to (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))))$
193	74 192	sylbir	$⊢ w \in ℤ_{\geq M} \to (φ \to (G (w) = (m \in (M \dots w) ⟼ G (m) (m)) \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))))$
194	193	a2d	$⊢ w \in ℤ_{\geq M} \to ((φ \to G (w) = (m \in (M \dots w) ⟼ G (m) (m))) \to (φ \to G (w + 1) = (m \in (M \dots w + 1) ⟼ G (m) (m))))$
195	37 42 47 52 73 194	uzind4	$⊢ k \in ℤ_{\geq M} \to (φ \to G (k) = (m \in (M \dots k) ⟼ G (m) (m)))$
196	195 1	eleq2s	$⊢ k \in Z \to (φ \to G (k) = (m \in (M \dots k) ⟼ G (m) (m)))$
197	196	impcom	$⊢ (φ \land k \in Z) \to G (k) = (m \in (M \dots k) ⟼ G (m) (m))$
198	197	dmeqd	$⊢ (φ \land k \in Z) \to dom G (k) = dom (m \in (M \dots k) ⟼ G (m) (m))$
199		dmmptg	$⊢ \forall m \in (M \dots k) G (m) (m) \in V \to dom (m \in (M \dots k) ⟼ G (m) (m)) = (M \dots k)$
200	68	a1i	$⊢ m \in (M \dots k) \to G (m) (m) \in V$
201	199 200	mprg	$⊢ dom (m \in (M \dots k) ⟼ G (m) (m)) = (M \dots k)$
202	198 201	eqtrdi	$⊢ (φ \land k \in Z) \to dom G (k) = (M \dots k)$
203	202	eqeq1d	$⊢ (φ \land k \in Z) \to (dom G (k) = (M \dots n) \leftrightarrow (M \dots k) = (M \dots n))$
204		simpr	$⊢ (φ \land k \in Z) \to k \in Z$
205	204 1	eleqtrdi	$⊢ (φ \land k \in Z) \to k \in ℤ_{\geq M}$
206		fzopth	$⊢ k \in ℤ_{\geq M} \to ((M \dots k) = (M \dots n) \leftrightarrow (M = M \land k = n))$
207	205 206	syl	$⊢ (φ \land k \in Z) \to ((M \dots k) = (M \dots n) \leftrightarrow (M = M \land k = n))$
208	203 207	bitrd	$⊢ (φ \land k \in Z) \to (dom G (k) = (M \dots n) \leftrightarrow (M = M \land k = n))$
209		simpr	$⊢ (M = M \land k = n) \to k = n$
210	208 209	syl6bi	$⊢ (φ \land k \in Z) \to (dom G (k) = (M \dots n) \to k = n)$
211	32 210	syl5	$⊢ (φ \land k \in Z) \to ((G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ) \to k = n)$
212		oveq2	$⊢ n = k \to (M \dots n) = (M \dots k)$
213	212	feq2d	$⊢ n = k \to (G (k) : (M \dots n) ⟶ A \leftrightarrow G (k) : (M \dots k) ⟶ A)$
214	4	sbcbidv	$⊢ n = k \to (\underset{˙}{[} G (k) / g \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} G (k) / g \underset{˙}{]} θ)$
215	213 214	anbi12d	$⊢ n = k \to ((G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ) \leftrightarrow (G (k) : (M \dots k) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} θ))$
216	215	equcoms	$⊢ k = n \to ((G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ) \leftrightarrow (G (k) : (M \dots k) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} θ))$
217	216	biimpcd	$⊢ (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ) \to (k = n \to (G (k) : (M \dots k) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} θ))$
218	211 217	sylcom	$⊢ (φ \land k \in Z) \to ((G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ) \to (G (k) : (M \dots k) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} θ))$
219	218	rexlimdvw	$⊢ (φ \land k \in Z) \to (\exists n \in Z (G (k) : (M \dots n) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} ψ) \to (G (k) : (M \dots k) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} θ))$
220	30 219	mpd	$⊢ (φ \land k \in Z) \to (G (k) : (M \dots k) ⟶ A \land \underset{˙}{[} G (k) / g \underset{˙}{]} θ)$
221	220	simpld	$⊢ (φ \land k \in Z) \to G (k) : (M \dots k) ⟶ A$
222		eluzfz2	$⊢ k \in ℤ_{\geq M} \to k \in (M \dots k)$
223	205 222	syl	$⊢ (φ \land k \in Z) \to k \in (M \dots k)$
224	221 223	ffvelrnd	$⊢ (φ \land k \in Z) \to G (k) (k) \in A$
225	55	cbvmptv	$⊢ (m \in Z ⟼ G (m) (m)) = (k \in Z ⟼ G (k) (k))$
226	12 224 225	fmptdf	$⊢ φ \to (m \in Z ⟼ G (m) (m)) : Z ⟶ A$
227	220	simprd	$⊢ (φ \land k \in Z) \to \underset{˙}{[} G (k) / g \underset{˙}{]} θ$
228	197 227	sbceq1dd	$⊢ (φ \land k \in Z) \to \underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} θ$
229	228	ex	$⊢ φ \to (k \in Z \to \underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} θ)$
230	12 229	ralrimi	$⊢ φ \to \forall k \in Z \underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} θ$
231		mpteq1	$⊢ (M \dots n) = (M \dots k) \to (m \in (M \dots n) ⟼ G (m) (m)) = (m \in (M \dots k) ⟼ G (m) (m))$
232		dfsbcq	$⊢ (m \in (M \dots n) ⟼ G (m) (m)) = (m \in (M \dots k) ⟼ G (m) (m)) \to (\underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} ψ)$
233	212 231 232	3syl	$⊢ n = k \to (\underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} ψ)$
234	4	sbcbidv	$⊢ n = k \to (\underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} θ)$
235	233 234	bitrd	$⊢ n = k \to (\underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} θ)$
236	235	cbvralvw	$⊢ \forall n \in Z \underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ \leftrightarrow \forall k \in Z \underset{˙}{[} (m \in (M \dots k) ⟼ G (m) (m)) / g \underset{˙}{]} θ$
237	230 236	sylibr	$⊢ φ \to \forall n \in Z \underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ$
238	80	mptex	$⊢ (m \in Z ⟼ G (m) (m)) \in V$
239		feq1	$⊢ f = (m \in Z ⟼ G (m) (m)) \to (f : Z ⟶ A \leftrightarrow (m \in Z ⟼ G (m) (m)) : Z ⟶ A)$
240		vex	$⊢ f \in V$
241	240	resex	$⊢ {f ↾}_{(M \dots n)} \in V$
242	241 2	sbcie	$⊢ \underset{˙}{[} ({f ↾}_{(M \dots n)}) / g \underset{˙}{]} ψ \leftrightarrow χ$
243		reseq1	$⊢ f = (m \in Z ⟼ G (m) (m)) \to {f ↾}_{(M \dots n)} = {(m \in Z ⟼ G (m) (m)) ↾}_{(M \dots n)}$
244		fzssuz	$⊢ (M \dots n) \subseteq ℤ_{\geq M}$
245	244 1	sseqtrri	$⊢ (M \dots n) \subseteq Z$
246		resmpt	$⊢ (M \dots n) \subseteq Z \to {(m \in Z ⟼ G (m) (m)) ↾}_{(M \dots n)} = (m \in (M \dots n) ⟼ G (m) (m))$
247	245 246	ax-mp	$⊢ {(m \in Z ⟼ G (m) (m)) ↾}_{(M \dots n)} = (m \in (M \dots n) ⟼ G (m) (m))$
248	243 247	eqtrdi	$⊢ f = (m \in Z ⟼ G (m) (m)) \to {f ↾}_{(M \dots n)} = (m \in (M \dots n) ⟼ G (m) (m))$
249	248	sbceq1d	$⊢ f = (m \in Z ⟼ G (m) (m)) \to (\underset{˙}{[} ({f ↾}_{(M \dots n)}) / g \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ)$
250	242 249	bitr3id	$⊢ f = (m \in Z ⟼ G (m) (m)) \to (χ \leftrightarrow \underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ)$
251	250	ralbidv	$⊢ f = (m \in Z ⟼ G (m) (m)) \to (\forall n \in Z χ \leftrightarrow \forall n \in Z \underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ)$
252	239 251	anbi12d	$⊢ f = (m \in Z ⟼ G (m) (m)) \to ((f : Z ⟶ A \land \forall n \in Z χ) \leftrightarrow ((m \in Z ⟼ G (m) (m)) : Z ⟶ A \land \forall n \in Z \underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ))$
253	238 252	spcev	$⊢ ((m \in Z ⟼ G (m) (m)) : Z ⟶ A \land \forall n \in Z \underset{˙}{[} (m \in (M \dots n) ⟼ G (m) (m)) / g \underset{˙}{]} ψ) \to \exists f (f : Z ⟶ A \land \forall n \in Z χ)$
254	226 237 253	syl2anc	$⊢ φ \to \exists f (f : Z ⟶ A \land \forall n \in Z χ)$

Metamath Proof Explorer

Theorem sdclem2

Proof