Metamath Proof Explorer

Theorem wwlktovfo

Description: Lemma 3 for wrd2f1tovbij . (Contributed by Alexander van der Vekens, 27-Jul-2018)

Ref Expression
Hypotheses wwlktovf1o.d ⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) }
wwlktovf1o.r ⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 }
wwlktovf1o.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 ‘ 1 ) )
Assertion wwlktovfo ( 𝑃 ∈ 𝑉 → 𝐹 : 𝐷 –onto→ 𝑅 )

Proof

Step Hyp Ref Expression
1 wwlktovf1o.d ⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) }
2 wwlktovf1o.r ⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 }
3 wwlktovf1o.f ⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 ‘ 1 ) )
4 1 2 3 wwlktovf ⊢ 𝐹 : 𝐷 ⟶ 𝑅
5 4 a1i ⊢ ( 𝑃 ∈ 𝑉 → 𝐹 : 𝐷 ⟶ 𝑅 )
6 preq2 ⊢ ( 𝑛 = 𝑝 → { 𝑃 , 𝑛 } = { 𝑃 , 𝑝 } )
7 6 eleq1d ⊢ ( 𝑛 = 𝑝 → ( { 𝑃 , 𝑛 } ∈ 𝑋 ↔ { 𝑃 , 𝑝 } ∈ 𝑋 ) )
8 7 2 elrab2 ⊢ ( 𝑝 ∈ 𝑅 ↔ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) )
9 simpl ⊢ ( ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) → 𝑝 ∈ 𝑉 )
10 9 anim2i ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ( 𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑉 ) )
11 eqidd ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } )
12 wrdlen2i ⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑉 ) → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) ) )
13 10 11 12 sylc ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) )
14 prex ⊢ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ V
15 14 a1i ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ V )
16 eleq1 ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ↔ 𝑢 ∈ Word 𝑉 ) )
17 16 biimpd ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 → 𝑢 ∈ Word 𝑉 ) )
18 17 adantr ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 → 𝑢 ∈ Word 𝑉 ) )
19 18 com12 ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → 𝑢 ∈ Word 𝑉 ) )
20 19 adantr ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → 𝑢 ∈ Word 𝑉 ) )
21 20 adantr ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → 𝑢 ∈ Word 𝑉 ) )
22 21 impcom ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) ) → 𝑢 ∈ Word 𝑉 )
23 fveqeq2 ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ↔ ( ♯ ‘ 𝑢 ) = 2 ) )
24 23 biimpd ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 → ( ♯ ‘ 𝑢 ) = 2 ) )
25 24 adantr ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 → ( ♯ ‘ 𝑢 ) = 2 ) )
26 25 com12 ⊢ ( ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( ♯ ‘ 𝑢 ) = 2 ) )
27 26 adantl ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( ♯ ‘ 𝑢 ) = 2 ) )
28 27 adantr ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( ♯ ‘ 𝑢 ) = 2 ) )
29 28 impcom ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) ) → ( ♯ ‘ 𝑢 ) = 2 )
30 fveq1 ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = ( 𝑢 ‘ 0 ) )
31 30 eqeq1d ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ↔ ( 𝑢 ‘ 0 ) = 𝑃 ) )
32 31 biimpd ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 → ( 𝑢 ‘ 0 ) = 𝑃 ) )
33 32 adantr ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 → ( 𝑢 ‘ 0 ) = 𝑃 ) )
34 33 com12 ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( 𝑢 ‘ 0 ) = 𝑃 ) )
35 34 adantr ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( 𝑢 ‘ 0 ) = 𝑃 ) )
36 35 adantl ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( 𝑢 ‘ 0 ) = 𝑃 ) )
37 36 impcom ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) ) → ( 𝑢 ‘ 0 ) = 𝑃 )
38 fveq1 ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = ( 𝑢 ‘ 1 ) )
39 38 eqeq1d ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ↔ ( 𝑢 ‘ 1 ) = 𝑝 ) )
40 31 39 anbi12d ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ↔ ( ( 𝑢 ‘ 0 ) = 𝑃 ∧ ( 𝑢 ‘ 1 ) = 𝑝 ) ) )
41 preq12 ⊢ ( ( ( 𝑢 ‘ 0 ) = 𝑃 ∧ ( 𝑢 ‘ 1 ) = 𝑝 ) → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } = { 𝑃 , 𝑝 } )
42 41 eqcomd ⊢ ( ( ( 𝑢 ‘ 0 ) = 𝑃 ∧ ( 𝑢 ‘ 1 ) = 𝑝 ) → { 𝑃 , 𝑝 } = { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } )
43 42 eleq1d ⊢ ( ( ( 𝑢 ‘ 0 ) = 𝑃 ∧ ( 𝑢 ‘ 1 ) = 𝑝 ) → ( { 𝑃 , 𝑝 } ∈ 𝑋 ↔ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) )
44 43 biimpd ⊢ ( ( ( 𝑢 ‘ 0 ) = 𝑃 ∧ ( 𝑢 ‘ 1 ) = 𝑝 ) → ( { 𝑃 , 𝑝 } ∈ 𝑋 → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) )
45 40 44 syl6bi ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) → ( { 𝑃 , 𝑝 } ∈ 𝑋 → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) )
46 45 com12 ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( { 𝑃 , 𝑝 } ∈ 𝑋 → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) )
47 46 adantl ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( { 𝑃 , 𝑝 } ∈ 𝑋 → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) )
48 47 com13 ⊢ ( { 𝑃 , 𝑝 } ∈ 𝑋 → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) )
49 48 ad2antll ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) )
50 49 impcom ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) )
51 50 imp ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) ) → { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 )
52 29 37 51 3jca ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) ) → ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) )
53 eqcom ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ↔ 𝑝 = ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) )
54 38 eqeq2d ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( 𝑝 = ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) ↔ 𝑝 = ( 𝑢 ‘ 1 ) ) )
55 54 biimpd ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( 𝑝 = ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) → 𝑝 = ( 𝑢 ‘ 1 ) ) )
56 53 55 syl5bi ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 → 𝑝 = ( 𝑢 ‘ 1 ) ) )
57 56 com12 ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → 𝑝 = ( 𝑢 ‘ 1 ) ) )
58 57 ad2antll ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → 𝑝 = ( 𝑢 ‘ 1 ) ) )
59 58 com12 ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → 𝑝 = ( 𝑢 ‘ 1 ) ) )
60 59 adantr ⊢ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → 𝑝 = ( 𝑢 ‘ 1 ) ) )
61 60 imp ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) ) → 𝑝 = ( 𝑢 ‘ 1 ) )
62 22 52 61 jca31 ⊢ ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 ∧ ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) ) → ( ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) )
63 62 exp31 ⊢ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } = 𝑢 → ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ( ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) ) ) )
64 63 eqcoms ⊢ ( 𝑢 = { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } → ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ( ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) ) ) )
65 64 impcom ⊢ ( ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) ∧ 𝑢 = { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ( ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) ) )
66 15 65 spcimedv ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ( ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ∈ Word 𝑉 ∧ ( ♯ ‘ { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ) = 2 ) ∧ ( ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 0 ) = 𝑃 ∧ ( { ⟨ 0 , 𝑃 ⟩ , ⟨ 1 , 𝑝 ⟩ } ‘ 1 ) = 𝑝 ) ) → ∃ 𝑢 ( ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) ) )
67 13 66 mpd ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ∃ 𝑢 ( ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) )
68 fveqeq2 ⊢ ( 𝑤 = 𝑢 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 𝑢 ) = 2 ) )
69 fveq1 ⊢ ( 𝑤 = 𝑢 → ( 𝑤 ‘ 0 ) = ( 𝑢 ‘ 0 ) )
70 69 eqeq1d ⊢ ( 𝑤 = 𝑢 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑢 ‘ 0 ) = 𝑃 ) )
71 fveq1 ⊢ ( 𝑤 = 𝑢 → ( 𝑤 ‘ 1 ) = ( 𝑢 ‘ 1 ) )
72 69 71 preq12d ⊢ ( 𝑤 = 𝑢 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } )
73 72 eleq1d ⊢ ( 𝑤 = 𝑢 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) )
74 68 70 73 3anbi123d ⊢ ( 𝑤 = 𝑢 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) )
75 74 elrab ⊢ ( 𝑢 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } ↔ ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) )
76 75 anbi1i ⊢ ( ( 𝑢 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) ↔ ( ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) )
77 76 exbii ⊢ ( ∃ 𝑢 ( 𝑢 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) ↔ ∃ 𝑢 ( ( 𝑢 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑢 ) = 2 ∧ ( 𝑢 ‘ 0 ) = 𝑃 ∧ { ( 𝑢 ‘ 0 ) , ( 𝑢 ‘ 1 ) } ∈ 𝑋 ) ) ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) )
78 67 77 sylibr ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ∃ 𝑢 ( 𝑢 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) )
79 df-rex ⊢ ( ∃ 𝑢 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } 𝑝 = ( 𝑢 ‘ 1 ) ↔ ∃ 𝑢 ( 𝑢 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } ∧ 𝑝 = ( 𝑢 ‘ 1 ) ) )
80 78 79 sylibr ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ∃ 𝑢 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } 𝑝 = ( 𝑢 ‘ 1 ) )
81 1 rexeqi ⊢ ( ∃ 𝑢 ∈ 𝐷 𝑝 = ( 𝑢 ‘ 1 ) ↔ ∃ 𝑢 ∈ { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) } 𝑝 = ( 𝑢 ‘ 1 ) )
82 80 81 sylibr ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ∃ 𝑢 ∈ 𝐷 𝑝 = ( 𝑢 ‘ 1 ) )
83 fveq1 ⊢ ( 𝑡 = 𝑢 → ( 𝑡 ‘ 1 ) = ( 𝑢 ‘ 1 ) )
84 fvex ⊢ ( 𝑢 ‘ 1 ) ∈ V
85 83 3 84 fvmpt ⊢ ( 𝑢 ∈ 𝐷 → ( 𝐹 ‘ 𝑢 ) = ( 𝑢 ‘ 1 ) )
86 85 eqeq2d ⊢ ( 𝑢 ∈ 𝐷 → ( 𝑝 = ( 𝐹 ‘ 𝑢 ) ↔ 𝑝 = ( 𝑢 ‘ 1 ) ) )
87 86 rexbiia ⊢ ( ∃ 𝑢 ∈ 𝐷 𝑝 = ( 𝐹 ‘ 𝑢 ) ↔ ∃ 𝑢 ∈ 𝐷 𝑝 = ( 𝑢 ‘ 1 ) )
88 82 87 sylibr ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ( 𝑝 ∈ 𝑉 ∧ { 𝑃 , 𝑝 } ∈ 𝑋 ) ) → ∃ 𝑢 ∈ 𝐷 𝑝 = ( 𝐹 ‘ 𝑢 ) )
89 8 88 sylan2b ⊢ ( ( 𝑃 ∈ 𝑉 ∧ 𝑝 ∈ 𝑅 ) → ∃ 𝑢 ∈ 𝐷 𝑝 = ( 𝐹 ‘ 𝑢 ) )
90 89 ralrimiva ⊢ ( 𝑃 ∈ 𝑉 → ∀ 𝑝 ∈ 𝑅 ∃ 𝑢 ∈ 𝐷 𝑝 = ( 𝐹 ‘ 𝑢 ) )
91 dffo3 ⊢ ( 𝐹 : 𝐷 –onto→ 𝑅 ↔ ( 𝐹 : 𝐷 ⟶ 𝑅 ∧ ∀ 𝑝 ∈ 𝑅 ∃ 𝑢 ∈ 𝐷 𝑝 = ( 𝐹 ‘ 𝑢 ) ) )
92 5 90 91 sylanbrc ⊢ ( 𝑃 ∈ 𝑉 → 𝐹 : 𝐷 –onto→ 𝑅 )