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 19978

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 6911	. . . . 5 ⊢ (𝑓 = 𝐹 → (♯‘𝑓) = (♯‘𝐹))
3	2	oveq1d 7461	. . . 4 ⊢ (𝑓 = 𝐹 → ((♯‘𝑓) − 1) = ((♯‘𝐹) − 1))
4	1, 3	fveq12d 6918	. . 3 ⊢ (𝑓 = 𝐹 → (𝑓‘((♯‘𝑓) − 1)) = (𝐹‘((♯‘𝐹) − 1)))
5		efgred.s	. . . 4 ⊢ 𝑆 = (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1)))
6		id 23	. . . . . 6 ⊢ (𝑚 = 𝑓 → 𝑚 = 𝑓)
7		fveq2 6911	. . . . . . 7 ⊢ (𝑚 = 𝑓 → (♯‘𝑚) = (♯‘𝑓))
8	7	oveq1d 7461	. . . . . 6 ⊢ (𝑚 = 𝑓 → ((♯‘𝑚) − 1) = ((♯‘𝑓) − 1))
9	6, 8	fveq12d 6918	. . . . 5 ⊢ (𝑚 = 𝑓 → (𝑚‘((♯‘𝑚) − 1)) = (𝑓‘((♯‘𝑓) − 1)))
10	9	cbvmptv 5213	. . . 4 ⊢ (𝑚 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑚‘((♯‘𝑚) − 1))) = (𝑓 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑓‘((♯‘𝑓) − 1)))
11	5, 10	eqtri 2786	. . 3 ⊢ 𝑆 = (𝑓 ∈ {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))} ↦ (𝑓‘((♯‘𝑓) − 1)))
12		fvex 6924	. . 3 ⊢ (𝐹‘((♯‘𝐹) − 1)) ∈ V
13	4, 11, 12	fvmpt 7019	. 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 19976	. . 3 ⊢ 𝑆:{𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}⟶𝑊
20	19	fdmi 6746	. 2 ⊢ dom 𝑆 = {𝑡 ∈ (Word 𝑊 ∖ {∅}) ∣ ((𝑡‘0) ∈ 𝐷 ∧ ∀𝑘 ∈ (1..^(♯‘𝑡))(𝑡‘𝑘) ∈ ran (𝑇‘(𝑡‘(𝑘 − 1))))}
21	13, 20	eleq2s 2882	1 ⊢ (𝐹 ∈ dom 𝑆 → (𝑆‘𝐹) = (𝐹‘((♯‘𝐹) − 1)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ∀wral 3080 {crab 3416 ∖ cdif 4048 ∅c0 4281 {csn 4588 ⟨cop 4838 ⟨cotp 4861 ∪ ciun 4954 ↦ cmpt 5190 I cid 5550 × cxp 5654 dom cdm 5656 ran crn 5657 ‘cfv 6561 (class class class)co 7446 ∈ cmpo 7448 1_oc1o 8500 2_oc2o 8501 0cc0 11230 1c1 11231 − cmin 11571 ...cfz 13669 ..^cfzo 13818 ♯chash 14504 Word cword 14688 splice csplice 14929 ⟨“cs2 15023 ~_FG cefg 19953

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778 ax-cnex 11286 ax-resscn 11287 ax-1cn 11288 ax-icn 11289 ax-addcl 11290 ax-addrcl 11291 ax-mulcl 11292 ax-mulrcl 11293 ax-mulcom 11294 ax-addass 11295 ax-mulass 11296 ax-distr 11297 ax-i2m1 11298 ax-1ne0 11299 ax-1rid 11300 ax-rnegex 11301 ax-rrecex 11302 ax-cnre 11303 ax-pre-lttri 11304 ax-pre-lttrn 11305 ax-pre-ltadd 11306 ax-pre-mulgt0 11307

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-om 7905 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-rdg 8449 df-1o 8507 df-er 8748 df-en 9005 df-dom 9006 df-sdom 9007 df-fin 9008 df-card 10050 df-pnf 11375 df-mnf 11376 df-xr 11377 df-ltxr 11378 df-le 11379 df-sub 11573 df-neg 11574 df-nn 12366 df-n0 12637 df-z 12724 df-uz 12996 df-fz 13670 df-fzo 13819 df-hash 14505 df-word 14689

This theorem is used by: efgsdmi 19979 efgsval2 19980 efgsrel 19981 efgs1b 19983 efgsp1 19984 efgsfo 19986 efgredlema 19987 efgredlemd 19991 efgredlem 19994 efgredeu 19999

W3C validator