sdclem1

	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 σ)\})$
Assertion	sdclem1	$⊢ φ \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	1	fvexi	$⊢ Z \in V$
13		simpl	$⊢ (g : (M \dots n) ⟶ A \land ψ) \to g : (M \dots n) ⟶ A$
14		ovex	$⊢ (M \dots n) \in V$
15		elmapg	$⊢ (A \in V \land (M \dots n) \in V) \to (g \in (A^{(M \dots n)}) \leftrightarrow g : (M \dots n) ⟶ A)$
16	6 14 15	sylancl	$⊢ φ \to (g \in (A^{(M \dots n)}) \leftrightarrow g : (M \dots n) ⟶ A)$
17	13 16	syl5ibr	$⊢ φ \to ((g : (M \dots n) ⟶ A \land ψ) \to g \in (A^{(M \dots n)}))$
18	17	abssdv	$⊢ φ \to \{g \| (g : (M \dots n) ⟶ A \land ψ)\} \subseteq A^{(M \dots n)}$
19		ovex	$⊢ A^{(M \dots n)} \in V$
20		ssexg	$⊢ (\{g \| (g : (M \dots n) ⟶ A \land ψ)\} \subseteq A^{(M \dots n)} \land A^{(M \dots n)} \in V) \to \{g \| (g : (M \dots n) ⟶ A \land ψ)\} \in V$
21	18 19 20	sylancl	$⊢ φ \to \{g \| (g : (M \dots n) ⟶ A \land ψ)\} \in V$
22	21	ralrimivw	$⊢ φ \to \forall n \in Z \{g \| (g : (M \dots n) ⟶ A \land ψ)\} \in V$
23		abrexex2g	$⊢ (Z \in V \land \forall n \in Z \{g \| (g : (M \dots n) ⟶ A \land ψ)\} \in V) \to \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} \in V$
24	12 22 23	sylancr	$⊢ φ \to \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} \in V$
25	10 24	eqeltrid	$⊢ φ \to J \in V$
26	25	adantr	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to J \in V$
27	7	adantr	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to M \in ℤ$
28		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
29	27 28	syl	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to M \in ℤ_{\geq M}$
30	29 1	eleqtrrdi	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to M \in Z$
31		simprl	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to g : \{M\} ⟶ A$
32		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
33	27 32	syl	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to (M \dots M) = \{M\}$
34	33	feq2d	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to (g : (M \dots M) ⟶ A \leftrightarrow g : \{M\} ⟶ A)$
35	31 34	mpbird	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to g : (M \dots M) ⟶ A$
36		simprr	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to τ$
37		oveq2	$⊢ n = M \to (M \dots n) = (M \dots M)$
38	37	feq2d	$⊢ n = M \to (g : (M \dots n) ⟶ A \leftrightarrow g : (M \dots M) ⟶ A)$
39	38 3	anbi12d	$⊢ n = M \to ((g : (M \dots n) ⟶ A \land ψ) \leftrightarrow (g : (M \dots M) ⟶ A \land τ))$
40	39	rspcev	$⊢ (M \in Z \land (g : (M \dots M) ⟶ A \land τ)) \to \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)$
41	30 35 36 40	syl12anc	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)$
42	10	abeq2i	$⊢ g \in J \leftrightarrow \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)$
43	41 42	sylibr	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to g \in J$
44	1	peano2uzs	$⊢ k \in Z \to k + 1 \in Z$
45	44	ad2antlr	$⊢ ((φ \land k \in Z) \land (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)) \to k + 1 \in Z$
46		simpr1	$⊢ ((φ \land k \in Z) \land (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)) \to h : (M \dots k + 1) ⟶ A$
47		simpr3	$⊢ ((φ \land k \in Z) \land (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)) \to σ$
48		vex	$⊢ h \in V$
49		ovex	$⊢ k + 1 \in V$
50	5	a1i	$⊢ φ \to ((g = h \land n = k + 1) \to (ψ \leftrightarrow σ))$
51	48 49 50	sbc2iedv	$⊢ φ \to (\underset{˙}{[} h / g \underset{˙}{]} \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ \leftrightarrow σ)$
52	51	ad2antrr	$⊢ ((φ \land k \in Z) \land (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)) \to (\underset{˙}{[} h / g \underset{˙}{]} \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ \leftrightarrow σ)$
53	47 52	mpbird	$⊢ ((φ \land k \in Z) \land (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)) \to \underset{˙}{[} h / g \underset{˙}{]} \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ$
54		nfv	$⊢ Ⅎ n h : (M \dots k + 1) ⟶ A$
55		nfcv	$⊢ \underline{Ⅎ} n h$
56		nfsbc1v	$⊢ Ⅎ n \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ$
57	55 56	nfsbcw	$⊢ Ⅎ n \underset{˙}{[} h / g \underset{˙}{]} \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ$
58	54 57	nfan	$⊢ Ⅎ n (h : (M \dots k + 1) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ)$
59		oveq2	$⊢ n = k + 1 \to (M \dots n) = (M \dots k + 1)$
60	59	feq2d	$⊢ n = k + 1 \to (h : (M \dots n) ⟶ A \leftrightarrow h : (M \dots k + 1) ⟶ A)$
61		sbceq1a	$⊢ n = k + 1 \to (ψ \leftrightarrow \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ)$
62	61	sbcbidv	$⊢ n = k + 1 \to (\underset{˙}{[} h / g \underset{˙}{]} ψ \leftrightarrow \underset{˙}{[} h / g \underset{˙}{]} \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ)$
63	60 62	anbi12d	$⊢ n = k + 1 \to ((h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ) \leftrightarrow (h : (M \dots k + 1) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ))$
64	58 63	rspce	$⊢ (k + 1 \in Z \land (h : (M \dots k + 1) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} \underset{˙}{[} (k + 1) / n \underset{˙}{]} ψ)) \to \exists n \in Z (h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ)$
65	45 46 53 64	syl12anc	$⊢ ((φ \land k \in Z) \land (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)) \to \exists n \in Z (h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ)$
66	10	eleq2i	$⊢ h \in J \leftrightarrow h \in \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\}$
67		nfcv	$⊢ \underline{Ⅎ} g Z$
68		nfv	$⊢ Ⅎ g h : (M \dots n) ⟶ A$
69		nfsbc1v	$⊢ Ⅎ g \underset{˙}{[} h / g \underset{˙}{]} ψ$
70	68 69	nfan	$⊢ Ⅎ g (h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ)$
71	67 70	nfrex	$⊢ Ⅎ g \exists n \in Z (h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ)$
72		feq1	$⊢ g = h \to (g : (M \dots n) ⟶ A \leftrightarrow h : (M \dots n) ⟶ A)$
73		sbceq1a	$⊢ g = h \to (ψ \leftrightarrow \underset{˙}{[} h / g \underset{˙}{]} ψ)$
74	72 73	anbi12d	$⊢ g = h \to ((g : (M \dots n) ⟶ A \land ψ) \leftrightarrow (h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ))$
75	74	rexbidv	$⊢ g = h \to (\exists n \in Z (g : (M \dots n) ⟶ A \land ψ) \leftrightarrow \exists n \in Z (h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ))$
76	71 48 75	elabf	$⊢ h \in \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} \leftrightarrow \exists n \in Z (h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ)$
77	66 76	bitri	$⊢ h \in J \leftrightarrow \exists n \in Z (h : (M \dots n) ⟶ A \land \underset{˙}{[} h / g \underset{˙}{]} ψ)$
78	65 77	sylibr	$⊢ ((φ \land k \in Z) \land (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)) \to h \in J$
79	78	rexlimdva2	$⊢ φ \to (\exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ) \to h \in J)$
80	79	abssdv	$⊢ φ \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \subseteq J$
81	80	ad2antrr	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land x \in J) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \subseteq J$
82	25	ad2antrr	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land x \in J) \to J \in V$
83		elpw2g	$⊢ J \in V \to (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in 𝒫 J \leftrightarrow \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \subseteq J)$
84	82 83	syl	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land x \in J) \to (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in 𝒫 J \leftrightarrow \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \subseteq J)$
85	81 84	mpbird	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land x \in J) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in 𝒫 J$
86		oveq2	$⊢ n = k \to (M \dots n) = (M \dots k)$
87	86	feq2d	$⊢ n = k \to (g : (M \dots n) ⟶ A \leftrightarrow g : (M \dots k) ⟶ A)$
88	87 4	anbi12d	$⊢ n = k \to ((g : (M \dots n) ⟶ A \land ψ) \leftrightarrow (g : (M \dots k) ⟶ A \land θ))$
89	88	cbvrexvw	$⊢ \exists n \in Z (g : (M \dots n) ⟶ A \land ψ) \leftrightarrow \exists k \in Z (g : (M \dots k) ⟶ A \land θ)$
90	9	reximdva	$⊢ φ \to (\exists k \in Z (g : (M \dots k) ⟶ A \land θ) \to \exists k \in Z \exists h (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ))$
91		rexcom4	$⊢ \exists k \in Z \exists h (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ) \leftrightarrow \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ)$
92	90 91	syl6ib	$⊢ φ \to (\exists k \in Z (g : (M \dots k) ⟶ A \land θ) \to \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ))$
93	89 92	syl5bi	$⊢ φ \to (\exists n \in Z (g : (M \dots n) ⟶ A \land ψ) \to \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ))$
94	93	ss2abdv	$⊢ φ \to \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} \subseteq \{g \| \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ)\}$
95	10 94	eqsstrid	$⊢ φ \to J \subseteq \{g \| \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ)\}$
96	95	sselda	$⊢ (φ \land x \in J) \to x \in \{g \| \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ)\}$
97		vex	$⊢ x \in V$
98		eqeq1	$⊢ g = x \to (g = {h ↾}_{(M \dots k)} \leftrightarrow x = {h ↾}_{(M \dots k)})$
99	98	3anbi2d	$⊢ g = x \to ((h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ) \leftrightarrow (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ))$
100	99	rexbidv	$⊢ g = x \to (\exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ) \leftrightarrow \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ))$
101	100	exbidv	$⊢ g = x \to (\exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ) \leftrightarrow \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ))$
102	97 101	elab	$⊢ x \in \{g \| \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land g = {h ↾}_{(M \dots k)} \land σ)\} \leftrightarrow \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)$
103	96 102	sylib	$⊢ (φ \land x \in J) \to \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)$
104		abn0	$⊢ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \neq \emptyset \leftrightarrow \exists h \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)$
105	103 104	sylibr	$⊢ (φ \land x \in J) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \neq \emptyset$
106	105	adantlr	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land x \in J) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \neq \emptyset$
107		eldifsn	$⊢ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in (𝒫 J ∖ \{\emptyset\}) \leftrightarrow (\{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in 𝒫 J \land \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \neq \emptyset)$
108	85 106 107	sylanbrc	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land x \in J) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in (𝒫 J ∖ \{\emptyset\})$
109	108	adantrl	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (w \in Z \land x \in J)) \to \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in (𝒫 J ∖ \{\emptyset\})$
110	109	ralrimivva	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to \forall w \in Z \forall x \in J \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in (𝒫 J ∖ \{\emptyset\})$
111	11	fmpo	$⊢ \forall w \in Z \forall x \in J \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\} \in (𝒫 J ∖ \{\emptyset\}) \leftrightarrow F : Z \times J ⟶ 𝒫 J ∖ \{\emptyset\}$
112	110 111	sylib	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to F : Z \times J ⟶ 𝒫 J ∖ \{\emptyset\}$
113	7	iftrued	$⊢ φ \to if (M \in ℤ, M, 0) = M$
114	113	fveq2d	$⊢ φ \to ℤ_{\geq if (M \in ℤ, M, 0)} = ℤ_{\geq M}$
115	114 1	eqtr4di	$⊢ φ \to ℤ_{\geq if (M \in ℤ, M, 0)} = Z$
116	115	xpeq1d	$⊢ φ \to ℤ_{\geq if (M \in ℤ, M, 0)} \times J = Z \times J$
117	116	feq2d	$⊢ φ \to (F : ℤ_{\geq if (M \in ℤ, M, 0)} \times J ⟶ 𝒫 J ∖ \{\emptyset\} \leftrightarrow F : Z \times J ⟶ 𝒫 J ∖ \{\emptyset\})$
118	117	biimpar	$⊢ (φ \land F : Z \times J ⟶ 𝒫 J ∖ \{\emptyset\}) \to F : ℤ_{\geq if (M \in ℤ, M, 0)} \times J ⟶ 𝒫 J ∖ \{\emptyset\}$
119	112 118	syldan	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to F : ℤ_{\geq if (M \in ℤ, M, 0)} \times J ⟶ 𝒫 J ∖ \{\emptyset\}$
120		0z	$⊢ 0 \in ℤ$
121	120	elimel	$⊢ if (M \in ℤ, M, 0) \in ℤ$
122		eqid	$⊢ ℤ_{\geq if (M \in ℤ, M, 0)} = ℤ_{\geq if (M \in ℤ, M, 0)}$
123	121 122	axdc4uz	$⊢ (J \in V \land g \in J \land F : ℤ_{\geq if (M \in ℤ, M, 0)} \times J ⟶ 𝒫 J ∖ \{\emptyset\}) \to \exists j (j : ℤ_{\geq if (M \in ℤ, M, 0)} ⟶ J \land j (if (M \in ℤ, M, 0)) = g \land \forall m \in ℤ_{\geq if (M \in ℤ, M, 0)} j (m + 1) \in (m F j (m)))$
124	26 43 119 123	syl3anc	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to \exists j (j : ℤ_{\geq if (M \in ℤ, M, 0)} ⟶ J \land j (if (M \in ℤ, M, 0)) = g \land \forall m \in ℤ_{\geq if (M \in ℤ, M, 0)} j (m + 1) \in (m F j (m)))$
125	27	iftrued	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to if (M \in ℤ, M, 0) = M$
126	125	fveq2d	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to ℤ_{\geq if (M \in ℤ, M, 0)} = ℤ_{\geq M}$
127	126 1	eqtr4di	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to ℤ_{\geq if (M \in ℤ, M, 0)} = Z$
128	127	feq2d	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to (j : ℤ_{\geq if (M \in ℤ, M, 0)} ⟶ J \leftrightarrow j : Z ⟶ J)$
129	89	abbii	$⊢ \{g \| \exists n \in Z (g : (M \dots n) ⟶ A \land ψ)\} = \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\}$
130	10 129	eqtri	$⊢ J = \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\}$
131		feq3	$⊢ J = \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \to (j : Z ⟶ J \leftrightarrow j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\})$
132	130 131	ax-mp	$⊢ j : Z ⟶ J \leftrightarrow j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\}$
133	128 132	bitrdi	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to (j : ℤ_{\geq if (M \in ℤ, M, 0)} ⟶ J \leftrightarrow j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\})$
134	125	fveqeq2d	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to (j (if (M \in ℤ, M, 0)) = g \leftrightarrow j (M) = g)$
135	127	raleqdv	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to (\forall m \in ℤ_{\geq if (M \in ℤ, M, 0)} j (m + 1) \in (m F j (m)) \leftrightarrow \forall m \in Z j (m + 1) \in (m F j (m)))$
136	133 134 135	3anbi123d	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to ((j : ℤ_{\geq if (M \in ℤ, M, 0)} ⟶ J \land j (if (M \in ℤ, M, 0)) = g \land \forall m \in ℤ_{\geq if (M \in ℤ, M, 0)} j (m + 1) \in (m F j (m))) \leftrightarrow (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m))))$
137	6	ad2antrr	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to A \in V$
138	7	ad2antrr	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to M \in ℤ$
139	8	ad2antrr	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to \exists g (g : \{M\} ⟶ A \land τ)$
140		simpll	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to φ$
141	140 9	sylan	$⊢ (((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \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 σ))$
142		nfv	$⊢ Ⅎ k (φ \land (g : \{M\} ⟶ A \land τ))$
143		nfcv	$⊢ \underline{Ⅎ} k j$
144		nfcv	$⊢ \underline{Ⅎ} k Z$
145		nfre1	$⊢ Ⅎ k \exists k \in Z (g : (M \dots k) ⟶ A \land θ)$
146	145	nfab	$⊢ \underline{Ⅎ} k \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\}$
147	143 144 146	nff	$⊢ Ⅎ k j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\}$
148		nfv	$⊢ Ⅎ k j (M) = g$
149		nfcv	$⊢ \underline{Ⅎ} k m$
150	130 146	nfcxfr	$⊢ \underline{Ⅎ} k J$
151		nfre1	$⊢ Ⅎ k \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)$
152	151	nfab	$⊢ \underline{Ⅎ} k \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\}$
153	144 150 152	nfmpo	$⊢ \underline{Ⅎ} k (w \in Z, x \in J ⟼ \{h \| \exists k \in Z (h : (M \dots k + 1) ⟶ A \land x = {h ↾}_{(M \dots k)} \land σ)\})$
154	11 153	nfcxfr	$⊢ \underline{Ⅎ} k F$
155		nfcv	$⊢ \underline{Ⅎ} k j (m)$
156	149 154 155	nfov	$⊢ \underline{Ⅎ} k (m F j (m))$
157	156	nfel2	$⊢ Ⅎ k j (m + 1) \in (m F j (m))$
158	144 157	nfralw	$⊢ Ⅎ k \forall m \in Z j (m + 1) \in (m F j (m))$
159	147 148 158	nf3an	$⊢ Ⅎ k (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))$
160	142 159	nfan	$⊢ Ⅎ k ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m))))$
161		simpr1	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\}$
162	161 132	sylibr	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to j : Z ⟶ J$
163	31	adantr	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to g : \{M\} ⟶ A$
164		simpr2	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to j (M) = g$
165	138 32	syl	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to (M \dots M) = \{M\}$
166	164 165	feq12d	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to (j (M) : (M \dots M) ⟶ A \leftrightarrow g : \{M\} ⟶ A)$
167	163 166	mpbird	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to j (M) : (M \dots M) ⟶ A$
168		simpr3	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to \forall m \in Z j (m + 1) \in (m F j (m))$
169		fvoveq1	$⊢ m = w \to j (m + 1) = j (w + 1)$
170		id	$⊢ m = w \to m = w$
171		fveq2	$⊢ m = w \to j (m) = j (w)$
172	170 171	oveq12d	$⊢ m = w \to m F j (m) = w F j (w)$
173	169 172	eleq12d	$⊢ m = w \to (j (m + 1) \in (m F j (m)) \leftrightarrow j (w + 1) \in (w F j (w)))$
174	173	rspccva	$⊢ (\forall m \in Z j (m + 1) \in (m F j (m)) \land w \in Z) \to j (w + 1) \in (w F j (w))$
175	168 174	sylan	$⊢ (((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \land w \in Z) \to j (w + 1) \in (w F j (w))$
176	1 2 3 4 5 137 138 139 141 10 11 160 162 167 175	sdclem2	$⊢ ((φ \land (g : \{M\} ⟶ A \land τ)) \land (j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m)))) \to \exists f (f : Z ⟶ A \land \forall n \in Z χ)$
177	176	ex	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to ((j : Z ⟶ \{g \| \exists k \in Z (g : (M \dots k) ⟶ A \land θ)\} \land j (M) = g \land \forall m \in Z j (m + 1) \in (m F j (m))) \to \exists f (f : Z ⟶ A \land \forall n \in Z χ))$
178	136 177	sylbid	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to ((j : ℤ_{\geq if (M \in ℤ, M, 0)} ⟶ J \land j (if (M \in ℤ, M, 0)) = g \land \forall m \in ℤ_{\geq if (M \in ℤ, M, 0)} j (m + 1) \in (m F j (m))) \to \exists f (f : Z ⟶ A \land \forall n \in Z χ))$
179	178	exlimdv	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to (\exists j (j : ℤ_{\geq if (M \in ℤ, M, 0)} ⟶ J \land j (if (M \in ℤ, M, 0)) = g \land \forall m \in ℤ_{\geq if (M \in ℤ, M, 0)} j (m + 1) \in (m F j (m))) \to \exists f (f : Z ⟶ A \land \forall n \in Z χ))$
180	124 179	mpd	$⊢ (φ \land (g : \{M\} ⟶ A \land τ)) \to \exists f (f : Z ⟶ A \land \forall n \in Z χ)$
181	8 180	exlimddv	$⊢ φ \to \exists f (f : Z ⟶ A \land \forall n \in Z χ)$

Metamath Proof Explorer

Theorem sdclem1

Proof