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

Theorem wwlktovfo 13894
Description: Lemma 3 for wrd2f1tovbij 13896. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
Hypotheses
Ref Expression
wrd2f1tovbij.d 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}
wrd2f1tovbij.r 𝑅 = {𝑛𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}
wrd2f1tovbij.f 𝐹 = (𝑡𝐷 ↦ (𝑡‘1))
Assertion
Ref Expression
wwlktovfo (𝑃𝑉𝐹:𝐷onto𝑅)
Distinct variable groups:   𝑡,𝐷   𝑃,𝑛,𝑡,𝑤   𝑡,𝑅   𝑛,𝑉,𝑡,𝑤   𝑛,𝑋,𝑤
Allowed substitution hints:   𝐷(𝑤,𝑛)   𝑅(𝑤,𝑛)   𝐹(𝑤,𝑡,𝑛)   𝑋(𝑡)

Proof of Theorem wwlktovfo
Dummy variables 𝑝 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wrd2f1tovbij.d . . . 4 𝐷 = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}
2 wrd2f1tovbij.r . . . 4 𝑅 = {𝑛𝑉 ∣ {𝑃, 𝑛} ∈ 𝑋}
3 wrd2f1tovbij.f . . . 4 𝐹 = (𝑡𝐷 ↦ (𝑡‘1))
41, 2, 3wwlktovf 13892 . . 3 𝐹:𝐷𝑅
54a1i 11 . 2 (𝑃𝑉𝐹:𝐷𝑅)
6 preq2 4405 . . . . . 6 (𝑛 = 𝑝 → {𝑃, 𝑛} = {𝑃, 𝑝})
76eleq1d 2816 . . . . 5 (𝑛 = 𝑝 → ({𝑃, 𝑛} ∈ 𝑋 ↔ {𝑃, 𝑝} ∈ 𝑋))
87, 2elrab2 3499 . . . 4 (𝑝𝑅 ↔ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))
9 simpl 474 . . . . . . . . . . 11 ((𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋) → 𝑝𝑉)
109anim2i 594 . . . . . . . . . 10 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → (𝑃𝑉𝑝𝑉))
11 eqidd 2753 . . . . . . . . . 10 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → {⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = {⟨0, 𝑃⟩, ⟨1, 𝑝⟩})
12 wrdlen2i 13879 . . . . . . . . . 10 ((𝑃𝑉𝑝𝑉) → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = {⟨0, 𝑃⟩, ⟨1, 𝑝⟩} → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝))))
1310, 11, 12sylc 65 . . . . . . . . 9 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)))
14 prex 5050 . . . . . . . . . . 11 {⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ V
1514a1i 11 . . . . . . . . . 10 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → {⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ V)
16 eleq1 2819 . . . . . . . . . . . . . . . . . . . 20 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉𝑢 ∈ Word 𝑉))
1716biimpd 219 . . . . . . . . . . . . . . . . . . 19 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉𝑢 ∈ Word 𝑉))
1817adantr 472 . . . . . . . . . . . . . . . . . 18 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉𝑢 ∈ Word 𝑉))
1918com12 32 . . . . . . . . . . . . . . . . 17 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → 𝑢 ∈ Word 𝑉))
2019adantr 472 . . . . . . . . . . . . . . . 16 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → 𝑢 ∈ Word 𝑉))
2120adantr 472 . . . . . . . . . . . . . . 15 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → 𝑢 ∈ Word 𝑉))
2221impcom 445 . . . . . . . . . . . . . 14 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝))) → 𝑢 ∈ Word 𝑉)
23 fveq2 6344 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = (♯‘𝑢))
2423eqeq1d 2754 . . . . . . . . . . . . . . . . . . . . 21 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ((♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2 ↔ (♯‘𝑢) = 2))
2524biimpd 219 . . . . . . . . . . . . . . . . . . . 20 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ((♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2 → (♯‘𝑢) = 2))
2625adantr 472 . . . . . . . . . . . . . . . . . . 19 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2 → (♯‘𝑢) = 2))
2726com12 32 . . . . . . . . . . . . . . . . . 18 ((♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2 → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (♯‘𝑢) = 2))
2827adantl 473 . . . . . . . . . . . . . . . . 17 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (♯‘𝑢) = 2))
2928adantr 472 . . . . . . . . . . . . . . . 16 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (♯‘𝑢) = 2))
3029impcom 445 . . . . . . . . . . . . . . 15 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝))) → (♯‘𝑢) = 2)
31 fveq1 6343 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = (𝑢‘0))
3231eqeq1d 2754 . . . . . . . . . . . . . . . . . . . . 21 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ↔ (𝑢‘0) = 𝑃))
3332biimpd 219 . . . . . . . . . . . . . . . . . . . 20 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 → (𝑢‘0) = 𝑃))
3433adantr 472 . . . . . . . . . . . . . . . . . . 19 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 → (𝑢‘0) = 𝑃))
3534com12 32 . . . . . . . . . . . . . . . . . 18 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃))
3635adantr 472 . . . . . . . . . . . . . . . . 17 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝) → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃))
3736adantl 473 . . . . . . . . . . . . . . . 16 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → (𝑢‘0) = 𝑃))
3837impcom 445 . . . . . . . . . . . . . . 15 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝))) → (𝑢‘0) = 𝑃)
39 fveq1 6343 . . . . . . . . . . . . . . . . . . . . . . . 24 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = (𝑢‘1))
4039eqeq1d 2754 . . . . . . . . . . . . . . . . . . . . . . 23 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝 ↔ (𝑢‘1) = 𝑝))
4132, 40anbi12d 749 . . . . . . . . . . . . . . . . . . . . . 22 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝) ↔ ((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝)))
42 preq12 4406 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → {(𝑢‘0), (𝑢‘1)} = {𝑃, 𝑝})
4342eqcomd 2758 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → {𝑃, 𝑝} = {(𝑢‘0), (𝑢‘1)})
4443eleq1d 2816 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 ↔ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))
4544biimpd 219 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑢‘0) = 𝑃 ∧ (𝑢‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))
4641, 45syl6bi 243 . . . . . . . . . . . . . . . . . . . . 21 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝) → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)))
4746com12 32 . . . . . . . . . . . . . . . . . . . 20 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝) → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)))
4847adantl 473 . . . . . . . . . . . . . . . . . . 19 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ({𝑃, 𝑝} ∈ 𝑋 → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)))
4948com13 88 . . . . . . . . . . . . . . . . . 18 ({𝑃, 𝑝} ∈ 𝑋 → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)))
5049ad2antll 767 . . . . . . . . . . . . . . . . 17 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)))
5150impcom 445 . . . . . . . . . . . . . . . 16 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))
5251imp 444 . . . . . . . . . . . . . . 15 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝))) → {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)
5330, 38, 523jca 1122 . . . . . . . . . . . . . 14 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝))) → ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))
54 eqcom 2759 . . . . . . . . . . . . . . . . . . . 20 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝𝑝 = ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1))
5539eqeq2d 2762 . . . . . . . . . . . . . . . . . . . . 21 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → (𝑝 = ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) ↔ 𝑝 = (𝑢‘1)))
5655biimpd 219 . . . . . . . . . . . . . . . . . . . 20 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → (𝑝 = ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) → 𝑝 = (𝑢‘1)))
5754, 56syl5bi 232 . . . . . . . . . . . . . . . . . . 19 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝𝑝 = (𝑢‘1)))
5857com12 32 . . . . . . . . . . . . . . . . . 18 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝 → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢𝑝 = (𝑢‘1)))
5958ad2antll 767 . . . . . . . . . . . . . . . . 17 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢𝑝 = (𝑢‘1)))
6059com12 32 . . . . . . . . . . . . . . . 16 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → 𝑝 = (𝑢‘1)))
6160adantr 472 . . . . . . . . . . . . . . 15 (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → 𝑝 = (𝑢‘1)))
6261imp 444 . . . . . . . . . . . . . 14 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝))) → 𝑝 = (𝑢‘1))
6322, 53, 62jca31 558 . . . . . . . . . . . . 13 ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 ∧ (𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋))) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝))) → ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))
6463exp31 631 . . . . . . . . . . . 12 ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} = 𝑢 → ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))))
6564eqcoms 2760 . . . . . . . . . . 11 (𝑢 = {⟨0, 𝑃⟩, ⟨1, 𝑝⟩} → ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))))
6665impcom 445 . . . . . . . . . 10 (((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) ∧ 𝑢 = {⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))))
6715, 66spcimedv 3424 . . . . . . . . 9 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ((({⟨0, 𝑃⟩, ⟨1, 𝑝⟩} ∈ Word 𝑉 ∧ (♯‘{⟨0, 𝑃⟩, ⟨1, 𝑝⟩}) = 2) ∧ (({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘0) = 𝑃 ∧ ({⟨0, 𝑃⟩, ⟨1, 𝑝⟩}‘1) = 𝑝)) → ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1))))
6813, 67mpd 15 . . . . . . . 8 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))
69 fveq2 6344 . . . . . . . . . . . . 13 (𝑤 = 𝑢 → (♯‘𝑤) = (♯‘𝑢))
7069eqeq1d 2754 . . . . . . . . . . . 12 (𝑤 = 𝑢 → ((♯‘𝑤) = 2 ↔ (♯‘𝑢) = 2))
71 fveq1 6343 . . . . . . . . . . . . 13 (𝑤 = 𝑢 → (𝑤‘0) = (𝑢‘0))
7271eqeq1d 2754 . . . . . . . . . . . 12 (𝑤 = 𝑢 → ((𝑤‘0) = 𝑃 ↔ (𝑢‘0) = 𝑃))
73 fveq1 6343 . . . . . . . . . . . . . 14 (𝑤 = 𝑢 → (𝑤‘1) = (𝑢‘1))
7471, 73preq12d 4412 . . . . . . . . . . . . 13 (𝑤 = 𝑢 → {(𝑤‘0), (𝑤‘1)} = {(𝑢‘0), (𝑢‘1)})
7574eleq1d 2816 . . . . . . . . . . . 12 (𝑤 = 𝑢 → ({(𝑤‘0), (𝑤‘1)} ∈ 𝑋 ↔ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋))
7670, 72, 753anbi123d 1540 . . . . . . . . . . 11 (𝑤 = 𝑢 → (((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋) ↔ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)))
7776elrab 3496 . . . . . . . . . 10 (𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ↔ (𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)))
7877anbi1i 733 . . . . . . . . 9 ((𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1)) ↔ ((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))
7978exbii 1915 . . . . . . . 8 (∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1)) ↔ ∃𝑢((𝑢 ∈ Word 𝑉 ∧ ((♯‘𝑢) = 2 ∧ (𝑢‘0) = 𝑃 ∧ {(𝑢‘0), (𝑢‘1)} ∈ 𝑋)) ∧ 𝑝 = (𝑢‘1)))
8068, 79sylibr 224 . . . . . . 7 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1)))
81 df-rex 3048 . . . . . . 7 (∃𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1) ↔ ∃𝑢(𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)} ∧ 𝑝 = (𝑢‘1)))
8280, 81sylibr 224 . . . . . 6 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1))
831rexeqi 3274 . . . . . 6 (∃𝑢𝐷 𝑝 = (𝑢‘1) ↔ ∃𝑢 ∈ {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝑋)}𝑝 = (𝑢‘1))
8482, 83sylibr 224 . . . . 5 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢𝐷 𝑝 = (𝑢‘1))
85 fveq1 6343 . . . . . . . 8 (𝑡 = 𝑢 → (𝑡‘1) = (𝑢‘1))
86 fvex 6354 . . . . . . . 8 (𝑢‘1) ∈ V
8785, 3, 86fvmpt 6436 . . . . . . 7 (𝑢𝐷 → (𝐹𝑢) = (𝑢‘1))
8887eqeq2d 2762 . . . . . 6 (𝑢𝐷 → (𝑝 = (𝐹𝑢) ↔ 𝑝 = (𝑢‘1)))
8988rexbiia 3170 . . . . 5 (∃𝑢𝐷 𝑝 = (𝐹𝑢) ↔ ∃𝑢𝐷 𝑝 = (𝑢‘1))
9084, 89sylibr 224 . . . 4 ((𝑃𝑉 ∧ (𝑝𝑉 ∧ {𝑃, 𝑝} ∈ 𝑋)) → ∃𝑢𝐷 𝑝 = (𝐹𝑢))
918, 90sylan2b 493 . . 3 ((𝑃𝑉𝑝𝑅) → ∃𝑢𝐷 𝑝 = (𝐹𝑢))
9291ralrimiva 3096 . 2 (𝑃𝑉 → ∀𝑝𝑅𝑢𝐷 𝑝 = (𝐹𝑢))
93 dffo3 6529 . 2 (𝐹:𝐷onto𝑅 ↔ (𝐹:𝐷𝑅 ∧ ∀𝑝𝑅𝑢𝐷 𝑝 = (𝐹𝑢)))
945, 92, 93sylanbrc 701 1 (𝑃𝑉𝐹:𝐷onto𝑅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1624  wex 1845  wcel 2131  wral 3042  wrex 3043  {crab 3046  Vcvv 3332  {cpr 4315  cop 4319  cmpt 4873  wf 6037  ontowfo 6039  cfv 6041  0cc0 10120  1c1 10121  2c2 11254  chash 13303  Word cword 13469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-1st 7325  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-oadd 7725  df-er 7903  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-card 8947  df-cda 9174  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-nn 11205  df-2 11263  df-n0 11477  df-z 11562  df-uz 11872  df-fz 12512  df-fzo 12652  df-hash 13304  df-word 13477
This theorem is referenced by:  wwlktovf1o  13895
  Copyright terms: Public domain W3C validator