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 )