Metamath Proof Explorer


Theorem cusgrfilem1

Description: Lemma 1 for cusgrfi . (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 11-Nov-2020)

Ref Expression
Hypotheses cusgrfi.v V = Vtx G
cusgrfi.p P = x 𝒫 V | a V a N x = a N
Assertion cusgrfilem1 G ComplUSGraph N V P Edg G

Proof

Step Hyp Ref Expression
1 cusgrfi.v V = Vtx G
2 cusgrfi.p P = x 𝒫 V | a V a N x = a N
3 eqid Edg G = Edg G
4 1 3 cusgredg G ComplUSGraph Edg G = x 𝒫 V | x = 2
5 fveq2 x = a N x = a N
6 5 ad2antlr a N x = a N a V N V x 𝒫 V x = a N
7 hashprg a V N V a N a N = 2
8 7 adantrr a V N V x 𝒫 V a N a N = 2
9 8 biimpcd a N a V N V x 𝒫 V a N = 2
10 9 adantr a N x = a N a V N V x 𝒫 V a N = 2
11 10 imp a N x = a N a V N V x 𝒫 V a N = 2
12 6 11 eqtrd a N x = a N a V N V x 𝒫 V x = 2
13 12 an13s N V x 𝒫 V a V a N x = a N x = 2
14 13 rexlimdvaa N V x 𝒫 V a V a N x = a N x = 2
15 14 ss2rabdv N V x 𝒫 V | a V a N x = a N x 𝒫 V | x = 2
16 2 a1i Edg G = x 𝒫 V | x = 2 P = x 𝒫 V | a V a N x = a N
17 id Edg G = x 𝒫 V | x = 2 Edg G = x 𝒫 V | x = 2
18 16 17 sseq12d Edg G = x 𝒫 V | x = 2 P Edg G x 𝒫 V | a V a N x = a N x 𝒫 V | x = 2
19 15 18 syl5ibr Edg G = x 𝒫 V | x = 2 N V P Edg G
20 4 19 syl G ComplUSGraph N V P Edg G
21 20 imp G ComplUSGraph N V P Edg G