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

Theorem efgrelexlemb 19618
Description: If two words 𝐴, 𝐡 are related under the free group equivalence, then there exist two extension sequences π‘Ž, 𝑏 such that π‘Ž ends at 𝐴, 𝑏 ends at 𝐡, and π‘Ž and 𝐡 have the same starting point. (Contributed by Mario Carneiro, 1-Oct-2015.)
Hypotheses
Ref Expression
efgval.w π‘Š = ( I β€˜Word (𝐼 Γ— 2o))
efgval.r ∼ = ( ~FG β€˜πΌ)
efgval2.m 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)
efgval2.t 𝑇 = (𝑣 ∈ π‘Š ↦ (𝑛 ∈ (0...(β™―β€˜π‘£)), 𝑀 ∈ (𝐼 Γ— 2o) ↦ (𝑣 splice βŸ¨π‘›, 𝑛, βŸ¨β€œπ‘€(π‘€β€˜π‘€)β€βŸ©βŸ©)))
efgred.d 𝐷 = (π‘Š βˆ– βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯))
efgred.s 𝑆 = (π‘š ∈ {𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))} ↦ (π‘šβ€˜((β™―β€˜π‘š) βˆ’ 1)))
efgrelexlem.1 𝐿 = {βŸ¨π‘–, π‘—βŸ© ∣ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑖})βˆƒπ‘‘ ∈ (◑𝑆 β€œ {𝑗})(π‘β€˜0) = (π‘‘β€˜0)}
Assertion
Ref Expression
efgrelexlemb ∼ βŠ† 𝐿
Distinct variable groups:   𝑐,𝑑,𝑖,𝑗   𝑦,𝑧   𝑛,𝑐,𝑑,𝑣,𝑀,𝑦,𝑧,π‘š,π‘₯   𝑀,𝑐   𝑖,π‘š,𝑛,𝑑,𝑣,𝑀,π‘₯,𝑀,𝑗   π‘˜,𝑐,𝑇,𝑖,𝑗,π‘š,𝑑,π‘₯   π‘Š,𝑐   π‘˜,𝑑,π‘š,𝑛,𝑑,𝑣,𝑀,π‘₯,𝑦,𝑧,π‘Š,𝑖,𝑗   ∼ ,𝑐,𝑑,𝑖,𝑗,π‘š,𝑑,π‘₯,𝑦,𝑧   𝑆,𝑐,𝑑,𝑖,𝑗   𝐼,𝑐,𝑖,𝑗,π‘š,𝑛,𝑑,𝑣,𝑀,π‘₯,𝑦,𝑧   𝐷,𝑐,𝑑,𝑖,𝑗,π‘š,𝑑
Allowed substitution hints:   𝐷(π‘₯,𝑦,𝑧,𝑀,𝑣,π‘˜,𝑛)   ∼ (𝑀,𝑣,π‘˜,𝑛)   𝑆(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑑,π‘˜,π‘š,𝑛)   𝑇(𝑦,𝑧,𝑀,𝑣,𝑛,𝑑)   𝐼(π‘˜,𝑑)   𝐿(π‘₯,𝑦,𝑧,𝑀,𝑣,𝑑,𝑖,𝑗,π‘˜,π‘š,𝑛,𝑐,𝑑)   𝑀(𝑦,𝑧,π‘˜,𝑑)

