Metamath Proof Explorer

Theorem frgrncvvdeqlem6

Description: Lemma 6 for frgrncvvdeq . (Contributed by Alexander van der Vekens, 23-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 30-Dec-2021)

Ref Expression
Hypotheses frgrncvvdeq.v1 ⊢ V = Vtx ⁡ G
frgrncvvdeq.e ⊢ E = Edg ⁡ G
frgrncvvdeq.nx ⊢ D = G NeighbVtx X
frgrncvvdeq.ny ⊢ N = G NeighbVtx Y
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 | x y ∈ E
Assertion frgrncvvdeqlem6 ⊢ φ ∧ x ∈ D → x A ⁡ x ∈ E

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v1 ⊢ V = Vtx ⁡ G
2 frgrncvvdeq.e ⊢ E = Edg ⁡ G
3 frgrncvvdeq.nx ⊢ D = G NeighbVtx X
4 frgrncvvdeq.ny ⊢ N = G NeighbVtx Y
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 | x y ∈ E
11 1 2 3 4 5 6 7 8 9 10 frgrncvvdeqlem5 ⊢ φ ∧ x ∈ D → A ⁡ x = G NeighbVtx x ∩ N
12 fvex ⊢ A ⁡ x ∈ V
13 elinsn ⊢ A ⁡ x ∈ V ∧ G NeighbVtx x ∩ N = A ⁡ x → A ⁡ x ∈ G NeighbVtx x ∧ A ⁡ x ∈ N
14 12 13 mpan ⊢ G NeighbVtx x ∩ N = A ⁡ x → A ⁡ x ∈ G NeighbVtx x ∧ A ⁡ x ∈ N
15 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
16 2 nbusgreledg ⊢ G ∈ USGraph → A ⁡ x ∈ G NeighbVtx x ↔ A ⁡ x x ∈ E
17 prcom ⊢ A ⁡ x x = x A ⁡ x
18 17 eleq1i ⊢ A ⁡ x x ∈ E ↔ x A ⁡ x ∈ E
19 16 18 bitrdi ⊢ G ∈ USGraph → A ⁡ x ∈ G NeighbVtx x ↔ x A ⁡ x ∈ E
20 19 biimpd ⊢ G ∈ USGraph → A ⁡ x ∈ G NeighbVtx x → x A ⁡ x ∈ E
21 9 15 20 3syl ⊢ φ → A ⁡ x ∈ G NeighbVtx x → x A ⁡ x ∈ E
22 21 adantr ⊢ φ ∧ x ∈ D → A ⁡ x ∈ G NeighbVtx x → x A ⁡ x ∈ E
23 22 com12 ⊢ A ⁡ x ∈ G NeighbVtx x → φ ∧ x ∈ D → x A ⁡ x ∈ E
24 23 adantr ⊢ A ⁡ x ∈ G NeighbVtx x ∧ A ⁡ x ∈ N → φ ∧ x ∈ D → x A ⁡ x ∈ E
25 14 24 syl ⊢ G NeighbVtx x ∩ N = A ⁡ x → φ ∧ x ∈ D → x A ⁡ x ∈ E
26 25 eqcoms ⊢ A ⁡ x = G NeighbVtx x ∩ N → φ ∧ x ∈ D → x A ⁡ x ∈ E
27 11 26 mpcom ⊢ φ ∧ x ∈ D → x A ⁡ x ∈ E