Metamath Proof Explorer

Theorem frgrncvvdeqlem8

Description: Lemma 8 for frgrncvvdeq . This corresponds to statement 2 in Huneke p. 1: "The map is one-to-one since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021) (Revised by AV, 30-Dec-2021)

Ref Expression
Hypotheses frgrncvvdeq.v1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgrncvvdeq.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
frgrncvvdeq.nx ⊢ 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
frgrncvvdeq.ny ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑌 )
frgrncvvdeq.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
frgrncvvdeq.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
frgrncvvdeq.ne ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
frgrncvvdeq.xy ⊢ ( 𝜑 → 𝑌 ∉ 𝐷 )
frgrncvvdeq.f ⊢ ( 𝜑 → 𝐺 ∈ FriendGraph )
frgrncvvdeq.a ⊢ 𝐴 = ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
Assertion frgrncvvdeqlem8 ( 𝜑 → 𝐴 : 𝐷 –1-1→ 𝑁 )

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v1 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrncvvdeq.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 frgrncvvdeq.nx ⊢ 𝐷 = ( 𝐺 NeighbVtx 𝑋 )
4 frgrncvvdeq.ny ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑌 )
5 frgrncvvdeq.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6 frgrncvvdeq.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 frgrncvvdeq.ne ⊢ ( 𝜑 → 𝑋 ≠ 𝑌 )
8 frgrncvvdeq.xy ⊢ ( 𝜑 → 𝑌 ∉ 𝐷 )
9 frgrncvvdeq.f ⊢ ( 𝜑 → 𝐺 ∈ FriendGraph )
10 frgrncvvdeq.a ⊢ 𝐴 = ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) )
11 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem4 ⊢ ( 𝜑 → 𝐴 : 𝐷 ⟶ 𝑁 )
12 simpr ⊢ ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) → 𝐴 : 𝐷 ⟶ 𝑁 )
13 ffvelrn ⊢ ( ( 𝐴 : 𝐷 ⟶ 𝑁 ∧ 𝑢 ∈ 𝐷 ) → ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 )
14 13 ad2ant2lr ⊢ ( ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 )
15 14 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) ) → ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 )
16 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem1 ⊢ ( 𝜑 → 𝑋 ∉ 𝑁 )
17 preq1 ⊢ ( 𝑥 = 𝑢 → { 𝑥 , 𝑦 } = { 𝑢 , 𝑦 } )
18 17 eleq1d ⊢ ( 𝑥 = 𝑢 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑢 , 𝑦 } ∈ 𝐸 ) )
19 18 riotabidv ⊢ ( 𝑥 = 𝑢 → ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) = ( ℩ 𝑦 ∈ 𝑁 { 𝑢 , 𝑦 } ∈ 𝐸 ) )
20 19 cbvmptv ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ) = ( 𝑢 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑢 , 𝑦 } ∈ 𝐸 ) )
21 10 20 eqtri ⊢ 𝐴 = ( 𝑢 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑢 , 𝑦 } ∈ 𝐸 ) )
22 1 2 3 4 5 6 7 8 9 21 frgrncvvdeqlem6 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐷 ) → { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 )
23 preq1 ⊢ ( 𝑥 = 𝑤 → { 𝑥 , 𝑦 } = { 𝑤 , 𝑦 } )
24 23 eleq1d ⊢ ( 𝑥 = 𝑤 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑤 , 𝑦 } ∈ 𝐸 ) )
25 24 riotabidv ⊢ ( 𝑥 = 𝑤 → ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) = ( ℩ 𝑦 ∈ 𝑁 { 𝑤 , 𝑦 } ∈ 𝐸 ) )
26 25 cbvmptv ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ) = ( 𝑤 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑤 , 𝑦 } ∈ 𝐸 ) )
27 10 26 eqtri ⊢ 𝐴 = ( 𝑤 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑤 , 𝑦 } ∈ 𝐸 ) )
28 1 2 3 4 5 6 7 8 9 27 frgrncvvdeqlem6 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝐷 ) → { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 )
29 22 28 anim12dan ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 ) )
30 preq2 ⊢ ( ( 𝐴 ‘ 𝑤 ) = ( 𝐴 ‘ 𝑢 ) → { 𝑤 , ( 𝐴 ‘ 𝑤 ) } = { 𝑤 , ( 𝐴 ‘ 𝑢 ) } )
31 30 eleq1d ⊢ ( ( 𝐴 ‘ 𝑤 ) = ( 𝐴 ‘ 𝑢 ) → ( { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 ↔ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) )
32 31 anbi2d ⊢ ( ( 𝐴 ‘ 𝑤 ) = ( 𝐴 ‘ 𝑢 ) → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 ) ↔ ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) ) )
33 32 eqcoms ⊢ ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 ) ↔ ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) ) )
34 33 biimpa ⊢ ( ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) ∧ ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 ) ) → ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) )
35 df-ne ⊢ ( 𝑢 ≠ 𝑤 ↔ ¬ 𝑢 = 𝑤 )
36 2 3 frgrnbnb ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 ≠ 𝑤 ) → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) → ( 𝐴 ‘ 𝑢 ) = 𝑋 ) )
37 9 36 syl3an1 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ∧ 𝑢 ≠ 𝑤 ) → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) → ( 𝐴 ‘ 𝑢 ) = 𝑋 ) )
38 37 3expa ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) ∧ 𝑢 ≠ 𝑤 ) → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) → ( 𝐴 ‘ 𝑢 ) = 𝑋 ) )
39 df-nel ⊢ ( 𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁 )
40 eleq1 ⊢ ( ( 𝐴 ‘ 𝑢 ) = 𝑋 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 ↔ 𝑋 ∈ 𝑁 ) )
41 40 biimpa ⊢ ( ( ( 𝐴 ‘ 𝑢 ) = 𝑋 ∧ ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 ) → 𝑋 ∈ 𝑁 )
42 41 pm2.24d ⊢ ( ( ( 𝐴 ‘ 𝑢 ) = 𝑋 ∧ ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 ) → ( ¬ 𝑋 ∈ 𝑁 → 𝑢 = 𝑤 ) )
43 42 expcom ⊢ ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) = 𝑋 → ( ¬ 𝑋 ∈ 𝑁 → 𝑢 = 𝑤 ) ) )
44 43 com13 ⊢ ( ¬ 𝑋 ∈ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) = 𝑋 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) )
45 39 44 sylbi ⊢ ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) = 𝑋 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) )
46 45 com12 ⊢ ( ( 𝐴 ‘ 𝑢 ) = 𝑋 → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) )
47 38 46 syl6 ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) ∧ 𝑢 ≠ 𝑤 ) → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) )
48 47 expcom ⊢ ( 𝑢 ≠ 𝑤 → ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) )
49 48 com23 ⊢ ( 𝑢 ≠ 𝑤 → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) → ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) )
50 35 49 sylbir ⊢ ( ¬ 𝑢 = 𝑤 → ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ) → ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) )
51 34 50 syl5com ⊢ ( ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) ∧ ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 ) ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) )
52 51 expcom ⊢ ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 ) → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) ) )
53 52 com24 ⊢ ( ( { 𝑢 , ( 𝐴 ‘ 𝑢 ) } ∈ 𝐸 ∧ { 𝑤 , ( 𝐴 ‘ 𝑤 ) } ∈ 𝐸 ) → ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) ) )
54 29 53 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) )
55 54 ex ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) ) )
56 55 com3r ⊢ ( ¬ 𝑢 = 𝑤 → ( 𝜑 → ( ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( 𝑋 ∉ 𝑁 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) ) )
57 56 com15 ⊢ ( 𝑋 ∉ 𝑁 → ( 𝜑 → ( ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) ) )
58 16 57 mpcom ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) )
59 58 expd ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐷 → ( 𝑤 ∈ 𝐷 → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) → ( 𝑢 ∈ 𝐷 → ( 𝑤 ∈ 𝐷 → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) ) ) ) )
61 60 imp42 ⊢ ( ( ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) ) → ( ¬ 𝑢 = 𝑤 → ( ( 𝐴 ‘ 𝑢 ) ∈ 𝑁 → 𝑢 = 𝑤 ) ) )
62 15 61 mpid ⊢ ( ( ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) ) → ( ¬ 𝑢 = 𝑤 → 𝑢 = 𝑤 ) )
63 62 pm2.18d ⊢ ( ( ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) ∧ ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) ) → 𝑢 = 𝑤 )
64 63 ex ⊢ ( ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) ∧ ( 𝑢 ∈ 𝐷 ∧ 𝑤 ∈ 𝐷 ) ) → ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → 𝑢 = 𝑤 ) )
65 64 ralrimivva ⊢ ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) → ∀ 𝑢 ∈ 𝐷 ∀ 𝑤 ∈ 𝐷 ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → 𝑢 = 𝑤 ) )
66 dff13 ⊢ ( 𝐴 : 𝐷 –1-1→ 𝑁 ↔ ( 𝐴 : 𝐷 ⟶ 𝑁 ∧ ∀ 𝑢 ∈ 𝐷 ∀ 𝑤 ∈ 𝐷 ( ( 𝐴 ‘ 𝑢 ) = ( 𝐴 ‘ 𝑤 ) → 𝑢 = 𝑤 ) ) )
67 12 65 66 sylanbrc ⊢ ( ( 𝜑 ∧ 𝐴 : 𝐷 ⟶ 𝑁 ) → 𝐴 : 𝐷 –1-1→ 𝑁 )
68 11 67 mpdan ⊢ ( 𝜑 → 𝐴 : 𝐷 –1-1→ 𝑁 )