Proof of Theorem efgrelexlemb
Dummy variables π‘Ž 𝑏 𝑓 𝑔 β„Ž π‘Ÿ 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 efgval.w . . 3 π‘Š = ( I β€˜Word (𝐼 Γ— 2o))
2 efgval.r . . 3 ∼ = ( ~FG β€˜πΌ)
3 efgval2.m . . 3 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ βŸ¨π‘¦, (1o βˆ– 𝑧)⟩)
4 efgval2.t . . 3 𝑇 = (𝑣 ∈ π‘Š ↦ (𝑛 ∈ (0...(β™―β€˜π‘£)), 𝑀 ∈ (𝐼 Γ— 2o) ↦ (𝑣 splice βŸ¨π‘›, 𝑛, βŸ¨β€œπ‘€(π‘€β€˜π‘€)β€βŸ©βŸ©)))
51, 2, 3, 4efgval2 19592 . 2 ∼ = ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)}
6 efgrelexlem.1 . . . . . . . 8 𝐿 = {βŸ¨π‘–, π‘—βŸ© ∣ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑖})βˆƒπ‘‘ ∈ (◑𝑆 β€œ {𝑗})(π‘β€˜0) = (π‘‘β€˜0)}
76relopabiv 5821 . . . . . . 7 Rel 𝐿
87a1i 11 . . . . . 6 (⊀ β†’ Rel 𝐿)
9 simpr 486 . . . . . . 7 ((⊀ ∧ 𝑓𝐿𝑔) β†’ 𝑓𝐿𝑔)
10 eqcom 2740 . . . . . . . . . 10 ((π‘Žβ€˜0) = (π‘β€˜0) ↔ (π‘β€˜0) = (π‘Žβ€˜0))
11102rexbii 3130 . . . . . . . . 9 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘β€˜0) = (π‘Žβ€˜0))
12 rexcom 3288 . . . . . . . . 9 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘β€˜0) = (π‘Žβ€˜0) ↔ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})(π‘β€˜0) = (π‘Žβ€˜0))
1311, 12bitri 275 . . . . . . . 8 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ↔ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})(π‘β€˜0) = (π‘Žβ€˜0))
14 efgred.d . . . . . . . . 9 𝐷 = (π‘Š βˆ– βˆͺ π‘₯ ∈ π‘Š ran (π‘‡β€˜π‘₯))
15 efgred.s . . . . . . . . 9 𝑆 = (π‘š ∈ {𝑑 ∈ (Word π‘Š βˆ– {βˆ…}) ∣ ((π‘‘β€˜0) ∈ 𝐷 ∧ βˆ€π‘˜ ∈ (1..^(β™―β€˜π‘‘))(π‘‘β€˜π‘˜) ∈ ran (π‘‡β€˜(π‘‘β€˜(π‘˜ βˆ’ 1))))} ↦ (π‘šβ€˜((β™―β€˜π‘š) βˆ’ 1)))
161, 2, 3, 4, 14, 15, 6efgrelexlema 19617 . . . . . . . 8 (𝑓𝐿𝑔 ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0))
171, 2, 3, 4, 14, 15, 6efgrelexlema 19617 . . . . . . . 8 (𝑔𝐿𝑓 ↔ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})(π‘β€˜0) = (π‘Žβ€˜0))
1813, 16, 173bitr4i 303 . . . . . . 7 (𝑓𝐿𝑔 ↔ 𝑔𝐿𝑓)
199, 18sylib 217 . . . . . 6 ((⊀ ∧ 𝑓𝐿𝑔) β†’ 𝑔𝐿𝑓)
201, 2, 3, 4, 14, 15, 6efgrelexlema 19617 . . . . . . . . 9 (π‘”πΏβ„Ž ↔ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0))
21 reeanv 3227 . . . . . . . . . 10 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})(βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) ↔ (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)))
221, 2, 3, 4, 14, 15efgsfo 19607 . . . . . . . . . . . . . . . . . . . 20 𝑆:dom 𝑆–ontoβ†’π‘Š
23 fofn 6808 . . . . . . . . . . . . . . . . . . . 20 (𝑆:dom 𝑆–ontoβ†’π‘Š β†’ 𝑆 Fn dom 𝑆)
2422, 23ax-mp 5 . . . . . . . . . . . . . . . . . . 19 𝑆 Fn dom 𝑆
25 fniniseg 7062 . . . . . . . . . . . . . . . . . . 19 (𝑆 Fn dom 𝑆 β†’ (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = 𝑔)))
2624, 25ax-mp 5 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = 𝑔))
27 fniniseg 7062 . . . . . . . . . . . . . . . . . . 19 (𝑆 Fn dom 𝑆 β†’ (𝑏 ∈ (◑𝑆 β€œ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘) = 𝑔)))
2824, 27ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (◑𝑆 β€œ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘) = 𝑔))
29 eqtr3 2759 . . . . . . . . . . . . . . . . . . . 20 (((π‘†β€˜π‘Ÿ) = 𝑔 ∧ (π‘†β€˜π‘) = 𝑔) β†’ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘))
301, 2, 3, 4, 14, 15efgred 19616 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘)) β†’ (π‘Ÿβ€˜0) = (π‘β€˜0))
3130eqcomd 2739 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘)) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
32313expa 1119 . . . . . . . . . . . . . . . . . . . 20 (((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) ∧ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘)) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
3329, 32sylan2 594 . . . . . . . . . . . . . . . . . . 19 (((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) ∧ ((π‘†β€˜π‘Ÿ) = 𝑔 ∧ (π‘†β€˜π‘) = 𝑔)) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
3433an4s 659 . . . . . . . . . . . . . . . . . 18 (((π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = 𝑔) ∧ (𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘) = 𝑔)) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
3526, 28, 34syl2anb 599 . . . . . . . . . . . . . . . . 17 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
36 eqeq2 2745 . . . . . . . . . . . . . . . . 17 ((π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ ((π‘β€˜0) = (π‘Ÿβ€˜0) ↔ (π‘β€˜0) = (π‘ β€˜0)))
3735, 36syl5ibcom 244 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ ((π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ (π‘β€˜0) = (π‘ β€˜0)))
3837reximdv 3171 . . . . . . . . . . . . . . 15 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘β€˜0) = (π‘ β€˜0)))
39 eqeq1 2737 . . . . . . . . . . . . . . . . 17 ((π‘Žβ€˜0) = (π‘β€˜0) β†’ ((π‘Žβ€˜0) = (π‘ β€˜0) ↔ (π‘β€˜0) = (π‘ β€˜0)))
4039rexbidv 3179 . . . . . . . . . . . . . . . 16 ((π‘Žβ€˜0) = (π‘β€˜0) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0) ↔ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘β€˜0) = (π‘ β€˜0)))
4140imbi2d 341 . . . . . . . . . . . . . . 15 ((π‘Žβ€˜0) = (π‘β€˜0) β†’ ((βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0)) ↔ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘β€˜0) = (π‘ β€˜0))))
4238, 41syl5ibrcom 246 . . . . . . . . . . . . . 14 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ ((π‘Žβ€˜0) = (π‘β€˜0) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))))
4342rexlimdva 3156 . . . . . . . . . . . . 13 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) β†’ (βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))))
4443impd 412 . . . . . . . . . . . 12 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) β†’ ((βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0)))
4544rexlimiv 3149 . . . . . . . . . . 11 (βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})(βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
4645reximi 3085 . . . . . . . . . 10 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})(βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
4721, 46sylbir 234 . . . . . . . . 9 ((βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
4816, 20, 47syl2anb 599 . . . . . . . 8 ((𝑓𝐿𝑔 ∧ π‘”πΏβ„Ž) β†’ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
491, 2, 3, 4, 14, 15, 6efgrelexlema 19617 . . . . . . . 8 (π‘“πΏβ„Ž ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
5048, 49sylibr 233 . . . . . . 7 ((𝑓𝐿𝑔 ∧ π‘”πΏβ„Ž) β†’ π‘“πΏβ„Ž)
5150adantl 483 . . . . . 6 ((⊀ ∧ (𝑓𝐿𝑔 ∧ π‘”πΏβ„Ž)) β†’ π‘“πΏβ„Ž)
52 eqid 2733 . . . . . . . . . . . 12 (π‘Žβ€˜0) = (π‘Žβ€˜0)
53 fveq1 6891 . . . . . . . . . . . . 13 (𝑏 = π‘Ž β†’ (π‘β€˜0) = (π‘Žβ€˜0))
5453rspceeqv 3634 . . . . . . . . . . . 12 ((π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ (π‘Žβ€˜0) = (π‘Žβ€˜0)) β†’ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
5552, 54mpan2 690 . . . . . . . . . . 11 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) β†’ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
5655pm4.71i 561 . . . . . . . . . 10 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0)))
57 fniniseg 7062 . . . . . . . . . . 11 (𝑆 Fn dom 𝑆 β†’ (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓)))
5824, 57ax-mp 5 . . . . . . . . . 10 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓))
5956, 58bitr3i 277 . . . . . . . . 9 ((π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0)) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓))
6059rexbii2 3091 . . . . . . . 8 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0) ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓)
611, 2, 3, 4, 14, 15, 6efgrelexlema 19617 . . . . . . . 8 (𝑓𝐿𝑓 ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
62 forn 6809 . . . . . . . . . . 11 (𝑆:dom 𝑆–ontoβ†’π‘Š β†’ ran 𝑆 = π‘Š)
6322, 62ax-mp 5 . . . . . . . . . 10 ran 𝑆 = π‘Š
6463eleq2i 2826 . . . . . . . . 9 (𝑓 ∈ ran 𝑆 ↔ 𝑓 ∈ π‘Š)
65 fvelrnb 6953 . . . . . . . . . 10 (𝑆 Fn dom 𝑆 β†’ (𝑓 ∈ ran 𝑆 ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓))
6624, 65ax-mp 5 . . . . . . . . 9 (𝑓 ∈ ran 𝑆 ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓)
6764, 66bitr3i 277 . . . . . . . 8 (𝑓 ∈ π‘Š ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓)
6860, 61, 673bitr4ri 304 . . . . . . 7 (𝑓 ∈ π‘Š ↔ 𝑓𝐿𝑓)
6968a1i 11 . . . . . 6 (⊀ β†’ (𝑓 ∈ π‘Š ↔ 𝑓𝐿𝑓))
708, 19, 51, 69iserd 8729 . . . . 5 (⊀ β†’ 𝐿 Er π‘Š)
7170mptru 1549 . . . 4 𝐿 Er π‘Š
72 simpl 484 . . . . . . . . . . 11 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ π‘Ž ∈ π‘Š)
73 foelrn 7108 . . . . . . . . . . 11 ((𝑆:dom 𝑆–ontoβ†’π‘Š ∧ π‘Ž ∈ π‘Š) β†’ βˆƒπ‘Ÿ ∈ dom 𝑆 π‘Ž = (π‘†β€˜π‘Ÿ))
7422, 72, 73sylancr 588 . . . . . . . . . 10 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ βˆƒπ‘Ÿ ∈ dom 𝑆 π‘Ž = (π‘†β€˜π‘Ÿ))
75 simprl 770 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ dom 𝑆)
76 simprr 772 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ž = (π‘†β€˜π‘Ÿ))
7776eqcomd 2739 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘†β€˜π‘Ÿ) = π‘Ž)
78 fniniseg 7062 . . . . . . . . . . . 12 (𝑆 Fn dom 𝑆 β†’ (π‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = π‘Ž)))
7924, 78ax-mp 5 . . . . . . . . . . 11 (π‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = π‘Ž))
8075, 77, 79sylanbrc 584 . . . . . . . . . 10 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž}))
81 simplr 768 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 𝑏 ∈ ran (π‘‡β€˜π‘Ž))
8276fveq2d 6896 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘‡β€˜π‘Ž) = (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
8382rneqd 5938 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ ran (π‘‡β€˜π‘Ž) = ran (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
8481, 83eleqtrd 2836 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 𝑏 ∈ ran (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
851, 2, 3, 4, 14, 15efgsp1 19605 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ ran (π‘‡β€˜(π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆)
8675, 84, 85syl2anc 585 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆)
871, 2, 3, 4, 14, 15efgsdm 19598 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ dom 𝑆 ↔ (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) ∧ (π‘Ÿβ€˜0) ∈ 𝐷 ∧ βˆ€π‘– ∈ (1..^(β™―β€˜π‘Ÿ))(π‘Ÿβ€˜π‘–) ∈ ran (π‘‡β€˜(π‘Ÿβ€˜(𝑖 βˆ’ 1)))))
8887simp1bi 1146 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ dom 𝑆 β†’ π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}))
8988ad2antrl 727 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}))
9089eldifad 3961 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ Word π‘Š)
911, 2, 3, 4efgtf 19590 . . . . . . . . . . . . . . . . 17 (π‘Ž ∈ π‘Š β†’ ((π‘‡β€˜π‘Ž) = (𝑓 ∈ (0...(β™―β€˜π‘Ž)), 𝑔 ∈ (𝐼 Γ— 2o) ↦ (π‘Ž splice βŸ¨π‘“, 𝑓, βŸ¨β€œπ‘”(π‘€β€˜π‘”)β€βŸ©βŸ©)) ∧ (π‘‡β€˜π‘Ž):((0...(β™―β€˜π‘Ž)) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š))
9291simprd 497 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ π‘Š β†’ (π‘‡β€˜π‘Ž):((0...(β™―β€˜π‘Ž)) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š)
9392frnd 6726 . . . . . . . . . . . . . . 15 (π‘Ž ∈ π‘Š β†’ ran (π‘‡β€˜π‘Ž) βŠ† π‘Š)
9493sselda 3983 . . . . . . . . . . . . . 14 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ 𝑏 ∈ π‘Š)
9594adantr 482 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 𝑏 ∈ π‘Š)
961, 2, 3, 4, 14, 15efgsval2 19601 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ Word π‘Š ∧ 𝑏 ∈ π‘Š ∧ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆) β†’ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)
9790, 95, 86, 96syl3anc 1372 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)
98 fniniseg 7062 . . . . . . . . . . . . 13 (𝑆 Fn dom 𝑆 β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ↔ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆 ∧ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)))
9924, 98ax-mp 5 . . . . . . . . . . . 12 ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ↔ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆 ∧ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏))
10086, 97, 99sylanbrc 584 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}))
10195s1cld 14553 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word π‘Š)
102 eldifsn 4791 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) ↔ (π‘Ÿ ∈ Word π‘Š ∧ π‘Ÿ β‰  βˆ…))
103 lennncl 14484 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ Word π‘Š ∧ π‘Ÿ β‰  βˆ…) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
104102, 103sylbi 216 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
10589, 104syl 17 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
106 lbfzo0 13672 . . . . . . . . . . . . . 14 (0 ∈ (0..^(β™―β€˜π‘Ÿ)) ↔ (β™―β€˜π‘Ÿ) ∈ β„•)
107105, 106sylibr 233 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 0 ∈ (0..^(β™―β€˜π‘Ÿ)))
108 ccatval1 14527 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ Word π‘Š ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word π‘Š ∧ 0 ∈ (0..^(β™―β€˜π‘Ÿ))) β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Ÿβ€˜0))
10990, 101, 107, 108syl3anc 1372 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Ÿβ€˜0))
110109eqcomd 2739 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿβ€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0))
111 fveq1 6891 . . . . . . . . . . . 12 (𝑠 = (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) β†’ (π‘ β€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0))
112111rspceeqv 3634 . . . . . . . . . . 11 (((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ∧ (π‘Ÿβ€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
113100, 110, 112syl2anc 585 . . . . . . . . . 10 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
11474, 80, 113reximssdv 3173 . . . . . . . . 9 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž})βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
1151, 2, 3, 4, 14, 15, 6efgrelexlema 19617 . . . . . . . . 9 (π‘ŽπΏπ‘ ↔ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž})βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
116114, 115sylibr 233 . . . . . . . 8 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ π‘ŽπΏπ‘)
117 vex 3479 . . . . . . . . 9 𝑏 ∈ V
118 vex 3479 . . . . . . . . 9 π‘Ž ∈ V
119117, 118elec 8747 . . . . . . . 8 (𝑏 ∈ [π‘Ž]𝐿 ↔ π‘ŽπΏπ‘)
120116, 119sylibr 233 . . . . . . 7 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ 𝑏 ∈ [π‘Ž]𝐿)
121120ex 414 . . . . . 6 (π‘Ž ∈ π‘Š β†’ (𝑏 ∈ ran (π‘‡β€˜π‘Ž) β†’ 𝑏 ∈ [π‘Ž]𝐿))
122121ssrdv 3989 . . . . 5 (π‘Ž ∈ π‘Š β†’ ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿)
123122rgen 3064 . . . 4 βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿
1241fvexi 6906 . . . . . 6 π‘Š ∈ V
125 erex 8727 . . . . . 6 (𝐿 Er π‘Š β†’ (π‘Š ∈ V β†’ 𝐿 ∈ V))
12671, 124, 125mp2 9 . . . . 5 𝐿 ∈ V
127 ereq1 8710 . . . . . 6 (π‘Ÿ = 𝐿 β†’ (π‘Ÿ Er π‘Š ↔ 𝐿 Er π‘Š))
128 eceq2 8743 . . . . . . . 8 (π‘Ÿ = 𝐿 β†’ [π‘Ž]π‘Ÿ = [π‘Ž]𝐿)
129128sseq2d 4015 . . . . . . 7 (π‘Ÿ = 𝐿 β†’ (ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ ↔ ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
130129ralbidv 3178 . . . . . 6 (π‘Ÿ = 𝐿 β†’ (βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ ↔ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
131127, 130anbi12d 632 . . . . 5 (π‘Ÿ = 𝐿 β†’ ((π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ) ↔ (𝐿 Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿)))
132126, 131elab 3669 . . . 4 (𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} ↔ (𝐿 Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
13371, 123, 132mpbir2an 710 . . 3 𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)}
134 intss1 4968 . . 3 (𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} β†’ ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} βŠ† 𝐿)
135133, 134ax-mp 5 . 2 ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} βŠ† 𝐿
1365, 135eqsstri 4017 1 ∼ βŠ† 𝐿
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107  {cab 2710   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆ– cdif 3946   βŠ† wss 3949  βˆ…c0 4323  {csn 4629  βŸ¨cop 4635  βŸ¨cotp 4637  βˆ© cint 4951  βˆͺ ciun 4998   class class class wbr 5149  {copab 5211   ↦ cmpt 5232   I cid 5574   Γ— cxp 5675  β—‘ccnv 5676  dom cdm 5677  ran crn 5678   β€œ cima 5680  Rel wrel 5682   Fn wfn 6539  βŸΆwf 6540  β€“ontoβ†’wfo 6542  β€˜cfv 6544  (class class class)co 7409   ∈ cmpo 7411  1oc1o 8459  2oc2o 8460   Er wer 8700  [cec 8701  0cc0 11110  1c1 11111   βˆ’ cmin 11444  β„•cn 12212  ...cfz 13484  ..^cfzo 13627  β™―chash 14290  Word cword 14464   ++ cconcat 14520  βŸ¨β€œcs1 14545   splice csplice 14699  βŸ¨β€œcs2 14792   ~FG cefg 19574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-ot 4638  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-er 8703  df-ec 8705  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-n0 12473  df-xnn0 12545  df-z 12559  df-uz 12823  df-rp 12975  df-fz 13485  df-fzo 13628  df-hash 14291  df-word 14465  df-concat 14521  df-s1 14546  df-substr 14591  df-pfx 14621  df-splice 14700  df-s2 14799  df-efg 19577
This theorem is referenced by:  efgrelex  19619
  Copyright terms: Public domain W3C validator