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

Theorem efgrelexlemb 19620
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 19594 . 2 ∼ = ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)}
6 efgrelexlem.1 . . . . . . . 8 𝐿 = {βŸ¨π‘–, π‘—βŸ© ∣ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑖})βˆƒπ‘‘ ∈ (◑𝑆 β€œ {𝑗})(π‘β€˜0) = (π‘‘β€˜0)}
76relopabiv 5820 . . . . . . 7 Rel 𝐿
87a1i 11 . . . . . 6 (⊀ β†’ Rel 𝐿)
9 simpr 485 . . . . . . 7 ((⊀ ∧ 𝑓𝐿𝑔) β†’ 𝑓𝐿𝑔)
10 eqcom 2739 . . . . . . . . . 10 ((π‘Žβ€˜0) = (π‘β€˜0) ↔ (π‘β€˜0) = (π‘Žβ€˜0))
11102rexbii 3129 . . . . . . . . 9 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘β€˜0) = (π‘Žβ€˜0))
12 rexcom 3287 . . . . . . . . 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 19619 . . . . . . . 8 (𝑓𝐿𝑔 ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0))
171, 2, 3, 4, 14, 15, 6efgrelexlema 19619 . . . . . . . 8 (𝑔𝐿𝑓 ↔ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})(π‘β€˜0) = (π‘Žβ€˜0))
1813, 16, 173bitr4i 302 . . . . . . 7 (𝑓𝐿𝑔 ↔ 𝑔𝐿𝑓)
199, 18sylib 217 . . . . . 6 ((⊀ ∧ 𝑓𝐿𝑔) β†’ 𝑔𝐿𝑓)
201, 2, 3, 4, 14, 15, 6efgrelexlema 19619 . . . . . . . . 9 (π‘”πΏβ„Ž ↔ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0))
21 reeanv 3226 . . . . . . . . . 10 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})(βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) ↔ (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)))
221, 2, 3, 4, 14, 15efgsfo 19609 . . . . . . . . . . . . . . . . . . . 20 𝑆:dom 𝑆–ontoβ†’π‘Š
23 fofn 6807 . . . . . . . . . . . . . . . . . . . 20 (𝑆:dom 𝑆–ontoβ†’π‘Š β†’ 𝑆 Fn dom 𝑆)
2422, 23ax-mp 5 . . . . . . . . . . . . . . . . . . 19 𝑆 Fn dom 𝑆
25 fniniseg 7061 . . . . . . . . . . . . . . . . . . 19 (𝑆 Fn dom 𝑆 β†’ (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = 𝑔)))
2624, 25ax-mp 5 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ↔ (π‘Ÿ ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = 𝑔))
27 fniniseg 7061 . . . . . . . . . . . . . . . . . . 19 (𝑆 Fn dom 𝑆 β†’ (𝑏 ∈ (◑𝑆 β€œ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘) = 𝑔)))
2824, 27ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ (◑𝑆 β€œ {𝑔}) ↔ (𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘) = 𝑔))
29 eqtr3 2758 . . . . . . . . . . . . . . . . . . . 20 (((π‘†β€˜π‘Ÿ) = 𝑔 ∧ (π‘†β€˜π‘) = 𝑔) β†’ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘))
301, 2, 3, 4, 14, 15efgred 19618 . . . . . . . . . . . . . . . . . . . . . 22 ((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ÿ) = (π‘†β€˜π‘)) β†’ (π‘Ÿβ€˜0) = (π‘β€˜0))
3130eqcomd 2738 . . . . . . . . . . . . . . . . . . . . 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 2744 . . . . . . . . . . . . . . . . 17 ((π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ ((π‘β€˜0) = (π‘Ÿβ€˜0) ↔ (π‘β€˜0) = (π‘ β€˜0)))
3735, 36syl5ibcom 244 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ ((π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ (π‘β€˜0) = (π‘ β€˜0)))
3837reximdv 3170 . . . . . . . . . . . . . . 15 ((π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) ∧ 𝑏 ∈ (◑𝑆 β€œ {𝑔})) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘β€˜0) = (π‘ β€˜0)))
39 eqeq1 2736 . . . . . . . . . . . . . . . . 17 ((π‘Žβ€˜0) = (π‘β€˜0) β†’ ((π‘Žβ€˜0) = (π‘ β€˜0) ↔ (π‘β€˜0) = (π‘ β€˜0)))
4039rexbidv 3178 . . . . . . . . . . . . . . . 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 3155 . . . . . . . . . . . . 13 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) β†’ (βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) β†’ (βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))))
4443impd 411 . . . . . . . . . . . 12 (π‘Ÿ ∈ (◑𝑆 β€œ {𝑔}) β†’ ((βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0)))
4544rexlimiv 3148 . . . . . . . . . . 11 (βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {𝑔})(βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑔})(π‘Žβ€˜0) = (π‘β€˜0) ∧ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Ÿβ€˜0) = (π‘ β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
4645reximi 3084 . . . . . . . . . 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 19619 . . . . . . . 8 (π‘“πΏβ„Ž ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘  ∈ (◑𝑆 β€œ {β„Ž})(π‘Žβ€˜0) = (π‘ β€˜0))
5048, 49sylibr 233 . . . . . . 7 ((𝑓𝐿𝑔 ∧ π‘”πΏβ„Ž) β†’ π‘“πΏβ„Ž)
5150adantl 482 . . . . . 6 ((⊀ ∧ (𝑓𝐿𝑔 ∧ π‘”πΏβ„Ž)) β†’ π‘“πΏβ„Ž)
52 eqid 2732 . . . . . . . . . . . 12 (π‘Žβ€˜0) = (π‘Žβ€˜0)
53 fveq1 6890 . . . . . . . . . . . . 13 (𝑏 = π‘Ž β†’ (π‘β€˜0) = (π‘Žβ€˜0))
5453rspceeqv 3633 . . . . . . . . . . . 12 ((π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ (π‘Žβ€˜0) = (π‘Žβ€˜0)) β†’ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
5552, 54mpan2 689 . . . . . . . . . . 11 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) β†’ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
5655pm4.71i 560 . . . . . . . . . 10 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0)))
57 fniniseg 7061 . . . . . . . . . . 11 (𝑆 Fn dom 𝑆 β†’ (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓)))
5824, 57ax-mp 5 . . . . . . . . . 10 (π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓))
5956, 58bitr3i 276 . . . . . . . . 9 ((π‘Ž ∈ (◑𝑆 β€œ {𝑓}) ∧ βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0)) ↔ (π‘Ž ∈ dom 𝑆 ∧ (π‘†β€˜π‘Ž) = 𝑓))
6059rexbii2 3090 . . . . . . . 8 (βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0) ↔ βˆƒπ‘Ž ∈ dom 𝑆(π‘†β€˜π‘Ž) = 𝑓)
611, 2, 3, 4, 14, 15, 6efgrelexlema 19619 . . . . . . . 8 (𝑓𝐿𝑓 ↔ βˆƒπ‘Ž ∈ (◑𝑆 β€œ {𝑓})βˆƒπ‘ ∈ (◑𝑆 β€œ {𝑓})(π‘Žβ€˜0) = (π‘β€˜0))
62 forn 6808 . . . . . . . . . . 11 (𝑆:dom 𝑆–ontoβ†’π‘Š β†’ ran 𝑆 = π‘Š)
6322, 62ax-mp 5 . . . . . . . . . 10 ran 𝑆 = π‘Š
6463eleq2i 2825 . . . . . . . . 9 (𝑓 ∈ ran 𝑆 ↔ 𝑓 ∈ π‘Š)
65 fvelrnb 6952 . . . . . . . . . 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 8731 . . . . 5 (⊀ β†’ 𝐿 Er π‘Š)
7170mptru 1548 . . . 4 𝐿 Er π‘Š
72 simpl 483 . . . . . . . . . . 11 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ π‘Ž ∈ π‘Š)
73 foelrn 7108 . . . . . . . . . . 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 2738 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘†β€˜π‘Ÿ) = π‘Ž)
78 fniniseg 7061 . . . . . . . . . . . 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 6895 . . . . . . . . . . . . . . 15 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘‡β€˜π‘Ž) = (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
8382rneqd 5937 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ ran (π‘‡β€˜π‘Ž) = ran (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
8481, 83eleqtrd 2835 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 𝑏 ∈ ran (π‘‡β€˜(π‘†β€˜π‘Ÿ)))
851, 2, 3, 4, 14, 15efgsp1 19607 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ dom 𝑆 ∧ 𝑏 ∈ ran (π‘‡β€˜(π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆)
8675, 84, 85syl2anc 584 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆)
871, 2, 3, 4, 14, 15efgsdm 19600 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ dom 𝑆 ↔ (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) ∧ (π‘Ÿβ€˜0) ∈ 𝐷 ∧ βˆ€π‘– ∈ (1..^(β™―β€˜π‘Ÿ))(π‘Ÿβ€˜π‘–) ∈ ran (π‘‡β€˜(π‘Ÿβ€˜(𝑖 βˆ’ 1)))))
8887simp1bi 1145 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ dom 𝑆 β†’ π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}))
8988ad2antrl 726 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}))
9089eldifad 3960 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ π‘Ÿ ∈ Word π‘Š)
911, 2, 3, 4efgtf 19592 . . . . . . . . . . . . . . . . 17 (π‘Ž ∈ π‘Š β†’ ((π‘‡β€˜π‘Ž) = (𝑓 ∈ (0...(β™―β€˜π‘Ž)), 𝑔 ∈ (𝐼 Γ— 2o) ↦ (π‘Ž splice βŸ¨π‘“, 𝑓, βŸ¨β€œπ‘”(π‘€β€˜π‘”)β€βŸ©βŸ©)) ∧ (π‘‡β€˜π‘Ž):((0...(β™―β€˜π‘Ž)) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š))
9291simprd 496 . . . . . . . . . . . . . . . 16 (π‘Ž ∈ π‘Š β†’ (π‘‡β€˜π‘Ž):((0...(β™―β€˜π‘Ž)) Γ— (𝐼 Γ— 2o))βŸΆπ‘Š)
9392frnd 6725 . . . . . . . . . . . . . . 15 (π‘Ž ∈ π‘Š β†’ ran (π‘‡β€˜π‘Ž) βŠ† π‘Š)
9493sselda 3982 . . . . . . . . . . . . . 14 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ 𝑏 ∈ π‘Š)
9594adantr 481 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 𝑏 ∈ π‘Š)
961, 2, 3, 4, 14, 15efgsval2 19603 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ Word π‘Š ∧ 𝑏 ∈ π‘Š ∧ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆) β†’ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)
9790, 95, 86, 96syl3anc 1371 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)
98 fniniseg 7061 . . . . . . . . . . . . 13 (𝑆 Fn dom 𝑆 β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ↔ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆 ∧ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏)))
9924, 98ax-mp 5 . . . . . . . . . . . 12 ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ↔ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ dom 𝑆 ∧ (π‘†β€˜(π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)) = 𝑏))
10086, 97, 99sylanbrc 583 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}))
10195s1cld 14555 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ βŸ¨β€œπ‘β€βŸ© ∈ Word π‘Š)
102 eldifsn 4790 . . . . . . . . . . . . . . . 16 (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) ↔ (π‘Ÿ ∈ Word π‘Š ∧ π‘Ÿ β‰  βˆ…))
103 lennncl 14486 . . . . . . . . . . . . . . . 16 ((π‘Ÿ ∈ Word π‘Š ∧ π‘Ÿ β‰  βˆ…) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
104102, 103sylbi 216 . . . . . . . . . . . . . . 15 (π‘Ÿ ∈ (Word π‘Š βˆ– {βˆ…}) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
10589, 104syl 17 . . . . . . . . . . . . . 14 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (β™―β€˜π‘Ÿ) ∈ β„•)
106 lbfzo0 13674 . . . . . . . . . . . . . 14 (0 ∈ (0..^(β™―β€˜π‘Ÿ)) ↔ (β™―β€˜π‘Ÿ) ∈ β„•)
107105, 106sylibr 233 . . . . . . . . . . . . 13 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ 0 ∈ (0..^(β™―β€˜π‘Ÿ)))
108 ccatval1 14529 . . . . . . . . . . . . 13 ((π‘Ÿ ∈ Word π‘Š ∧ βŸ¨β€œπ‘β€βŸ© ∈ Word π‘Š ∧ 0 ∈ (0..^(β™―β€˜π‘Ÿ))) β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Ÿβ€˜0))
10990, 101, 107, 108syl3anc 1371 . . . . . . . . . . . 12 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0) = (π‘Ÿβ€˜0))
110109eqcomd 2738 . . . . . . . . . . 11 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ (π‘Ÿβ€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0))
111 fveq1 6890 . . . . . . . . . . . 12 (𝑠 = (π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) β†’ (π‘ β€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0))
112111rspceeqv 3633 . . . . . . . . . . 11 (((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©) ∈ (◑𝑆 β€œ {𝑏}) ∧ (π‘Ÿβ€˜0) = ((π‘Ÿ ++ βŸ¨β€œπ‘β€βŸ©)β€˜0)) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
113100, 110, 112syl2anc 584 . . . . . . . . . 10 (((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) ∧ (π‘Ÿ ∈ dom 𝑆 ∧ π‘Ž = (π‘†β€˜π‘Ÿ))) β†’ βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
11474, 80, 113reximssdv 3172 . . . . . . . . 9 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž})βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
1151, 2, 3, 4, 14, 15, 6efgrelexlema 19619 . . . . . . . . 9 (π‘ŽπΏπ‘ ↔ βˆƒπ‘Ÿ ∈ (◑𝑆 β€œ {π‘Ž})βˆƒπ‘  ∈ (◑𝑆 β€œ {𝑏})(π‘Ÿβ€˜0) = (π‘ β€˜0))
116114, 115sylibr 233 . . . . . . . 8 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ π‘ŽπΏπ‘)
117 vex 3478 . . . . . . . . 9 𝑏 ∈ V
118 vex 3478 . . . . . . . . 9 π‘Ž ∈ V
119117, 118elec 8749 . . . . . . . 8 (𝑏 ∈ [π‘Ž]𝐿 ↔ π‘ŽπΏπ‘)
120116, 119sylibr 233 . . . . . . 7 ((π‘Ž ∈ π‘Š ∧ 𝑏 ∈ ran (π‘‡β€˜π‘Ž)) β†’ 𝑏 ∈ [π‘Ž]𝐿)
121120ex 413 . . . . . 6 (π‘Ž ∈ π‘Š β†’ (𝑏 ∈ ran (π‘‡β€˜π‘Ž) β†’ 𝑏 ∈ [π‘Ž]𝐿))
122121ssrdv 3988 . . . . 5 (π‘Ž ∈ π‘Š β†’ ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿)
123122rgen 3063 . . . 4 βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿
1241fvexi 6905 . . . . . 6 π‘Š ∈ V
125 erex 8729 . . . . . 6 (𝐿 Er π‘Š β†’ (π‘Š ∈ V β†’ 𝐿 ∈ V))
12671, 124, 125mp2 9 . . . . 5 𝐿 ∈ V
127 ereq1 8712 . . . . . 6 (π‘Ÿ = 𝐿 β†’ (π‘Ÿ Er π‘Š ↔ 𝐿 Er π‘Š))
128 eceq2 8745 . . . . . . . 8 (π‘Ÿ = 𝐿 β†’ [π‘Ž]π‘Ÿ = [π‘Ž]𝐿)
129128sseq2d 4014 . . . . . . 7 (π‘Ÿ = 𝐿 β†’ (ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ ↔ ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
130129ralbidv 3177 . . . . . 6 (π‘Ÿ = 𝐿 β†’ (βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ ↔ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
131127, 130anbi12d 631 . . . . 5 (π‘Ÿ = 𝐿 β†’ ((π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ) ↔ (𝐿 Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿)))
132126, 131elab 3668 . . . 4 (𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} ↔ (𝐿 Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]𝐿))
13371, 123, 132mpbir2an 709 . . 3 𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)}
134 intss1 4967 . . 3 (𝐿 ∈ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} β†’ ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} βŠ† 𝐿)
135133, 134ax-mp 5 . 2 ∩ {π‘Ÿ ∣ (π‘Ÿ Er π‘Š ∧ βˆ€π‘Ž ∈ π‘Š ran (π‘‡β€˜π‘Ž) βŠ† [π‘Ž]π‘Ÿ)} βŠ† 𝐿
1365, 135eqsstri 4016 1 ∼ βŠ† 𝐿
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106  {cab 2709   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432  Vcvv 3474   βˆ– cdif 3945   βŠ† wss 3948  βˆ…c0 4322  {csn 4628  βŸ¨cop 4634  βŸ¨cotp 4636  βˆ© cint 4950  βˆͺ ciun 4997   class class class wbr 5148  {copab 5210   ↦ cmpt 5231   I cid 5573   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676  ran crn 5677   β€œ cima 5679  Rel wrel 5681   Fn wfn 6538  βŸΆwf 6539  β€“ontoβ†’wfo 6541  β€˜cfv 6543  (class class class)co 7411   ∈ cmpo 7413  1oc1o 8461  2oc2o 8462   Er wer 8702  [cec 8703  0cc0 11112  1c1 11113   βˆ’ cmin 11446  β„•cn 12214  ...cfz 13486  ..^cfzo 13629  β™―chash 14292  Word cword 14466   ++ cconcat 14522  βŸ¨β€œcs1 14547   splice csplice 14701  βŸ¨β€œcs2 14794   ~FG cefg 19576
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 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
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 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-ot 4637  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-er 8705  df-ec 8707  df-map 8824  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-card 9936  df-pnf 11252  df-mnf 11253  df-xr 11254  df-ltxr 11255  df-le 11256  df-sub 11448  df-neg 11449  df-nn 12215  df-2 12277  df-n0 12475  df-xnn0 12547  df-z 12561  df-uz 12825  df-rp 12977  df-fz 13487  df-fzo 13630  df-hash 14293  df-word 14467  df-concat 14523  df-s1 14548  df-substr 14593  df-pfx 14623  df-splice 14702  df-s2 14801  df-efg 19579
This theorem is referenced by:  efgrelex  19621
  Copyright terms: Public domain W3C validator