This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wwlktovf1

Description: Lemma 2 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 wwlktovf1 𝐹 : 𝐷 –1-1→ 𝑅

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 fveq1 ⊢ ( 𝑡 = 𝑥 → ( 𝑡 ‘ 1 ) = ( 𝑥 ‘ 1 ) )
6 fvex ⊢ ( 𝑥 ‘ 1 ) ∈ V
7 5 3 6 fvmpt ⊢ ( 𝑥 ∈ 𝐷 → ( 𝐹 ‘ 𝑥 ) = ( 𝑥 ‘ 1 ) )
8 fveq1 ⊢ ( 𝑡 = 𝑦 → ( 𝑡 ‘ 1 ) = ( 𝑦 ‘ 1 ) )
9 fvex ⊢ ( 𝑦 ‘ 1 ) ∈ V
10 8 3 9 fvmpt ⊢ ( 𝑦 ∈ 𝐷 → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ‘ 1 ) )
11 7 10 eqeqan12d ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) )
12 fveqeq2 ⊢ ( 𝑤 = 𝑥 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 𝑥 ) = 2 ) )
13 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ 0 ) = ( 𝑥 ‘ 0 ) )
14 13 eqeq1d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑥 ‘ 0 ) = 𝑃 ) )
15 fveq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ‘ 1 ) = ( 𝑥 ‘ 1 ) )
16 13 15 preq12d ⊢ ( 𝑤 = 𝑥 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } )
17 16 eleq1d ⊢ ( 𝑤 = 𝑥 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) )
18 12 14 17 3anbi123d ⊢ ( 𝑤 = 𝑥 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) )
19 18 1 elrab2 ⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) )
20 fveqeq2 ⊢ ( 𝑤 = 𝑦 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 𝑦 ) = 2 ) )
21 fveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
22 21 eqeq1d ⊢ ( 𝑤 = 𝑦 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑦 ‘ 0 ) = 𝑃 ) )
23 fveq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 ‘ 1 ) = ( 𝑦 ‘ 1 ) )
24 21 23 preq12d ⊢ ( 𝑤 = 𝑦 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } )
25 24 eleq1d ⊢ ( 𝑤 = 𝑦 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) )
26 20 22 25 3anbi123d ⊢ ( 𝑤 = 𝑦 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) )
27 26 1 elrab2 ⊢ ( 𝑦 ∈ 𝐷 ↔ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) )
28 simpr1 ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) → ( ♯ ‘ 𝑥 ) = 2 )
29 simpr1 ⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) → ( ♯ ‘ 𝑦 ) = 2 )
30 29 eqcomd ⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) → 2 = ( ♯ ‘ 𝑦 ) )
31 28 30 sylan9eq ⊢ ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
32 31 adantr ⊢ ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
33 simpr2 ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) → ( 𝑥 ‘ 0 ) = 𝑃 )
34 simpr2 ⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) → ( 𝑦 ‘ 0 ) = 𝑃 )
35 34 eqcomd ⊢ ( ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) → 𝑃 = ( 𝑦 ‘ 0 ) )
36 33 35 sylan9eq ⊢ ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
37 36 adantr ⊢ ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
38 simpr ⊢ ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) )
39 oveq2 ⊢ ( ( ♯ ‘ 𝑥 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝑥 ) ) = ( 0 ..^ 2 ) )
40 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
41 39 40 eqtrdi ⊢ ( ( ♯ ‘ 𝑥 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝑥 ) ) = { 0 , 1 } )
42 41 raleqdv ⊢ ( ( ♯ ‘ 𝑥 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ { 0 , 1 } ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) )
43 c0ex ⊢ 0 ∈ V
44 1ex ⊢ 1 ∈ V
45 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑥 ‘ 𝑖 ) = ( 𝑥 ‘ 0 ) )
46 fveq2 ⊢ ( 𝑖 = 0 → ( 𝑦 ‘ 𝑖 ) = ( 𝑦 ‘ 0 ) )
47 45 46 eqeq12d ⊢ ( 𝑖 = 0 → ( ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ) )
48 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑥 ‘ 𝑖 ) = ( 𝑥 ‘ 1 ) )
49 fveq2 ⊢ ( 𝑖 = 1 → ( 𝑦 ‘ 𝑖 ) = ( 𝑦 ‘ 1 ) )
50 48 49 eqeq12d ⊢ ( 𝑖 = 1 → ( ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) )
51 43 44 47 50 ralpr ⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) )
52 42 51 bitrdi ⊢ ( ( ♯ ‘ 𝑥 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) ) )
53 52 3ad2ant1 ⊢ ( ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) ) )
54 53 ad3antlr ⊢ ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ↔ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) ) )
55 37 38 54 mpbir2and ⊢ ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) )
56 eqwrd ⊢ ( ( 𝑥 ∈ Word 𝑉 ∧ 𝑦 ∈ Word 𝑉 ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) )
57 56 ad2ant2r ⊢ ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) )
58 57 adantr ⊢ ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥 ‘ 𝑖 ) = ( 𝑦 ‘ 𝑖 ) ) ) )
59 32 55 58 mpbir2and ⊢ ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → 𝑥 = 𝑦 )
60 59 ex ⊢ ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) → ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) → 𝑥 = 𝑦 ) )
61 19 27 60 syl2anb ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) → 𝑥 = 𝑦 ) )
62 11 61 sylbid ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
63 62 rgen2 ⊢ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 )
64 dff13 ⊢ ( 𝐹 : 𝐷 –1-1→ 𝑅 ↔ ( 𝐹 : 𝐷 ⟶ 𝑅 ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
65 4 63 64 mpbir2an ⊢ 𝐹 : 𝐷 –1-1→ 𝑅