Theorem fdc1

Description: Variant of fdc with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010)

	Ref	Expression
Hypotheses	fdc1.1	$$⊢A\in \mathrm{V}$$
	fdc1.2	$$⊢M\in \mathbb{Z}$$
	fdc1.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	fdc1.4	$$⊢N=M+1$$
	fdc1.5	$$⊢a=f\left(M\right)\to \left(\zeta \leftrightarrow \sigma \right)$$
	fdc1.6	$$⊢a=f\left(k-1\right)\to \left(\phi \leftrightarrow \psi \right)$$
	fdc1.7	$$⊢b=f\left(k\right)\to \left(\psi \leftrightarrow \chi \right)$$
	fdc1.8	$$⊢a=f\left(n\right)\to \left(\theta \leftrightarrow \tau \right)$$
	fdc1.9	$$⊢\eta \to \exists a\in A\zeta$$
	fdc1.10	$$⊢\eta \to R\mathrm{Fr}A$$
	fdc1.11	$$⊢\left(\eta \wedge a\in A\right)\to \left(\theta \vee \exists b\in A\phi \right)$$
	fdc1.12	$$⊢\left(\left(\eta \wedge \phi \right)\wedge \left(a\in A\wedge b\in A\right)\right)\to bRa$$
Assertion	fdc1	$$⊢\eta \to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		fdc1.1	$$⊢A\in \mathrm{V}$$
2		fdc1.2	$$⊢M\in \mathbb{Z}$$
3		fdc1.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		fdc1.4	$$⊢N=M+1$$
5		fdc1.5	$$⊢a=f\left(M\right)\to \left(\zeta \leftrightarrow \sigma \right)$$
6		fdc1.6	$$⊢a=f\left(k-1\right)\to \left(\phi \leftrightarrow \psi \right)$$
7		fdc1.7	$$⊢b=f\left(k\right)\to \left(\psi \leftrightarrow \chi \right)$$
8		fdc1.8	$$⊢a=f\left(n\right)\to \left(\theta \leftrightarrow \tau \right)$$
9		fdc1.9	$$⊢\eta \to \exists a\in A\zeta$$
10		fdc1.10	$$⊢\eta \to R\mathrm{Fr}A$$
11		fdc1.11	$$⊢\left(\eta \wedge a\in A\right)\to \left(\theta \vee \exists b\in A\phi \right)$$
12		fdc1.12	$$⊢\left(\left(\eta \wedge \phi \right)\wedge \left(a\in A\wedge b\in A\right)\right)\to bRa$$
13		eleq1w	$$⊢c=a\to \left(c\in A\leftrightarrow a\in A\right)$$
14	13	anbi2d	$$⊢c=a\to \left(\left(\eta \wedge c\in A\right)\leftrightarrow \left(\eta \wedge a\in A\right)\right)$$
15		sbceq2a	$$⊢c=a\to \left(\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \leftrightarrow \zeta \right)$$
16	14 15	anbi12d	$$⊢c=a\to \left(\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\leftrightarrow \left(\left(\eta \wedge a\in A\right)\wedge \zeta \right)\right)$$
17	16	imbi1d	$$⊢c=a\to \left(\left(\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)\right)\leftrightarrow \left(\left(\left(\eta \wedge a\in A\right)\wedge \zeta \right)\to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)\right)\right)$$
18		sbsbc	$$⊢\left[d/a\right]\phi \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi$$
19		nfv	$$⊢Ⅎa\psi$$
20	19 6	sbhypf	$$⊢d=f\left(k-1\right)\to \left(\left[d/a\right]\phi \leftrightarrow \psi \right)$$
21	18 20	bitr3id	$$⊢d=f\left(k-1\right)\to \left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
22		sbsbc	$$⊢\left[d/a\right]\theta \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta$$
23		nfv	$$⊢Ⅎa\tau$$
24	23 8	sbhypf	$$⊢d=f\left(n\right)\to \left(\left[d/a\right]\theta \leftrightarrow \tau \right)$$
25	22 24	bitr3id	$$⊢d=f\left(n\right)\to \left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta \leftrightarrow \tau \right)$$
26		simprl	$$⊢\left(\eta \wedge \left(c\in A\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\right)\to c\in A$$
27	10	adantr	$$⊢\left(\eta \wedge \left(c\in A\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\right)\to R\mathrm{Fr}A$$
28		nfv	$$⊢Ⅎa\left(\eta \wedge d\in A\right)$$
29		nfsbc1v	$$⊢Ⅎa\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}aA$$
31		nfsbc1v	$$⊢Ⅎa\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi$$
32	30 31	nfrexw	$$⊢Ⅎa\exists b\in A\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi$$
33	29 32	nfor	$$⊢Ⅎa\left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta \vee \exists b\in A\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
34	28 33	nfim	$$⊢Ⅎa\left(\left(\eta \wedge d\in A\right)\to \left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta \vee \exists b\in A\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\right)$$
35		eleq1w	$$⊢a=d\to \left(a\in A\leftrightarrow d\in A\right)$$
36	35	anbi2d	$$⊢a=d\to \left(\left(\eta \wedge a\in A\right)\leftrightarrow \left(\eta \wedge d\in A\right)\right)$$
37		sbceq1a	$$⊢a=d\to \left(\theta \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta \right)$$
38		sbceq1a	$$⊢a=d\to \left(\phi \leftrightarrow \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
39	38	rexbidv	$$⊢a=d\to \left(\exists b\in A\phi \leftrightarrow \exists b\in A\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
40	37 39	orbi12d	$$⊢a=d\to \left(\left(\theta \vee \exists b\in A\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta \vee \exists b\in A\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\right)$$
41	36 40	imbi12d	$$⊢a=d\to \left(\left(\left(\eta \wedge a\in A\right)\to \left(\theta \vee \exists b\in A\phi \right)\right)\leftrightarrow \left(\left(\eta \wedge d\in A\right)\to \left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta \vee \exists b\in A\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\right)\right)$$
42	34 41 11	chvarfv	$$⊢\left(\eta \wedge d\in A\right)\to \left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta \vee \exists b\in A\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
43	42	adantlr	$$⊢\left(\left(\eta \wedge \left(c\in A\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\right)\wedge d\in A\right)\to \left(\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\theta \vee \exists b\in A\underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
44		nfv	$$⊢Ⅎa\eta$$
45	44 31	nfan	$$⊢Ⅎa\left(\eta \wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)$$
46		nfv	$$⊢Ⅎa\left(d\in A\wedge b\in A\right)$$
47	45 46	nfan	$$⊢Ⅎa\left(\left(\eta \wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\wedge \left(d\in A\wedge b\in A\right)\right)$$
48		nfv	$$⊢ℲabRd$$
49	47 48	nfim	$$⊢Ⅎa\left(\left(\left(\eta \wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\wedge \left(d\in A\wedge b\in A\right)\right)\to bRd\right)$$
50	38	anbi2d	$$⊢a=d\to \left(\left(\eta \wedge \phi \right)\leftrightarrow \left(\eta \wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\right)$$
51	35	anbi1d	$$⊢a=d\to \left(\left(a\in A\wedge b\in A\right)\leftrightarrow \left(d\in A\wedge b\in A\right)\right)$$
52	50 51	anbi12d	$$⊢a=d\to \left(\left(\left(\eta \wedge \phi \right)\wedge \left(a\in A\wedge b\in A\right)\right)\leftrightarrow \left(\left(\eta \wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\wedge \left(d\in A\wedge b\in A\right)\right)\right)$$
53		breq2	$$⊢a=d\to \left(bRa\leftrightarrow bRd\right)$$
54	52 53	imbi12d	$$⊢a=d\to \left(\left(\left(\left(\eta \wedge \phi \right)\wedge \left(a\in A\wedge b\in A\right)\right)\to bRa\right)\leftrightarrow \left(\left(\left(\eta \wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\wedge \left(d\in A\wedge b\in A\right)\right)\to bRd\right)\right)$$
55	49 54 12	chvarfv	$$⊢\left(\left(\eta \wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\wedge \left(d\in A\wedge b\in A\right)\right)\to bRd$$
56	55	adantllr	$$⊢\left(\left(\left(\eta \wedge \left(c\in A\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\right)\wedge \underset{\dot{}}{[}d/a\underset{\dot{}}{]}\phi \right)\wedge \left(d\in A\wedge b\in A\right)\right)\to bRd$$
57	1 2 3 4 21 7 25 26 27 43 56	fdc	$$⊢\left(\eta \wedge \left(c\in A\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\right)\to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(f\left(M\right)=c\wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)$$
58	57	anassrs	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(f\left(M\right)=c\wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)$$
59		idd	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \left(f:\left(M\dots n\right)⟶A\to f:\left(M\dots n\right)⟶A\right)$$
60		dfsbcq	$$⊢f\left(M\right)=c\to \left(\underset{\dot{}}{[}f\left(M\right)/a\underset{\dot{}}{]}\zeta \leftrightarrow \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)$$
61		fvex	$$⊢f\left(M\right)\in \mathrm{V}$$
62	61 5	sbcie	$$⊢\underset{\dot{}}{[}f\left(M\right)/a\underset{\dot{}}{]}\zeta \leftrightarrow \sigma$$
63	60 62	bitr3di	$$⊢f\left(M\right)=c\to \left(\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \leftrightarrow \sigma \right)$$
64	63	biimpcd	$$⊢\underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \to \left(f\left(M\right)=c\to \sigma \right)$$
65	64	adantl	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \left(f\left(M\right)=c\to \sigma \right)$$
66	65	anim1d	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \left(\left(f\left(M\right)=c\wedge \tau \right)\to \left(\sigma \wedge \tau \right)\right)$$
67		idd	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \left(\forall k\in \left(N\dots n\right)\chi \to \forall k\in \left(N\dots n\right)\chi \right)$$
68	59 66 67	3anim123d	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \left(\left(f:\left(M\dots n\right)⟶A\wedge \left(f\left(M\right)=c\wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)\to \left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)\right)$$
69	68	eximdv	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \left(\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(f\left(M\right)=c\wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)\to \exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)\right)$$
70	69	reximdv	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \left(\exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(f\left(M\right)=c\wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)\to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)\right)$$
71	58 70	mpd	$$⊢\left(\left(\eta \wedge c\in A\right)\wedge \underset{\dot{}}{[}c/a\underset{\dot{}}{]}\zeta \right)\to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)$$
72	17 71	chvarvv	$$⊢\left(\left(\eta \wedge a\in A\right)\wedge \zeta \right)\to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)$$
73	72 9	r19.29a	$$⊢\eta \to \exists n\in Z\exists f\left(f:\left(M\dots n\right)⟶A\wedge \left(\sigma \wedge \tau \right)\wedge \forall k\in \left(N\dots n\right)\chi \right)$$