efgsval - Metamath Proof Explorer

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

Theorem efgsval 19832

Description: Value of the auxiliary function 𝑆 defining a sequence of extensions. (Contributed by Mario Carneiro, 27-Sep-2015.)

**Hypotheses**
Ref	Expression
efgval.w	⊢ 𝑊 = ( I ‘Word (𝐼 × 2_o))
efgval.r	⊢ ∼ = ( ~_FG ‘𝐼)
efgval2.m	⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_o ↦ ⟨𝑦, (1_o ∖ 𝑧)⟩)
efgval2.t	⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2_o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
efgred.d	⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
efgred.s	⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))

**Assertion**
Ref	Expression
efgsval	⊢ (𝐹 ∈ dom 𝑆 → (𝑆‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))

Distinct variable groups: 𝑦,𝑧 𝑡,𝑛,𝑣,𝑤,𝑦,𝑧,𝑚,𝑥 𝑚,𝑀 𝑥,𝑛,𝑀,𝑡,𝑣,𝑤 𝑘,𝑚,𝑡,𝑥,𝑇 𝑘,𝑛,𝑣,𝑤,𝑦,𝑧,𝑊,𝑚,𝑡,𝑥 ∼ ,𝑚,𝑡,𝑥,𝑦,𝑧 𝑚,𝐼,𝑛,𝑡,𝑣,𝑤,𝑥,𝑦,𝑧 𝐷,𝑚,𝑡 Allowed substitution hints: 𝐷(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑘, 𝑛) ∼ (𝑤, 𝑣, 𝑘, 𝑛) 𝑆(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑡, 𝑘, 𝑚, 𝑛) 𝑇(𝑦, 𝑧, 𝑤, 𝑣, 𝑛) 𝐹(𝑥, 𝑦, 𝑧, 𝑤, 𝑣, 𝑡, 𝑘, 𝑚, 𝑛) 𝐼(𝑘) 𝑀(𝑦, 𝑧, 𝑘)

Proof of Theorem efgsval Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 23	. . . 4 ⊢ (𝑓 = 𝐹 → 𝑓 = 𝐹)
2		fveq2 6888	. . . . 5 ⊢ (𝑓 = 𝐹 → (♯‘𝑓) = (♯‘𝐹))
3	2	oveq1d 7438	. . . 4 ⊢ (𝑓 = 𝐹 → ((♯‘𝑓) − 1) = ((♯‘𝐹) − 1))
4	1, 3	fveq12d 6895	. . 3 ⊢ (𝑓 = 𝐹 → (𝑓‘((♯‘𝑓) − 1)) = (𝐹‘((♯‘𝐹) − 1)))
5		efgred.s	. . . 4 ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
6		id 23	. . . . . 6 ⊢ (𝑚 = 𝑓 → 𝑚 = 𝑓)
7		fveq2 6888	. . . . . . 7 ⊢ (𝑚 = 𝑓 → (♯‘𝑚) = (♯‘𝑓))
8	7	oveq1d 7438	. . . . . 6 ⊢ (𝑚 = 𝑓 → ((♯‘𝑚) − 1) = ((♯‘𝑓) − 1))
9	6, 8	fveq12d 6895	. . . . 5 ⊢ (𝑚 = 𝑓 → (𝑚‘((♯‘𝑚) − 1)) = (𝑓‘((♯‘𝑓) − 1)))
10	9	cbvmptv 5220	. . . 4 ⊢ (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1))) = (𝑓 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑓‘((♯‘𝑓) − 1)))
11	5, 10	eqtri 2789	. . 3 ⊢ 𝑆 = (𝑓 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑓‘((♯‘𝑓) − 1)))
12		fvex 6901	. . 3 ⊢ (𝐹‘((♯‘𝐹) − 1)) ∈ V
13	4, 11, 12	fvmpt 6996	. 2 ⊢ (𝐹 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} → (𝑆‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))
14		efgval.w	. . . 4 ⊢ 𝑊 = ( I ‘Word (𝐼 × 2_o))
15		efgval.r	. . . 4 ⊢ ∼ = ( ~_FG ‘𝐼)
16		efgval2.m	. . . 4 ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2_o ↦ ⟨𝑦, (1_o ∖ 𝑧)⟩)
17		efgval2.t	. . . 4 ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2_o) ↦ (𝑣 splice ⟨𝑛, 𝑛, ⟨“𝑤(𝑀‘𝑤)”⟩⟩)))
18		efgred.d	. . . 4 ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥))
19	14, 15, 16, 17, 18, 5	efgsf 19830	. . 3 ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
20	19	fdmi 6724	. 2 ⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
21	13, 20	eleq2s 2884	1 ⊢ (𝐹 ∈ dom 𝑆 → (𝑆‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ∀wral 3082 {crab 3419 ∖ cdif 3905 ∅c0 4289 {csn 4594 ⟨cop 4600 ⟨cotp 4602 ∪ ciun 4961 ↦ cmpt 5197 I cid 5560 × cxp 5664 dom cdm 5666 ran crn 5667 ‘cfv 6543 (class class class)co 7423 ∈ cmpo 7425 1_oc1o 8455 2_oc2o 8456 0cc0 11118 1c1 11119 − cmin 11459 ...cfz 13553 ..^cfzo 13701 ♯chash 14386 Word cword 14570 splice csplice 14810 ⟨“cs2 14904 ~_FG cefg 19807

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-om 7872 df-1st 7995 df-2nd 7996 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-er 8703 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-card 9944 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-nn 12252 df-n0 12523 df-z 12610 df-uz 12881 df-fz 13554 df-fzo 13702 df-hash 14387 df-word 14571

This theorem is used by: efgsdmi 19833 efgsval2 19834 efgsrel 19835 efgs1b 19837 efgsp1 19838 efgsfo 19840 efgredlema 19841 efgredlemd 19845 efgredlem 19848 efgredeu 19853

W3C validator