Metamath Proof Explorer

Theorem frgrncvvdeqlem9

Description: Lemma 9 for frgrncvvdeq . This corresponds to statement 3 in Huneke p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 12-Feb-2022)

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 frgrncvvdeqlem9 ( 𝜑 → 𝐴 : 𝐷 –onto→ 𝑁 )

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 9 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝐺 ∈ FriendGraph )
13 4 eleq2i ⊢ ( 𝑛 ∈ 𝑁 ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) )
14 1 nbgrisvtx ⊢ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) → 𝑛 ∈ 𝑉 )
15 14 a1i ⊢ ( 𝜑 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑌 ) → 𝑛 ∈ 𝑉 ) )
16 13 15 syl5bi ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑁 → 𝑛 ∈ 𝑉 ) )
17 16 imp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝑛 ∈ 𝑉 )
18 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝑋 ∈ 𝑉 )
19 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem1 ⊢ ( 𝜑 → 𝑋 ∉ 𝑁 )
20 df-nel ⊢ ( 𝑋 ∉ 𝑁 ↔ ¬ 𝑋 ∈ 𝑁 )
21 nelelne ⊢ ( ¬ 𝑋 ∈ 𝑁 → ( 𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋 ) )
22 20 21 sylbi ⊢ ( 𝑋 ∉ 𝑁 → ( 𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋 ) )
23 19 22 syl ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑁 → 𝑛 ≠ 𝑋 ) )
24 23 imp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → 𝑛 ≠ 𝑋 )
25 17 18 24 3jca ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋 ) )
26 12 25 jca ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( 𝐺 ∈ FriendGraph ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋 ) ) )
27 1 2 frcond2 ⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋 ) → ∃! 𝑚 ∈ 𝑉 ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) )
28 27 imp ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑛 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑛 ≠ 𝑋 ) ) → ∃! 𝑚 ∈ 𝑉 ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) )
29 reurex ⊢ ( ∃! 𝑚 ∈ 𝑉 ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → ∃ 𝑚 ∈ 𝑉 ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) )
30 df-rex ⊢ ( ∃ 𝑚 ∈ 𝑉 ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ↔ ∃ 𝑚 ( 𝑚 ∈ 𝑉 ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) )
31 29 30 sylib ⊢ ( ∃! 𝑚 ∈ 𝑉 ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → ∃ 𝑚 ( 𝑚 ∈ 𝑉 ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) )
32 26 28 31 3syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ∃ 𝑚 ( 𝑚 ∈ 𝑉 ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) )
33 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
34 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑚 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ { 𝑚 , 𝑋 } ∈ 𝐸 ) )
35 34 bicomd ⊢ ( 𝐺 ∈ USGraph → ( { 𝑚 , 𝑋 } ∈ 𝐸 ↔ 𝑚 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) )
36 9 33 35 3syl ⊢ ( 𝜑 → ( { 𝑚 , 𝑋 } ∈ 𝐸 ↔ 𝑚 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) )
37 36 biimpa ⊢ ( ( 𝜑 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → 𝑚 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
38 3 eleq2i ⊢ ( 𝑚 ∈ 𝐷 ↔ 𝑚 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
39 37 38 sylibr ⊢ ( ( 𝜑 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → 𝑚 ∈ 𝐷 )
40 39 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) → 𝑚 ∈ 𝐷 )
41 2 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) ↔ { 𝑛 , 𝑚 } ∈ 𝐸 ) )
42 41 biimpar ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑛 , 𝑚 } ∈ 𝐸 ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) )
43 42 a1d ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑛 , 𝑚 } ∈ 𝐸 ) → ( { 𝑚 , 𝑋 } ∈ 𝐸 → 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) ) )
44 43 expimpd ⊢ ( 𝐺 ∈ USGraph → ( ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) ) )
45 9 33 44 3syl ⊢ ( 𝜑 → ( ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) ) )
46 45 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) ) )
47 46 imp ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) → 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) )
48 elin ⊢ ( 𝑛 ∈ ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) ↔ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) ∧ 𝑛 ∈ 𝑁 ) )
49 simpl ⊢ ( ( 𝜑 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → 𝜑 )
50 49 39 jca ⊢ ( ( 𝜑 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → ( 𝜑 ∧ 𝑚 ∈ 𝐷 ) )
51 preq1 ⊢ ( 𝑥 = 𝑚 → { 𝑥 , 𝑦 } = { 𝑚 , 𝑦 } )
52 51 eleq1d ⊢ ( 𝑥 = 𝑚 → ( { 𝑥 , 𝑦 } ∈ 𝐸 ↔ { 𝑚 , 𝑦 } ∈ 𝐸 ) )
53 52 riotabidv ⊢ ( 𝑥 = 𝑚 → ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) = ( ℩ 𝑦 ∈ 𝑁 { 𝑚 , 𝑦 } ∈ 𝐸 ) )
54 53 cbvmptv ⊢ ( 𝑥 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑥 , 𝑦 } ∈ 𝐸 ) ) = ( 𝑚 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑚 , 𝑦 } ∈ 𝐸 ) )
55 10 54 eqtri ⊢ 𝐴 = ( 𝑚 ∈ 𝐷 ↦ ( ℩ 𝑦 ∈ 𝑁 { 𝑚 , 𝑦 } ∈ 𝐸 ) )
56 1 2 3 4 5 6 7 8 9 55 frgrncvvdeqlem5 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝐷 ) → { ( 𝐴 ‘ 𝑚 ) } = ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) )
57 eleq2 ⊢ ( ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) = { ( 𝐴 ‘ 𝑚 ) } → ( 𝑛 ∈ ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) ↔ 𝑛 ∈ { ( 𝐴 ‘ 𝑚 ) } ) )
58 57 eqcoms ⊢ ( { ( 𝐴 ‘ 𝑚 ) } = ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) → ( 𝑛 ∈ ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) ↔ 𝑛 ∈ { ( 𝐴 ‘ 𝑚 ) } ) )
59 elsni ⊢ ( 𝑛 ∈ { ( 𝐴 ‘ 𝑚 ) } → 𝑛 = ( 𝐴 ‘ 𝑚 ) )
60 58 59 syl6bi ⊢ ( { ( 𝐴 ‘ 𝑚 ) } = ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) → ( 𝑛 ∈ ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) )
61 50 56 60 3syl ⊢ ( ( 𝜑 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → ( 𝑛 ∈ ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) )
62 61 expcom ⊢ ( { 𝑚 , 𝑋 } ∈ 𝐸 → ( 𝜑 → ( 𝑛 ∈ ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) )
63 62 com3r ⊢ ( 𝑛 ∈ ( ( 𝐺 NeighbVtx 𝑚 ) ∩ 𝑁 ) → ( { 𝑚 , 𝑋 } ∈ 𝐸 → ( 𝜑 → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) )
64 48 63 sylbir ⊢ ( ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) ∧ 𝑛 ∈ 𝑁 ) → ( { 𝑚 , 𝑋 } ∈ 𝐸 → ( 𝜑 → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) )
65 64 ex ⊢ ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) → ( 𝑛 ∈ 𝑁 → ( { 𝑚 , 𝑋 } ∈ 𝐸 → ( 𝜑 → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) ) )
66 65 com14 ⊢ ( 𝜑 → ( 𝑛 ∈ 𝑁 → ( { 𝑚 , 𝑋 } ∈ 𝐸 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) ) )
67 66 imp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( { 𝑚 , 𝑋 } ∈ 𝐸 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) )
68 67 adantld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) )
69 68 imp ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑚 ) → 𝑛 = ( 𝐴 ‘ 𝑚 ) ) )
70 47 69 mpd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) → 𝑛 = ( 𝐴 ‘ 𝑚 ) )
71 40 70 jca ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) → ( 𝑚 ∈ 𝐷 ∧ 𝑛 = ( 𝐴 ‘ 𝑚 ) ) )
72 71 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) → ( 𝑚 ∈ 𝐷 ∧ 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) )
73 72 adantld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( ( 𝑚 ∈ 𝑉 ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) → ( 𝑚 ∈ 𝐷 ∧ 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) )
74 73 eximdv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ( ∃ 𝑚 ( 𝑚 ∈ 𝑉 ∧ ( { 𝑛 , 𝑚 } ∈ 𝐸 ∧ { 𝑚 , 𝑋 } ∈ 𝐸 ) ) → ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = ( 𝐴 ‘ 𝑚 ) ) ) )
75 32 74 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = ( 𝐴 ‘ 𝑚 ) ) )
76 df-rex ⊢ ( ∃ 𝑚 ∈ 𝐷 𝑛 = ( 𝐴 ‘ 𝑚 ) ↔ ∃ 𝑚 ( 𝑚 ∈ 𝐷 ∧ 𝑛 = ( 𝐴 ‘ 𝑚 ) ) )
77 75 76 sylibr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑁 ) → ∃ 𝑚 ∈ 𝐷 𝑛 = ( 𝐴 ‘ 𝑚 ) )
78 77 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑁 ∃ 𝑚 ∈ 𝐷 𝑛 = ( 𝐴 ‘ 𝑚 ) )
79 dffo3 ⊢ ( 𝐴 : 𝐷 –onto→ 𝑁 ↔ ( 𝐴 : 𝐷 ⟶ 𝑁 ∧ ∀ 𝑛 ∈ 𝑁 ∃ 𝑚 ∈ 𝐷 𝑛 = ( 𝐴 ‘ 𝑚 ) ) )
80 11 78 79 sylanbrc ⊢ ( 𝜑 → 𝐴 : 𝐷 –onto→ 𝑁 )