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∈Va≠N∧x=aN
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∈Va≠N∧x=aN
3 eqid ⊢Edg⁡G=Edg⁡G
4 1 3 cusgredg ⊢G∈ComplUSGraph→Edg⁡G=x∈𝒫V|x=2
5 fveq2 ⊢x=aN→x=aN
6 5 ad2antlr ⊢a≠N∧x=aN∧a∈V∧N∈V∧x∈𝒫V→x=aN
7 hashprg ⊢a∈V∧N∈V→a≠N↔aN=2
8 7 adantrr ⊢a∈V∧N∈V∧x∈𝒫V→a≠N↔aN=2
9 8 biimpcd ⊢a≠N→a∈V∧N∈V∧x∈𝒫V→aN=2
10 9 adantr ⊢a≠N∧x=aN→a∈V∧N∈V∧x∈𝒫V→aN=2
11 10 imp ⊢a≠N∧x=aN∧a∈V∧N∈V∧x∈𝒫V→aN=2
12 6 11 eqtrd ⊢a≠N∧x=aN∧a∈V∧N∈V∧x∈𝒫V→x=2
13 12 an13s ⊢N∈V∧x∈𝒫V∧a∈V∧a≠N∧x=aN→x=2
14 13 rexlimdvaa ⊢N∈V∧x∈𝒫V→∃a∈Va≠N∧x=aN→x=2
15 14 ss2rabdv ⊢N∈V→x∈𝒫V|∃a∈Va≠N∧x=aN⊆x∈𝒫V|x=2
16 2 a1i ⊢Edg⁡G=x∈𝒫V|x=2→P=x∈𝒫V|∃a∈Va≠N∧x=aN
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∈Va≠N∧x=aN⊆x∈𝒫V|x=2
19 15 18 imbitrrid ⊢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