Metamath Proof Explorer

Theorem cusgrres

Description: Restricting a complete simple graph. (Contributed by Alexander van der Vekens, 2-Jan-2018)

Ref Expression
Hypotheses cusgrres.v ⊢V=Vtx⁡G
cusgrres.e ⊢E=Edg⁡G
cusgrres.f ⊢F=e∈E|N∉e
cusgrres.s ⊢S=V∖NI↾F
Assertion cusgrres ⊢G∈ComplUSGraph∧N∈V→S∈ComplUSGraph

Proof

Step Hyp Ref Expression
1 cusgrres.v ⊢V=Vtx⁡G
2 cusgrres.e ⊢E=Edg⁡G
3 cusgrres.f ⊢F=e∈E|N∉e
4 cusgrres.s ⊢S=V∖NI↾F
5 cusgrusgr ⊢G∈ComplUSGraph→G∈USGraph
6 1 2 3 4 usgrres1 ⊢G∈USGraph∧N∈V→S∈USGraph
7 5 6 sylan ⊢G∈ComplUSGraph∧N∈V→S∈USGraph
8 iscusgr ⊢G∈ComplUSGraph↔G∈USGraph∧G∈ComplGraph
9 usgrupgr ⊢G∈USGraph→G∈UPGraph
10 9 adantr ⊢G∈USGraph∧G∈ComplGraph→G∈UPGraph
11 10 anim1i ⊢G∈USGraph∧G∈ComplGraph∧N∈V→G∈UPGraph∧N∈V
12 11 anim1i ⊢G∈USGraph∧G∈ComplGraph∧N∈V∧v∈V∖N→G∈UPGraph∧N∈V∧v∈V∖N
13 1 iscplgr ⊢G∈USGraph→G∈ComplGraph↔∀n∈Vn∈UnivVtx⁡G
14 eldifi ⊢v∈V∖N→v∈V
15 14 ad2antll ⊢G∈USGraph∧N∈V∧v∈V∖N→v∈V
16 eleq1w ⊢n=v→n∈UnivVtx⁡G↔v∈UnivVtx⁡G
17 16 rspcv ⊢v∈V→∀n∈Vn∈UnivVtx⁡G→v∈UnivVtx⁡G
18 15 17 syl ⊢G∈USGraph∧N∈V∧v∈V∖N→∀n∈Vn∈UnivVtx⁡G→v∈UnivVtx⁡G
19 18 ex ⊢G∈USGraph→N∈V∧v∈V∖N→∀n∈Vn∈UnivVtx⁡G→v∈UnivVtx⁡G
20 19 com23 ⊢G∈USGraph→∀n∈Vn∈UnivVtx⁡G→N∈V∧v∈V∖N→v∈UnivVtx⁡G
21 13 20 sylbid ⊢G∈USGraph→G∈ComplGraph→N∈V∧v∈V∖N→v∈UnivVtx⁡G
22 21 imp ⊢G∈USGraph∧G∈ComplGraph→N∈V∧v∈V∖N→v∈UnivVtx⁡G
23 22 impl ⊢G∈USGraph∧G∈ComplGraph∧N∈V∧v∈V∖N→v∈UnivVtx⁡G
24 1 2 3 4 uvtxupgrres ⊢G∈UPGraph∧N∈V∧v∈V∖N→v∈UnivVtx⁡G→v∈UnivVtx⁡S
25 12 23 24 sylc ⊢G∈USGraph∧G∈ComplGraph∧N∈V∧v∈V∖N→v∈UnivVtx⁡S
26 25 ralrimiva ⊢G∈USGraph∧G∈ComplGraph∧N∈V→∀v∈V∖Nv∈UnivVtx⁡S
27 8 26 sylanb ⊢G∈ComplUSGraph∧N∈V→∀v∈V∖Nv∈UnivVtx⁡S
28 opex ⊢V∖NI↾F∈V
29 4 28 eqeltri ⊢S∈V
30 1 2 3 4 upgrres1lem2 ⊢Vtx⁡S=V∖N
31 30 eqcomi ⊢V∖N=Vtx⁡S
32 31 iscplgr ⊢S∈V→S∈ComplGraph↔∀v∈V∖Nv∈UnivVtx⁡S
33 29 32 mp1i ⊢G∈ComplUSGraph∧N∈V→S∈ComplGraph↔∀v∈V∖Nv∈UnivVtx⁡S
34 27 33 mpbird ⊢G∈ComplUSGraph∧N∈V→S∈ComplGraph
35 iscusgr ⊢S∈ComplUSGraph↔S∈USGraph∧S∈ComplGraph
36 7 34 35 sylanbrc ⊢G∈ComplUSGraph∧N∈V→S∈ComplUSGraph