Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  efgsrel Structured version   Visualization version   GIF version

Theorem efgsrel 18354
 Description: The start and end of any extension sequence are related (i.e. evaluate to the same element of the quotient group to be created). (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
efgval.r = ( ~FG𝐼)
efgval2.m 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
efgval2.t 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
efgred.d 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
efgred.s 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
Assertion
Ref Expression
efgsrel (𝐹 ∈ dom 𝑆 → (𝐹‘0) (𝑆𝐹))
Distinct variable groups:   𝑦,𝑧   𝑡,𝑛,𝑣,𝑤,𝑦,𝑧,𝑚,𝑥   𝑚,𝑀   𝑥,𝑛,𝑀,𝑡,𝑣,𝑤   𝑘,𝑚,𝑡,𝑥,𝑇   𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥   ,𝑚,𝑡,𝑥,𝑦,𝑧   𝑚,𝐼,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧   𝐷,𝑚,𝑡
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑧,𝑤,𝑣,𝑘,𝑛)   (𝑤,𝑣,𝑘,𝑛)   𝑆(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝑇(𝑦,𝑧,𝑤,𝑣,𝑛)   𝐹(𝑥,𝑦,𝑧,𝑤,𝑣,𝑡,𝑘,𝑚,𝑛)   𝐼(𝑘)   𝑀(𝑦,𝑧,𝑘)

Proof of Theorem efgsrel
Dummy variables 𝑎 𝑖 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . . . . 6 𝑊 = ( I ‘Word (𝐼 × 2𝑜))
2 efgval.r . . . . . 6 = ( ~FG𝐼)
3 efgval2.m . . . . . 6 𝑀 = (𝑦𝐼, 𝑧 ∈ 2𝑜 ↦ ⟨𝑦, (1𝑜𝑧)⟩)
4 efgval2.t . . . . . 6 𝑇 = (𝑣𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2𝑜) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀𝑤)”⟩⟩)))
5 efgred.d . . . . . 6 𝐷 = (𝑊 𝑥𝑊 ran (𝑇𝑥))
6 efgred.s . . . . . 6 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
71, 2, 3, 4, 5, 6efgsdm 18350 . . . . 5 (𝐹 ∈ dom 𝑆 ↔ (𝐹 ∈ (Word 𝑊 ∖ {∅}) ∧ (𝐹‘0) ∈ 𝐷 ∧ ∀𝑎 ∈ (1..^(♯‘𝐹))(𝐹𝑎) ∈ ran (𝑇‘(𝐹‘(𝑎 − 1)))))
87simp1bi 1139 . . . 4 (𝐹 ∈ dom 𝑆𝐹 ∈ (Word 𝑊 ∖ {∅}))
9 eldifsn 4453 . . . . 5 (𝐹 ∈ (Word 𝑊 ∖ {∅}) ↔ (𝐹 ∈ Word 𝑊𝐹 ≠ ∅))
10 lennncl 13521 . . . . 5 ((𝐹 ∈ Word 𝑊𝐹 ≠ ∅) → (♯‘𝐹) ∈ ℕ)
119, 10sylbi 207 . . . 4 (𝐹 ∈ (Word 𝑊 ∖ {∅}) → (♯‘𝐹) ∈ ℕ)
12 fzo0end 12768 . . . 4 ((♯‘𝐹) ∈ ℕ → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
138, 11, 123syl 18 . . 3 (𝐹 ∈ dom 𝑆 → ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)))
14 nnm1nn0 11536 . . . . 5 ((♯‘𝐹) ∈ ℕ → ((♯‘𝐹) − 1) ∈ ℕ0)
158, 11, 143syl 18 . . . 4 (𝐹 ∈ dom 𝑆 → ((♯‘𝐹) − 1) ∈ ℕ0)
16 eleq1 2838 . . . . . . 7 (𝑎 = 0 → (𝑎 ∈ (0..^(♯‘𝐹)) ↔ 0 ∈ (0..^(♯‘𝐹))))
17 fveq2 6332 . . . . . . . 8 (𝑎 = 0 → (𝐹𝑎) = (𝐹‘0))
1817breq2d 4798 . . . . . . 7 (𝑎 = 0 → ((𝐹‘0) (𝐹𝑎) ↔ (𝐹‘0) (𝐹‘0)))
1916, 18imbi12d 333 . . . . . 6 (𝑎 = 0 → ((𝑎 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑎)) ↔ (0 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘0))))
2019imbi2d 329 . . . . 5 (𝑎 = 0 → ((𝐹 ∈ dom 𝑆 → (𝑎 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑎))) ↔ (𝐹 ∈ dom 𝑆 → (0 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘0)))))
21 eleq1 2838 . . . . . . 7 (𝑎 = 𝑖 → (𝑎 ∈ (0..^(♯‘𝐹)) ↔ 𝑖 ∈ (0..^(♯‘𝐹))))
22 fveq2 6332 . . . . . . . 8 (𝑎 = 𝑖 → (𝐹𝑎) = (𝐹𝑖))
2322breq2d 4798 . . . . . . 7 (𝑎 = 𝑖 → ((𝐹‘0) (𝐹𝑎) ↔ (𝐹‘0) (𝐹𝑖)))
2421, 23imbi12d 333 . . . . . 6 (𝑎 = 𝑖 → ((𝑎 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑎)) ↔ (𝑖 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑖))))
2524imbi2d 329 . . . . 5 (𝑎 = 𝑖 → ((𝐹 ∈ dom 𝑆 → (𝑎 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑎))) ↔ (𝐹 ∈ dom 𝑆 → (𝑖 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑖)))))
26 eleq1 2838 . . . . . . 7 (𝑎 = (𝑖 + 1) → (𝑎 ∈ (0..^(♯‘𝐹)) ↔ (𝑖 + 1) ∈ (0..^(♯‘𝐹))))
27 fveq2 6332 . . . . . . . 8 (𝑎 = (𝑖 + 1) → (𝐹𝑎) = (𝐹‘(𝑖 + 1)))
2827breq2d 4798 . . . . . . 7 (𝑎 = (𝑖 + 1) → ((𝐹‘0) (𝐹𝑎) ↔ (𝐹‘0) (𝐹‘(𝑖 + 1))))
2926, 28imbi12d 333 . . . . . 6 (𝑎 = (𝑖 + 1) → ((𝑎 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑎)) ↔ ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘(𝑖 + 1)))))
3029imbi2d 329 . . . . 5 (𝑎 = (𝑖 + 1) → ((𝐹 ∈ dom 𝑆 → (𝑎 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑎))) ↔ (𝐹 ∈ dom 𝑆 → ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘(𝑖 + 1))))))
31 eleq1 2838 . . . . . . 7 (𝑎 = ((♯‘𝐹) − 1) → (𝑎 ∈ (0..^(♯‘𝐹)) ↔ ((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹))))
32 fveq2 6332 . . . . . . . 8 (𝑎 = ((♯‘𝐹) − 1) → (𝐹𝑎) = (𝐹‘((♯‘𝐹) − 1)))
3332breq2d 4798 . . . . . . 7 (𝑎 = ((♯‘𝐹) − 1) → ((𝐹‘0) (𝐹𝑎) ↔ (𝐹‘0) (𝐹‘((♯‘𝐹) − 1))))
3431, 33imbi12d 333 . . . . . 6 (𝑎 = ((♯‘𝐹) − 1) → ((𝑎 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑎)) ↔ (((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘((♯‘𝐹) − 1)))))
3534imbi2d 329 . . . . 5 (𝑎 = ((♯‘𝐹) − 1) → ((𝐹 ∈ dom 𝑆 → (𝑎 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑎))) ↔ (𝐹 ∈ dom 𝑆 → (((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘((♯‘𝐹) − 1))))))
361, 2efger 18338 . . . . . . . 8 Er 𝑊
3736a1i 11 . . . . . . 7 ((𝐹 ∈ dom 𝑆 ∧ 0 ∈ (0..^(♯‘𝐹))) → Er 𝑊)
38 eldifi 3883 . . . . . . . . 9 (𝐹 ∈ (Word 𝑊 ∖ {∅}) → 𝐹 ∈ Word 𝑊)
39 wrdf 13506 . . . . . . . . 9 (𝐹 ∈ Word 𝑊𝐹:(0..^(♯‘𝐹))⟶𝑊)
408, 38, 393syl 18 . . . . . . . 8 (𝐹 ∈ dom 𝑆𝐹:(0..^(♯‘𝐹))⟶𝑊)
4140ffvelrnda 6502 . . . . . . 7 ((𝐹 ∈ dom 𝑆 ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝐹‘0) ∈ 𝑊)
4237, 41erref 7916 . . . . . 6 ((𝐹 ∈ dom 𝑆 ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝐹‘0) (𝐹‘0))
4342ex 397 . . . . 5 (𝐹 ∈ dom 𝑆 → (0 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘0)))
44 elnn0uz 11927 . . . . . . . . . . . 12 (𝑖 ∈ ℕ0𝑖 ∈ (ℤ‘0))
45 peano2fzor 12783 . . . . . . . . . . . 12 ((𝑖 ∈ (ℤ‘0) ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → 𝑖 ∈ (0..^(♯‘𝐹)))
4644, 45sylanb 570 . . . . . . . . . . 11 ((𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → 𝑖 ∈ (0..^(♯‘𝐹)))
47463adant1 1124 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → 𝑖 ∈ (0..^(♯‘𝐹)))
48473expia 1114 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0) → ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → 𝑖 ∈ (0..^(♯‘𝐹))))
4948imim1d 82 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0) → ((𝑖 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑖)) → ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑖))))
50403ad2ant1 1127 . . . . . . . . . . . . 13 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → 𝐹:(0..^(♯‘𝐹))⟶𝑊)
5150, 47ffvelrnd 6503 . . . . . . . . . . . 12 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝐹𝑖) ∈ 𝑊)
52 fvoveq1 6816 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑖 + 1) → (𝐹‘(𝑎 − 1)) = (𝐹‘((𝑖 + 1) − 1)))
5352fveq2d 6336 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑖 + 1) → (𝑇‘(𝐹‘(𝑎 − 1))) = (𝑇‘(𝐹‘((𝑖 + 1) − 1))))
5453rneqd 5491 . . . . . . . . . . . . . . 15 (𝑎 = (𝑖 + 1) → ran (𝑇‘(𝐹‘(𝑎 − 1))) = ran (𝑇‘(𝐹‘((𝑖 + 1) − 1))))
5527, 54eleq12d 2844 . . . . . . . . . . . . . 14 (𝑎 = (𝑖 + 1) → ((𝐹𝑎) ∈ ran (𝑇‘(𝐹‘(𝑎 − 1))) ↔ (𝐹‘(𝑖 + 1)) ∈ ran (𝑇‘(𝐹‘((𝑖 + 1) − 1)))))
567simp3bi 1141 . . . . . . . . . . . . . . 15 (𝐹 ∈ dom 𝑆 → ∀𝑎 ∈ (1..^(♯‘𝐹))(𝐹𝑎) ∈ ran (𝑇‘(𝐹‘(𝑎 − 1))))
57563ad2ant1 1127 . . . . . . . . . . . . . 14 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → ∀𝑎 ∈ (1..^(♯‘𝐹))(𝐹𝑎) ∈ ran (𝑇‘(𝐹‘(𝑎 − 1))))
58 nn0p1nn 11534 . . . . . . . . . . . . . . . . 17 (𝑖 ∈ ℕ0 → (𝑖 + 1) ∈ ℕ)
59583ad2ant2 1128 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝑖 + 1) ∈ ℕ)
60 nnuz 11925 . . . . . . . . . . . . . . . 16 ℕ = (ℤ‘1)
6159, 60syl6eleq 2860 . . . . . . . . . . . . . . 15 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝑖 + 1) ∈ (ℤ‘1))
62 elfzolt2b 12689 . . . . . . . . . . . . . . . 16 ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝑖 + 1) ∈ ((𝑖 + 1)..^(♯‘𝐹)))
63623ad2ant3 1129 . . . . . . . . . . . . . . 15 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝑖 + 1) ∈ ((𝑖 + 1)..^(♯‘𝐹)))
64 elfzo3 12694 . . . . . . . . . . . . . . 15 ((𝑖 + 1) ∈ (1..^(♯‘𝐹)) ↔ ((𝑖 + 1) ∈ (ℤ‘1) ∧ (𝑖 + 1) ∈ ((𝑖 + 1)..^(♯‘𝐹))))
6561, 63, 64sylanbrc 572 . . . . . . . . . . . . . 14 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝑖 + 1) ∈ (1..^(♯‘𝐹)))
6655, 57, 65rspcdva 3466 . . . . . . . . . . . . 13 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝐹‘(𝑖 + 1)) ∈ ran (𝑇‘(𝐹‘((𝑖 + 1) − 1))))
67 nn0cn 11504 . . . . . . . . . . . . . . . . . 18 (𝑖 ∈ ℕ0𝑖 ∈ ℂ)
68673ad2ant2 1128 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → 𝑖 ∈ ℂ)
69 ax-1cn 10196 . . . . . . . . . . . . . . . . 17 1 ∈ ℂ
70 pncan 10489 . . . . . . . . . . . . . . . . 17 ((𝑖 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑖 + 1) − 1) = 𝑖)
7168, 69, 70sylancl 574 . . . . . . . . . . . . . . . 16 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → ((𝑖 + 1) − 1) = 𝑖)
7271fveq2d 6336 . . . . . . . . . . . . . . 15 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝐹‘((𝑖 + 1) − 1)) = (𝐹𝑖))
7372fveq2d 6336 . . . . . . . . . . . . . 14 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝑇‘(𝐹‘((𝑖 + 1) − 1))) = (𝑇‘(𝐹𝑖)))
7473rneqd 5491 . . . . . . . . . . . . 13 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → ran (𝑇‘(𝐹‘((𝑖 + 1) − 1))) = ran (𝑇‘(𝐹𝑖)))
7566, 74eleqtrd 2852 . . . . . . . . . . . 12 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝐹‘(𝑖 + 1)) ∈ ran (𝑇‘(𝐹𝑖)))
761, 2, 3, 4efgi2 18345 . . . . . . . . . . . 12 (((𝐹𝑖) ∈ 𝑊 ∧ (𝐹‘(𝑖 + 1)) ∈ ran (𝑇‘(𝐹𝑖))) → (𝐹𝑖) (𝐹‘(𝑖 + 1)))
7751, 75, 76syl2anc 573 . . . . . . . . . . 11 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (𝐹𝑖) (𝐹‘(𝑖 + 1)))
7836a1i 11 . . . . . . . . . . . 12 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → Er 𝑊)
7978ertr 7911 . . . . . . . . . . 11 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → (((𝐹‘0) (𝐹𝑖) ∧ (𝐹𝑖) (𝐹‘(𝑖 + 1))) → (𝐹‘0) (𝐹‘(𝑖 + 1))))
8077, 79mpan2d 674 . . . . . . . . . 10 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0 ∧ (𝑖 + 1) ∈ (0..^(♯‘𝐹))) → ((𝐹‘0) (𝐹𝑖) → (𝐹‘0) (𝐹‘(𝑖 + 1))))
81803expia 1114 . . . . . . . . 9 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0) → ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → ((𝐹‘0) (𝐹𝑖) → (𝐹‘0) (𝐹‘(𝑖 + 1)))))
8281a2d 29 . . . . . . . 8 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0) → (((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑖)) → ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘(𝑖 + 1)))))
8349, 82syld 47 . . . . . . 7 ((𝐹 ∈ dom 𝑆𝑖 ∈ ℕ0) → ((𝑖 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑖)) → ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘(𝑖 + 1)))))
8483expcom 398 . . . . . 6 (𝑖 ∈ ℕ0 → (𝐹 ∈ dom 𝑆 → ((𝑖 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑖)) → ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘(𝑖 + 1))))))
8584a2d 29 . . . . 5 (𝑖 ∈ ℕ0 → ((𝐹 ∈ dom 𝑆 → (𝑖 ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹𝑖))) → (𝐹 ∈ dom 𝑆 → ((𝑖 + 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘(𝑖 + 1))))))
8620, 25, 30, 35, 43, 85nn0ind 11674 . . . 4 (((♯‘𝐹) − 1) ∈ ℕ0 → (𝐹 ∈ dom 𝑆 → (((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘((♯‘𝐹) − 1)))))
8715, 86mpcom 38 . . 3 (𝐹 ∈ dom 𝑆 → (((♯‘𝐹) − 1) ∈ (0..^(♯‘𝐹)) → (𝐹‘0) (𝐹‘((♯‘𝐹) − 1))))
8813, 87mpd 15 . 2 (𝐹 ∈ dom 𝑆 → (𝐹‘0) (𝐹‘((♯‘𝐹) − 1)))
891, 2, 3, 4, 5, 6efgsval 18351 . 2 (𝐹 ∈ dom 𝑆 → (𝑆𝐹) = (𝐹‘((♯‘𝐹) − 1)))
9088, 89breqtrrd 4814 1 (𝐹 ∈ dom 𝑆 → (𝐹‘0) (𝑆𝐹))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ∀wral 3061  {crab 3065   ∖ cdif 3720  ∅c0 4063  {csn 4316  ⟨cop 4322  ⟨cotp 4324  ∪ ciun 4654   class class class wbr 4786   ↦ cmpt 4863   I cid 5156   × cxp 5247  dom cdm 5249  ran crn 5250  ⟶wf 6027  ‘cfv 6031  (class class class)co 6793   ↦ cmpt2 6795  1𝑜c1o 7706  2𝑜c2o 7707   Er wer 7893  ℂcc 10136  0cc0 10138  1c1 10139   + caddc 10141   − cmin 10468  ℕcn 11222  ℕ0cn0 11494  ℤ≥cuz 11888  ...cfz 12533  ..^cfzo 12673  ♯chash 13321  Word cword 13487   splice csplice 13492  ⟨“cs2 13795   ~FG cefg 18326 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-ot 4325  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-ec 7898  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-n0 11495  df-z 11580  df-uz 11889  df-fz 12534  df-fzo 12674  df-hash 13322  df-word 13495  df-concat 13497  df-s1 13498  df-substr 13499  df-splice 13500  df-s2 13802  df-efg 18329 This theorem is referenced by:  efgredeu  18372  efgred2  18373
 Copyright terms: Public domain W3C validator