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

Theorem efgrelexlemb 19532
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 19506 . 2 ∼ = ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)}
6 efgrelexlem.1 . . . . . . . 8 𝐿 = {βŸ¨π‘–, π‘—βŸ© ∣ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑖})βˆƒπ‘‘ ∈ (◑𝑆 β€œ {𝑗})(π‘β€˜0) = (π‘‘β€˜0)}
76relopabiv 5776 . . . . . . 7 Rel 𝐿
87a1i 11 . . . . . 6 (⊀ β†’ Rel 𝐿)
9 simpr 485 . . . . . . 7 ((⊀ ∧ 𝑓𝐿𝑔) β†’ 𝑓𝐿𝑔)
10 eqcom 2743 . . . . . . . . . 10 ((π‘Žβ€˜0) = (π‘β€˜0) ↔ (π‘β€˜0) = (π‘Žβ€˜0))
11102rexbii 3128 . . . . . . . . 9 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘β€˜0) = (π‘Žβ€˜0))
12 rexcom 3273 . . . . . . . . 9 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘β€˜0) = (π‘Žβ€˜0) ↔ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})(π‘β€˜0) = (π‘Žβ€˜0))
1311, 12bitri 274 . . . . . . . 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 19531 . . . . . . . 8 (𝑓𝐿𝑔 ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0))
171, 2, 3, 4, 14, 15, 6efgrelexlema 19531 . . . . . . . 8 (𝑔𝐿𝑓 ↔ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})(π‘β€˜0) = (π‘Žβ€˜0))
1813, 16, 173bitr4i 302 . . . . . . 7 (𝑓𝐿𝑔 ↔ 𝑔𝐿𝑓)
199, 18sylib 217 . . . . . 6 ((⊀ ∧ 𝑓𝐿𝑔) β†’ 𝑔𝐿𝑓)
201, 2, 3, 4, 14, 15, 6efgrelexlema 19531 . . . . . . . . 9 (π‘”πΏβ„Ž ↔ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0))
21 reeanv 3217 . . . . . . . . . 10 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})(βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) ↔ (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)))
221, 2, 3, 4, 14, 15efgsfo 19521 . . . . . . . . . . . . . . . . . . . 20 𝑆:dom 𝑆–ontoβ†’π‘Š
23 fofn 6758 . . . . . . . . . . . . . . . . . . . 20 (𝑆:dom 𝑆–ontoβ†’π‘Š β†’ 𝑆 Fn dom 𝑆)
2422, 23ax-mp 5 . . . . . . . . . . . . . . . . . . 19 𝑆 Fn dom 𝑆
25 fniniseg 7010 . . . . . . . . . . . . . . . . . . 19 (𝑆 Fn dom 𝑆 β†’ (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = 𝑔)))
2624, 25ax-mp 5 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = 𝑔))
27 fniniseg 7010 . . . . . . . . . . . . . . . . . . 19 (𝑆 Fn dom 𝑆 β†’ (𝑏 ∈ (◑𝑆 β€œ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘) = 𝑔)))
2824, 27ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (◑𝑆 β€œ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘) = 𝑔))
29 eqtr3 2762 . . . . . . . . . . . . . . . . . . . 20 (((π‘†β€˜π‘Ÿ) = 𝑔 ∧ (π‘†β€˜π‘) = 𝑔) β†’ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘))
301, 2, 3, 4, 14, 15efgred 19530 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘)) β†’ (π‘Ÿβ€˜0) = (π‘β€˜0))
3130eqcomd 2742 . . . . . . . . . . . . . . . . . . . . 21 ((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘)) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
32313expa 1118 . . . . . . . . . . . . . . . . . . . 20 (((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) ∧ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘)) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
3329, 32sylan2 593 . . . . . . . . . . . . . . . . . . 19 (((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆) ∧ ((π‘†β€˜π‘Ÿ) = 𝑔 ∧ (π‘†β€˜π‘) = 𝑔)) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
3433an4s 658 . . . . . . . . . . . . . . . . . 18 (((π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = 𝑔) ∧ (𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘) = 𝑔)) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
3526, 28, 34syl2anb 598 . . . . . . . . . . . . . . . . 17 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ (π‘β€˜0) = (π‘Ÿβ€˜0))
36 eqeq2 2748 . . . . . . . . . . . . . . . . 17 ((π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ ((π‘β€˜0) = (π‘Ÿβ€˜0) ↔ (π‘β€˜0) = (π‘ β€˜0)))
3735, 36syl5ibcom 244 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ ((π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ (π‘β€˜0) = (π‘ β€˜0)))
3837reximdv 3167 . . . . . . . . . . . . . . 15 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘β€˜0) = (π‘ β€˜0)))
39 eqeq1 2740 . . . . . . . . . . . . . . . . 17 ((π‘Žβ€˜0) = (π‘β€˜0) β†’ ((π‘Žβ€˜0) = (π‘ β€˜0) ↔ (π‘β€˜0) = (π‘ β€˜0)))
4039rexbidv 3175 . . . . . . . . . . . . . . . 16 ((π‘Žβ€˜0) = (π‘β€˜0) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0) ↔ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘β€˜0) = (π‘ β€˜0)))
4140imbi2d 340 . . . . . . . . . . . . . . 15 ((π‘Žβ€˜0) = (π‘β€˜0) β†’ ((βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0)) ↔ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘β€˜0) = (π‘ β€˜0))))
4238, 41syl5ibrcom 246 . . . . . . . . . . . . . 14 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ ((π‘Žβ€˜0) = (π‘β€˜0) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))))
4342rexlimdva 3152 . . . . . . . . . . . . 13 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) β†’ (βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))))
4443impd 411 . . . . . . . . . . . 12 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) β†’ ((βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0)))
4544rexlimiv 3145 . . . . . . . . . . 11 (βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})(βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
4645reximi 3087 . . . . . . . . . 10 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})(βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
4721, 46sylbir 234 . . . . . . . . 9 ((βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
4816, 20, 47syl2anb 598 . . . . . . . 8 ((𝑓𝐿𝑔 ∧ π‘”πΏβ„Ž) β†’ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
491, 2, 3, 4, 14, 15, 6efgrelexlema 19531 . . . . . . . 8 (π‘“πΏβ„Ž ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
5048, 49sylibr 233 . . . . . . 7 ((𝑓𝐿𝑔 ∧ π‘”πΏβ„Ž) β†’ π‘“πΏβ„Ž)
5150adantl 482 . . . . . 6 ((⊀ ∧ (𝑓𝐿𝑔 ∧ π‘”πΏβ„Ž)) β†’ π‘“πΏβ„Ž)
52 eqid 2736 . . . . . . . . . . . 12 (π‘Žβ€˜0) = (π‘Žβ€˜0)
53 fveq1 6841 . . . . . . . . . . . . 13 (𝑏 = π‘Ž β†’ (π‘β€˜0) = (π‘Žβ€˜0))
5453rspceeqv 3595 . . . . . . . . . . . 12 ((π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ (π‘Žβ€˜0) = (π‘Žβ€˜0)) β†’ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
5552, 54mpan2 689 . . . . . . . . . . 11 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) β†’ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
5655pm4.71i 560 . . . . . . . . . 10 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0)))
57 fniniseg 7010 . . . . . . . . . . 11 (𝑆 Fn dom 𝑆 β†’ (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓)))
5824, 57ax-mp 5 . . . . . . . . . 10 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓))
5956, 58bitr3i 276 . . . . . . . . 9 ((π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0)) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓))
6059rexbii2 3093 . . . . . . . 8 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0) ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓)
611, 2, 3, 4, 14, 15, 6efgrelexlema 19531 . . . . . . . 8 (𝑓𝐿𝑓 ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
62 forn 6759 . . . . . . . . . . 11 (𝑆:dom 𝑆–ontoβ†’π‘Š β†’ ran 𝑆 = π‘Š)
6322, 62ax-mp 5 . . . . . . . . . 10 ran 𝑆 = π‘Š
6463eleq2i 2829 . . . . . . . . 9 (𝑓 ∈ ran 𝑆 ↔ 𝑓 ∈ π‘Š)
65 fvelrnb 6903 . . . . . . . . . 10 (𝑆 Fn dom 𝑆 β†’ (𝑓 ∈ ran 𝑆 ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓))
6624, 65ax-mp 5 . . . . . . . . 9 (𝑓 ∈ ran 𝑆 ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓)
6764, 66bitr3i 276 . . . . . . . 8 (𝑓 ∈ π‘Š ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓)
6860, 61, 673bitr4ri 303 . . . . . . 7 (𝑓 ∈ π‘Š ↔ 𝑓𝐿𝑓)
6968a1i 11 . . . . . 6 (⊀ β†’ (𝑓 ∈ π‘Š ↔ 𝑓𝐿𝑓))
708, 19, 51, 69iserd 8674 . . . . 5 (⊀ β†’ 𝐿 Er π‘Š)
7170mptru 1548 . . . 4 𝐿 Er π‘Š
72 simpl 483 . . . . . . . . . . 11 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ π‘Ž ∈ π‘Š)
73 foelrn 7056 . . . . . . . . . . 11 ((𝑆:dom 𝑆–ontoβ†’π‘Š ∧ π‘Ž ∈ π‘Š) β†’ βˆƒπ‘Ÿ ∈ dom 𝑆 π‘Ž = (π‘†β€˜π‘Ÿ))
7422, 72, 73sylancr 587 . . . . . . . . . 10 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ βˆƒπ‘Ÿ ∈ dom 𝑆 π‘Ž = (π‘†β€˜π‘Ÿ))
75 simprl 769 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ dom 𝑆)
76 simprr 771 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ž = (π‘†β€˜π‘Ÿ))
7776eqcomd 2742 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘†β€˜π‘Ÿ) = π‘Ž)
78 fniniseg 7010 . . . . . . . . . . . 12 (𝑆 Fn dom 𝑆 β†’ (π‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = π‘Ž)))
7924, 78ax-mp 5 . . . . . . . . . . 11 (π‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = π‘Ž))
8075, 77, 79sylanbrc 583 . . . . . . . . . 10 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž}))
81 simplr 767 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 𝑏 ∈ ran (π‘‡β€˜π‘Ž))
8276fveq2d 6846 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘‡β€˜π‘Ž) = (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
8382rneqd 5893 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ ran (π‘‡β€˜π‘Ž) = ran (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
8481, 83eleqtrd 2839 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 𝑏 ∈ ran (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
851, 2, 3, 4, 14, 15efgsp1 19519 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ ran (π‘‡β€˜(π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆)
8675, 84, 85syl2anc 584 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆)
871, 2, 3, 4, 14, 15efgsdm 19512 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ dom 𝑆 ↔ (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) ∧ (π‘Ÿβ€˜0) ∈ 𝐷 ∧ βˆ€π‘– ∈ (1..^(β™―β€˜π‘Ÿ))(π‘Ÿβ€˜π‘–) ∈ ran (π‘‡β€˜(π‘Ÿβ€˜(𝑖 βˆ’ 1)))))
8887simp1bi 1145 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ dom 𝑆 β†’ π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}))
8988ad2antrl 726 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}))
9089eldifad 3922 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ Word π‘Š)
911, 2, 3, 4efgtf 19504 . . . . . . . . . . . . . . . . 17 (π‘Ž ∈ π‘Š β†’ ((π‘‡β€˜π‘Ž) = (𝑓 ∈ (0...(β™―β€˜π‘Ž)), 𝑔 ∈ (𝐼 Γ— 2o) ↦ (π‘Ž splice βŸ¨π‘“, 𝑓, βŸ¨β€œπ‘”(π‘€β€˜π‘”)β€βŸ©βŸ©)) ∧ (π‘‡β€˜π‘Ž):((0...(β™―β€˜π‘Ž)) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š))
9291simprd 496 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ π‘Š β†’ (π‘‡β€˜π‘Ž):((0...(β™―β€˜π‘Ž)) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š)
9392frnd 6676 . . . . . . . . . . . . . . 15 (π‘Ž ∈ π‘Š β†’ ran (π‘‡β€˜π‘Ž) βŠ† π‘Š)
9493sselda 3944 . . . . . . . . . . . . . 14 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ 𝑏 ∈ π‘Š)
9594adantr 481 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 𝑏 ∈ π‘Š)
961, 2, 3, 4, 14, 15efgsval2 19515 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ Word π‘Š ∧ 𝑏 ∈ π‘Š ∧ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆) β†’ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)
9790, 95, 86, 96syl3anc 1371 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)
98 fniniseg 7010 . . . . . . . . . . . . 13 (𝑆 Fn dom 𝑆 β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ↔ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆 ∧ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)))
9924, 98ax-mp 5 . . . . . . . . . . . 12 ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ↔ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆 ∧ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏))
10086, 97, 99sylanbrc 583 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}))
10195s1cld 14491 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word π‘Š)
102 eldifsn 4747 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) ↔ (π‘Ÿ ∈ Word π‘Š ∧ π‘Ÿ β‰  βˆ…))
103 lennncl 14422 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ Word π‘Š ∧ π‘Ÿ β‰  βˆ…) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
104102, 103sylbi 216 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
10589, 104syl 17 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
106 lbfzo0 13612 . . . . . . . . . . . . . 14 (0 ∈ (0..^(β™―β€˜π‘Ÿ)) ↔ (β™―β€˜π‘Ÿ) ∈ β„•)
107105, 106sylibr 233 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 0 ∈ (0..^(β™―β€˜π‘Ÿ)))
108 ccatval1 14465 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ Word π‘Š ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word π‘Š ∧ 0 ∈ (0..^(β™―β€˜π‘Ÿ))) β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Ÿβ€˜0))
10990, 101, 107, 108syl3anc 1371 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Ÿβ€˜0))
110109eqcomd 2742 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿβ€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0))
111 fveq1 6841 . . . . . . . . . . . 12 (𝑠 = (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) β†’ (π‘ β€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0))
112111rspceeqv 3595 . . . . . . . . . . 11 (((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ∧ (π‘Ÿβ€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
113100, 110, 112syl2anc 584 . . . . . . . . . 10 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
11474, 80, 113reximssdv 3169 . . . . . . . . 9 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž})βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
1151, 2, 3, 4, 14, 15, 6efgrelexlema 19531 . . . . . . . . 9 (π‘ŽπΏπ‘ ↔ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž})βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
116114, 115sylibr 233 . . . . . . . 8 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ π‘ŽπΏπ‘)
117 vex 3449 . . . . . . . . 9 𝑏 ∈ V
118 vex 3449 . . . . . . . . 9 π‘Ž ∈ V
119117, 118elec 8692 . . . . . . . 8 (𝑏 ∈ [π‘Ž]𝐿 ↔ π‘ŽπΏπ‘)
120116, 119sylibr 233 . . . . . . 7 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ 𝑏 ∈ [π‘Ž]𝐿)
121120ex 413 . . . . . 6 (π‘Ž ∈ π‘Š β†’ (𝑏 ∈ ran (π‘‡β€˜π‘Ž) β†’ 𝑏 ∈ [π‘Ž]𝐿))
122121ssrdv 3950 . . . . 5 (π‘Ž ∈ π‘Š β†’ ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿)
123122rgen 3066 . . . 4 βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿
1241fvexi 6856 . . . . . 6 π‘Š ∈ V
125 erex 8672 . . . . . 6 (𝐿 Er π‘Š β†’ (π‘Š ∈ V β†’ 𝐿 ∈ V))
12671, 124, 125mp2 9 . . . . 5 𝐿 ∈ V
127 ereq1 8655 . . . . . 6 (π‘Ÿ = 𝐿 β†’ (π‘Ÿ Er π‘Š ↔ 𝐿 Er π‘Š))
128 eceq2 8688 . . . . . . . 8 (π‘Ÿ = 𝐿 β†’ [π‘Ž]π‘Ÿ = [π‘Ž]𝐿)
129128sseq2d 3976 . . . . . . 7 (π‘Ÿ = 𝐿 β†’ (ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ ↔ ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
130129ralbidv 3174 . . . . . 6 (π‘Ÿ = 𝐿 β†’ (βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ ↔ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
131127, 130anbi12d 631 . . . . 5 (π‘Ÿ = 𝐿 β†’ ((π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ) ↔ (𝐿 Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿)))
132126, 131elab 3630 . . . 4 (𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} ↔ (𝐿 Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
13371, 123, 132mpbir2an 709 . . 3 𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)}
134 intss1 4924 . . 3 (𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} β†’ ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} βŠ† 𝐿)
135133, 134ax-mp 5 . 2 ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} βŠ† 𝐿
1365, 135eqsstri 3978 1 ∼ βŠ† 𝐿
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106  {cab 2713   β‰  wne 2943  βˆ€wral 3064  βˆƒwrex 3073  {crab 3407  Vcvv 3445   βˆ– cdif 3907   βŠ† wss 3910  βˆ…c0 4282  {csn 4586  βŸ¨cop 4592  βŸ¨cotp 4594  βˆ© cint 4907  βˆͺ ciun 4954   class class class wbr 5105  {copab 5167   ↦ cmpt 5188   I cid 5530   Γ— cxp 5631  β—‘ccnv 5632  dom cdm 5633  ran crn 5634   β€œ cima 5636  Rel wrel 5638   Fn wfn 6491  βŸΆwf 6492  β€“ontoβ†’wfo 6494  β€˜cfv 6496  (class class class)co 7357   ∈ cmpo 7359  1oc1o 8405  2oc2o 8406   Er wer 8645  [cec 8646  0cc0 11051  1c1 11052   βˆ’ cmin 11385  β„•cn 12153  ...cfz 13424  ..^cfzo 13567  β™―chash 14230  Word cword 14402   ++ cconcat 14458  βŸ¨β€œcs1 14483   splice csplice 14637  βŸ¨β€œcs2 14730   ~FG cefg 19488
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-ot 4595  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-ec 8650  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-rp 12916  df-fz 13425  df-fzo 13568  df-hash 14231  df-word 14403  df-concat 14459  df-s1 14484  df-substr 14529  df-pfx 14559  df-splice 14638  df-s2 14737  df-efg 19491
This theorem is referenced by:  efgrelex  19533
  Copyright terms: Public domain W3C validator