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 ∖ N I ↾ 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 ∖ N I ↾ 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 ∈ V n ∈ 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 ∈ V n ∈ UnivVtx ⁡ G → v ∈ UnivVtx ⁡ G
18 15 17 syl ⊢ G ∈ USGraph ∧ N ∈ V ∧ v ∈ V ∖ N → ∀ n ∈ V n ∈ UnivVtx ⁡ G → v ∈ UnivVtx ⁡ G
19 18 ex ⊢ G ∈ USGraph → N ∈ V ∧ v ∈ V ∖ N → ∀ n ∈ V n ∈ UnivVtx ⁡ G → v ∈ UnivVtx ⁡ G
20 19 com23 ⊢ G ∈ USGraph → ∀ n ∈ V n ∈ 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 ∖ N v ∈ UnivVtx ⁡ S
27 8 26 sylanb ⊢ G ∈ ComplUSGraph ∧ N ∈ V → ∀ v ∈ V ∖ N v ∈ UnivVtx ⁡ S
28 opex ⊢ V ∖ N I ↾ 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 ∖ N v ∈ UnivVtx ⁡ S
33 29 32 mp1i ⊢ G ∈ ComplUSGraph ∧ N ∈ V → S ∈ ComplGraph ↔ ∀ v ∈ V ∖ N v ∈ 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