Theorem fdc1

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

	Ref	Expression
Hypotheses	fdc1.1	⊢ 𝐴 ∈ V
	fdc1.2	⊢ 𝑀 ∈ ℤ
	fdc1.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	fdc1.4	⊢ 𝑁 = ( 𝑀 + 1 )
	fdc1.5	⊢ ( 𝑎 = ( 𝑓 ‘ 𝑀 ) → ( 𝜁 ↔ 𝜎 ) )
	fdc1.6	⊢ ( 𝑎 = ( 𝑓 ‘ ( 𝑘 − 1 ) ) → ( 𝜑 ↔ 𝜓 ) )
	fdc1.7	⊢ ( 𝑏 = ( 𝑓 ‘ 𝑘 ) → ( 𝜓 ↔ 𝜒 ) )
	fdc1.8	⊢ ( 𝑎 = ( 𝑓 ‘ 𝑛 ) → ( 𝜃 ↔ 𝜏 ) )
	fdc1.9	⊢ ( 𝜂 → ∃ 𝑎 ∈ 𝐴 𝜁 )
	fdc1.10	⊢ ( 𝜂 → 𝑅 Fr 𝐴 )
	fdc1.11	⊢ ( ( 𝜂 ∧ 𝑎 ∈ 𝐴 ) → ( 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 𝜑 ) )
	fdc1.12	⊢ ( ( ( 𝜂 ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 𝑅 𝑎 )
Assertion	fdc1	⊢ ( 𝜂 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		fdc1.1	⊢ 𝐴 ∈ V
2		fdc1.2	⊢ 𝑀 ∈ ℤ
3		fdc1.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		fdc1.4	⊢ 𝑁 = ( 𝑀 + 1 )
5		fdc1.5	⊢ ( 𝑎 = ( 𝑓 ‘ 𝑀 ) → ( 𝜁 ↔ 𝜎 ) )
6		fdc1.6	⊢ ( 𝑎 = ( 𝑓 ‘ ( 𝑘 − 1 ) ) → ( 𝜑 ↔ 𝜓 ) )
7		fdc1.7	⊢ ( 𝑏 = ( 𝑓 ‘ 𝑘 ) → ( 𝜓 ↔ 𝜒 ) )
8		fdc1.8	⊢ ( 𝑎 = ( 𝑓 ‘ 𝑛 ) → ( 𝜃 ↔ 𝜏 ) )
9		fdc1.9	⊢ ( 𝜂 → ∃ 𝑎 ∈ 𝐴 𝜁 )
10		fdc1.10	⊢ ( 𝜂 → 𝑅 Fr 𝐴 )
11		fdc1.11	⊢ ( ( 𝜂 ∧ 𝑎 ∈ 𝐴 ) → ( 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 𝜑 ) )
12		fdc1.12	⊢ ( ( ( 𝜂 ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 𝑅 𝑎 )
13		eleq1w	⊢ ( 𝑐 = 𝑎 → ( 𝑐 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴 ) )
14	13	anbi2d	⊢ ( 𝑐 = 𝑎 → ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ↔ ( 𝜂 ∧ 𝑎 ∈ 𝐴 ) ) )
15		sbceq2a	⊢ ( 𝑐 = 𝑎 → ( [ 𝑐 / 𝑎 ] 𝜁 ↔ 𝜁 ) )
16	14 15	anbi12d	⊢ ( 𝑐 = 𝑎 → ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) ↔ ( ( 𝜂 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝜁 ) ) )
17	16	imbi1d	⊢ ( 𝑐 = 𝑎 → ( ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) ↔ ( ( ( 𝜂 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝜁 ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) ) )
18		sbsbc	⊢ ( [ 𝑑 / 𝑎 ] 𝜑 ↔ [ 𝑑 / 𝑎 ] 𝜑 )
19		nfv	⊢ Ⅎ 𝑎 𝜓
20	19 6	sbhypf	⊢ ( 𝑑 = ( 𝑓 ‘ ( 𝑘 − 1 ) ) → ( [ 𝑑 / 𝑎 ] 𝜑 ↔ 𝜓 ) )
21	18 20	bitr3id	⊢ ( 𝑑 = ( 𝑓 ‘ ( 𝑘 − 1 ) ) → ( [ 𝑑 / 𝑎 ] 𝜑 ↔ 𝜓 ) )
22		sbsbc	⊢ ( [ 𝑑 / 𝑎 ] 𝜃 ↔ [ 𝑑 / 𝑎 ] 𝜃 )
23		nfv	⊢ Ⅎ 𝑎 𝜏
24	23 8	sbhypf	⊢ ( 𝑑 = ( 𝑓 ‘ 𝑛 ) → ( [ 𝑑 / 𝑎 ] 𝜃 ↔ 𝜏 ) )
25	22 24	bitr3id	⊢ ( 𝑑 = ( 𝑓 ‘ 𝑛 ) → ( [ 𝑑 / 𝑎 ] 𝜃 ↔ 𝜏 ) )
26		simprl	⊢ ( ( 𝜂 ∧ ( 𝑐 ∈ 𝐴 ∧ [ 𝑐 / 𝑎 ] 𝜁 ) ) → 𝑐 ∈ 𝐴 )
27	10	adantr	⊢ ( ( 𝜂 ∧ ( 𝑐 ∈ 𝐴 ∧ [ 𝑐 / 𝑎 ] 𝜁 ) ) → 𝑅 Fr 𝐴 )
28		nfv	⊢ Ⅎ 𝑎 ( 𝜂 ∧ 𝑑 ∈ 𝐴 )
29		nfsbc1v	⊢ Ⅎ 𝑎 [ 𝑑 / 𝑎 ] 𝜃
30		nfcv	⊢ Ⅎ 𝑎 𝐴
31		nfsbc1v	⊢ Ⅎ 𝑎 [ 𝑑 / 𝑎 ] 𝜑
32	30 31	nfrexw	⊢ Ⅎ 𝑎 ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑
33	29 32	nfor	⊢ Ⅎ 𝑎 ( [ 𝑑 / 𝑎 ] 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑 )
34	28 33	nfim	⊢ Ⅎ 𝑎 ( ( 𝜂 ∧ 𝑑 ∈ 𝐴 ) → ( [ 𝑑 / 𝑎 ] 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑 ) )
35		eleq1w	⊢ ( 𝑎 = 𝑑 → ( 𝑎 ∈ 𝐴 ↔ 𝑑 ∈ 𝐴 ) )
36	35	anbi2d	⊢ ( 𝑎 = 𝑑 → ( ( 𝜂 ∧ 𝑎 ∈ 𝐴 ) ↔ ( 𝜂 ∧ 𝑑 ∈ 𝐴 ) ) )
37		sbceq1a	⊢ ( 𝑎 = 𝑑 → ( 𝜃 ↔ [ 𝑑 / 𝑎 ] 𝜃 ) )
38		sbceq1a	⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ [ 𝑑 / 𝑎 ] 𝜑 ) )
39	38	rexbidv	⊢ ( 𝑎 = 𝑑 → ( ∃ 𝑏 ∈ 𝐴 𝜑 ↔ ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑 ) )
40	37 39	orbi12d	⊢ ( 𝑎 = 𝑑 → ( ( 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 𝜑 ) ↔ ( [ 𝑑 / 𝑎 ] 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑 ) ) )
41	36 40	imbi12d	⊢ ( 𝑎 = 𝑑 → ( ( ( 𝜂 ∧ 𝑎 ∈ 𝐴 ) → ( 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 𝜑 ) ) ↔ ( ( 𝜂 ∧ 𝑑 ∈ 𝐴 ) → ( [ 𝑑 / 𝑎 ] 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑 ) ) ) )
42	34 41 11	chvarfv	⊢ ( ( 𝜂 ∧ 𝑑 ∈ 𝐴 ) → ( [ 𝑑 / 𝑎 ] 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑 ) )
43	42	adantlr	⊢ ( ( ( 𝜂 ∧ ( 𝑐 ∈ 𝐴 ∧ [ 𝑐 / 𝑎 ] 𝜁 ) ) ∧ 𝑑 ∈ 𝐴 ) → ( [ 𝑑 / 𝑎 ] 𝜃 ∨ ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑 ) )
44		nfv	⊢ Ⅎ 𝑎 𝜂
45	44 31	nfan	⊢ Ⅎ 𝑎 ( 𝜂 ∧ [ 𝑑 / 𝑎 ] 𝜑 )
46		nfv	⊢ Ⅎ 𝑎 ( 𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 )
47	45 46	nfan	⊢ Ⅎ 𝑎 ( ( 𝜂 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) )
48		nfv	⊢ Ⅎ 𝑎 𝑏 𝑅 𝑑
49	47 48	nfim	⊢ Ⅎ 𝑎 ( ( ( 𝜂 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 𝑅 𝑑 )
50	38	anbi2d	⊢ ( 𝑎 = 𝑑 → ( ( 𝜂 ∧ 𝜑 ) ↔ ( 𝜂 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ) )
51	35	anbi1d	⊢ ( 𝑎 = 𝑑 → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) )
52	50 51	anbi12d	⊢ ( 𝑎 = 𝑑 → ( ( ( 𝜂 ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ↔ ( ( 𝜂 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) ) )
53		breq2	⊢ ( 𝑎 = 𝑑 → ( 𝑏 𝑅 𝑎 ↔ 𝑏 𝑅 𝑑 ) )
54	52 53	imbi12d	⊢ ( 𝑎 = 𝑑 → ( ( ( ( 𝜂 ∧ 𝜑 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 𝑅 𝑎 ) ↔ ( ( ( 𝜂 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 𝑅 𝑑 ) ) )
55	49 54 12	chvarfv	⊢ ( ( ( 𝜂 ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 𝑅 𝑑 )
56	55	adantllr	⊢ ( ( ( ( 𝜂 ∧ ( 𝑐 ∈ 𝐴 ∧ [ 𝑐 / 𝑎 ] 𝜁 ) ) ∧ [ 𝑑 / 𝑎 ] 𝜑 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) ) → 𝑏 𝑅 𝑑 )
57	1 2 3 4 21 7 25 26 27 43 56	fdc	⊢ ( ( 𝜂 ∧ ( 𝑐 ∈ 𝐴 ∧ [ 𝑐 / 𝑎 ] 𝜁 ) ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
58	57	anassrs	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
59		idd	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 → 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ) )
60		dfsbcq	⊢ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 → ( [ ( 𝑓 ‘ 𝑀 ) / 𝑎 ] 𝜁 ↔ [ 𝑐 / 𝑎 ] 𝜁 ) )
61		fvex	⊢ ( 𝑓 ‘ 𝑀 ) ∈ V
62	61 5	sbcie	⊢ ( [ ( 𝑓 ‘ 𝑀 ) / 𝑎 ] 𝜁 ↔ 𝜎 )
63	60 62	bitr3di	⊢ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 → ( [ 𝑐 / 𝑎 ] 𝜁 ↔ 𝜎 ) )
64	63	biimpcd	⊢ ( [ 𝑐 / 𝑎 ] 𝜁 → ( ( 𝑓 ‘ 𝑀 ) = 𝑐 → 𝜎 ) )
65	64	adantl	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ( ( 𝑓 ‘ 𝑀 ) = 𝑐 → 𝜎 ) )
66	65	anim1d	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ( ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) → ( 𝜎 ∧ 𝜏 ) ) )
67		idd	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ( ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 → ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
68	59 66 67	3anim123d	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ( ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) → ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
69	68	eximdv	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ( ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) → ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
70	69	reximdv	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ( ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( ( 𝑓 ‘ 𝑀 ) = 𝑐 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) ) )
71	58 70	mpd	⊢ ( ( ( 𝜂 ∧ 𝑐 ∈ 𝐴 ) ∧ [ 𝑐 / 𝑎 ] 𝜁 ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
72	17 71	chvarvv	⊢ ( ( ( 𝜂 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝜁 ) → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )
73	72 9	r19.29a	⊢ ( 𝜂 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )