This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cusgrres.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
cusgrres.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
cusgrres.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
Assertion cusgrres ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ ComplUSGraph )

Proof

Step Hyp Ref Expression
1 cusgrres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrres.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 cusgrres.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4 cusgrres.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
5 cusgrusgr ⊢ ( 𝐺 ∈ ComplUSGraph → 𝐺 ∈ USGraph )
6 1 2 3 4 usgrres1 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ USGraph )
7 5 6 sylan ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ USGraph )
8 iscusgr ⊢ ( 𝐺 ∈ ComplUSGraph ↔ ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) )
9 usgrupgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UPGraph )
10 9 adantr ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) → 𝐺 ∈ UPGraph )
11 10 anim1i ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) )
12 11 anim1i ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) )
13 1 iscplgr ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑛 ∈ 𝑉 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ) )
14 eldifi ⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) → 𝑣 ∈ 𝑉 )
15 14 ad2antll ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) → 𝑣 ∈ 𝑉 )
16 eleq1w ⊢ ( 𝑛 = 𝑣 → ( 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) ↔ 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
17 16 rspcv ⊢ ( 𝑣 ∈ 𝑉 → ( ∀ 𝑛 ∈ 𝑉 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
18 15 17 syl ⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ) → ( ∀ 𝑛 ∈ 𝑉 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
19 18 ex ⊢ ( 𝐺 ∈ USGraph → ( ( 𝑁 ∈ 𝑉 ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ∀ 𝑛 ∈ 𝑉 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) ) )
20 19 com23 ⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑛 ∈ 𝑉 𝑛 ∈ ( UnivVtx ‘ 𝐺 ) → ( ( 𝑁 ∈ 𝑉 ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) ) )
21 13 20 sylbid ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 ∈ ComplGraph → ( ( 𝑁 ∈ 𝑉 ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) ) )
22 21 imp ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) → ( ( 𝑁 ∈ 𝑉 ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
23 22 impl ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
24 1 2 3 4 uvtxupgrres ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) → 𝑣 ∈ ( UnivVtx ‘ 𝑆 ) ) )
25 12 23 24 sylc ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝑣 ∈ ( UnivVtx ‘ 𝑆 ) )
26 25 ralrimiva ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐺 ∈ ComplGraph ) ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑣 ∈ ( UnivVtx ‘ 𝑆 ) )
27 8 26 sylanb ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑣 ∈ ( UnivVtx ‘ 𝑆 ) )
28 opex ⊢ ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩ ∈ V
29 4 28 eqeltri ⊢ 𝑆 ∈ V
30 1 2 3 4 upgrres1lem2 ⊢ ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
31 30 eqcomi ⊢ ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
32 31 iscplgr ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑣 ∈ ( UnivVtx ‘ 𝑆 ) ) )
33 29 32 mp1i ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝑆 ∈ ComplGraph ↔ ∀ 𝑣 ∈ ( 𝑉 ∖ { 𝑁 } ) 𝑣 ∈ ( UnivVtx ‘ 𝑆 ) ) )
34 27 33 mpbird ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ ComplGraph )
35 iscusgr ⊢ ( 𝑆 ∈ ComplUSGraph ↔ ( 𝑆 ∈ USGraph ∧ 𝑆 ∈ ComplGraph ) )
36 7 34 35 sylanbrc ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑆 ∈ ComplUSGraph )