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 ⊢V=Vtx⁡G
frgrncvvdeq.e ⊢E=Edg⁡G
frgrncvvdeq.nx ⊢D=GNeighbVtxX
frgrncvvdeq.ny ⊢N=GNeighbVtxY
frgrncvvdeq.x ⊢φ→X∈V
frgrncvvdeq.y ⊢φ→Y∈V
frgrncvvdeq.ne ⊢φ→X≠Y
frgrncvvdeq.xy ⊢φ→Y∉D
frgrncvvdeq.f ⊢φ→G∈FriendGraph
frgrncvvdeq.a ⊢A=x∈D⟼ιy∈N|xy∈E
Assertion frgrncvvdeqlem9 ⊢φ→A:D⟶ontoN

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v1 ⊢V=Vtx⁡G
2 frgrncvvdeq.e ⊢E=Edg⁡G
3 frgrncvvdeq.nx ⊢D=GNeighbVtxX
4 frgrncvvdeq.ny ⊢N=GNeighbVtxY
5 frgrncvvdeq.x ⊢φ→X∈V
6 frgrncvvdeq.y ⊢φ→Y∈V
7 frgrncvvdeq.ne ⊢φ→X≠Y
8 frgrncvvdeq.xy ⊢φ→Y∉D
9 frgrncvvdeq.f ⊢φ→G∈FriendGraph
10 frgrncvvdeq.a ⊢A=x∈D⟼ιy∈N|xy∈E
11 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem4 ⊢φ→A:D⟶N
12 9 adantr ⊢φ∧n∈N→G∈FriendGraph
13 4 eleq2i ⊢n∈N↔n∈GNeighbVtxY
14 1 nbgrisvtx ⊢n∈GNeighbVtxY→n∈V
15 14 a1i ⊢φ→n∈GNeighbVtxY→n∈V
16 13 15 biimtrid ⊢φ→n∈N→n∈V
17 16 imp ⊢φ∧n∈N→n∈V
18 5 adantr ⊢φ∧n∈N→X∈V
19 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem1 ⊢φ→X∉N
20 df-nel ⊢X∉N↔¬X∈N
21 nelelne ⊢¬X∈N→n∈N→n≠X
22 20 21 sylbi ⊢X∉N→n∈N→n≠X
23 19 22 syl ⊢φ→n∈N→n≠X
24 23 imp ⊢φ∧n∈N→n≠X
25 17 18 24 3jca ⊢φ∧n∈N→n∈V∧X∈V∧n≠X
26 12 25 jca ⊢φ∧n∈N→G∈FriendGraph∧n∈V∧X∈V∧n≠X
27 1 2 frcond2 ⊢G∈FriendGraph→n∈V∧X∈V∧n≠X→∃!m∈Vnm∈E∧mX∈E
28 27 imp ⊢G∈FriendGraph∧n∈V∧X∈V∧n≠X→∃!m∈Vnm∈E∧mX∈E
29 reurex ⊢∃!m∈Vnm∈E∧mX∈E→∃m∈Vnm∈E∧mX∈E
30 df-rex ⊢∃m∈Vnm∈E∧mX∈E↔∃mm∈V∧nm∈E∧mX∈E
31 29 30 sylib ⊢∃!m∈Vnm∈E∧mX∈E→∃mm∈V∧nm∈E∧mX∈E
32 26 28 31 3syl ⊢φ∧n∈N→∃mm∈V∧nm∈E∧mX∈E
33 frgrusgr ⊢G∈FriendGraph→G∈USGraph
34 2 nbusgreledg ⊢G∈USGraph→m∈GNeighbVtxX↔mX∈E
35 34 bicomd ⊢G∈USGraph→mX∈E↔m∈GNeighbVtxX
36 9 33 35 3syl ⊢φ→mX∈E↔m∈GNeighbVtxX
37 36 biimpa ⊢φ∧mX∈E→m∈GNeighbVtxX
38 3 eleq2i ⊢m∈D↔m∈GNeighbVtxX
39 37 38 sylibr ⊢φ∧mX∈E→m∈D
40 39 ad2ant2rl ⊢φ∧n∈N∧nm∈E∧mX∈E→m∈D
41 2 nbusgreledg ⊢G∈USGraph→n∈GNeighbVtxm↔nm∈E
42 41 biimpar ⊢G∈USGraph∧nm∈E→n∈GNeighbVtxm
43 42 a1d ⊢G∈USGraph∧nm∈E→mX∈E→n∈GNeighbVtxm
44 43 expimpd ⊢G∈USGraph→nm∈E∧mX∈E→n∈GNeighbVtxm
45 9 33 44 3syl ⊢φ→nm∈E∧mX∈E→n∈GNeighbVtxm
46 45 adantr ⊢φ∧n∈N→nm∈E∧mX∈E→n∈GNeighbVtxm
47 46 imp ⊢φ∧n∈N∧nm∈E∧mX∈E→n∈GNeighbVtxm
48 elin ⊢n∈GNeighbVtxm∩N↔n∈GNeighbVtxm∧n∈N
49 simpl ⊢φ∧mX∈E→φ
50 49 39 jca ⊢φ∧mX∈E→φ∧m∈D
51 preq1 ⊢x=m→xy=my
52 51 eleq1d ⊢x=m→xy∈E↔my∈E
53 52 riotabidv ⊢x=m→ιy∈N|xy∈E=ιy∈N|my∈E
54 53 cbvmptv ⊢x∈D⟼ιy∈N|xy∈E=m∈D⟼ιy∈N|my∈E
55 10 54 eqtri ⊢A=m∈D⟼ιy∈N|my∈E
56 1 2 3 4 5 6 7 8 9 55 frgrncvvdeqlem5 ⊢φ∧m∈D→A⁡m=GNeighbVtxm∩N
57 eleq2 ⊢GNeighbVtxm∩N=A⁡m→n∈GNeighbVtxm∩N↔n∈A⁡m
58 57 eqcoms ⊢A⁡m=GNeighbVtxm∩N→n∈GNeighbVtxm∩N↔n∈A⁡m
59 elsni ⊢n∈A⁡m→n=A⁡m
60 58 59 syl6bi ⊢A⁡m=GNeighbVtxm∩N→n∈GNeighbVtxm∩N→n=A⁡m
61 50 56 60 3syl ⊢φ∧mX∈E→n∈GNeighbVtxm∩N→n=A⁡m
62 61 expcom ⊢mX∈E→φ→n∈GNeighbVtxm∩N→n=A⁡m
63 62 com3r ⊢n∈GNeighbVtxm∩N→mX∈E→φ→n=A⁡m
64 48 63 sylbir ⊢n∈GNeighbVtxm∧n∈N→mX∈E→φ→n=A⁡m
65 64 ex ⊢n∈GNeighbVtxm→n∈N→mX∈E→φ→n=A⁡m
66 65 com14 ⊢φ→n∈N→mX∈E→n∈GNeighbVtxm→n=A⁡m
67 66 imp ⊢φ∧n∈N→mX∈E→n∈GNeighbVtxm→n=A⁡m
68 67 adantld ⊢φ∧n∈N→nm∈E∧mX∈E→n∈GNeighbVtxm→n=A⁡m
69 68 imp ⊢φ∧n∈N∧nm∈E∧mX∈E→n∈GNeighbVtxm→n=A⁡m
70 47 69 mpd ⊢φ∧n∈N∧nm∈E∧mX∈E→n=A⁡m
71 40 70 jca ⊢φ∧n∈N∧nm∈E∧mX∈E→m∈D∧n=A⁡m
72 71 ex ⊢φ∧n∈N→nm∈E∧mX∈E→m∈D∧n=A⁡m
73 72 adantld ⊢φ∧n∈N→m∈V∧nm∈E∧mX∈E→m∈D∧n=A⁡m
74 73 eximdv ⊢φ∧n∈N→∃mm∈V∧nm∈E∧mX∈E→∃mm∈D∧n=A⁡m
75 32 74 mpd ⊢φ∧n∈N→∃mm∈D∧n=A⁡m
76 df-rex ⊢∃m∈Dn=A⁡m↔∃mm∈D∧n=A⁡m
77 75 76 sylibr ⊢φ∧n∈N→∃m∈Dn=A⁡m
78 77 ralrimiva ⊢φ→∀n∈N∃m∈Dn=A⁡m
79 dffo3 ⊢A:D⟶ontoN↔A:D⟶N∧∀n∈N∃m∈Dn=A⁡m
80 11 78 79 sylanbrc ⊢φ→A:D⟶ontoN