Metamath Proof Explorer

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 nfrex ⊢ Ⅎ 𝑎 ∃ 𝑏 ∈ 𝐴 [ 𝑑 / 𝑎 ] 𝜑
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 ⊢ ( 𝜂 → ∃ 𝑛 ∈ 𝑍 ∃ 𝑓 ( 𝑓 : ( 𝑀 ... 𝑛 ) ⟶ 𝐴 ∧ ( 𝜎 ∧ 𝜏 ) ∧ ∀ 𝑘 ∈ ( 𝑁 ... 𝑛 ) 𝜒 ) )