Metamath Proof Explorer

Theorem uvtxupgrres

Description: A universal vertex is universal in a restricted pseudograph. (Contributed by Alexander van der Vekens, 2-Jan-2018) (Revised by AV, 8-Nov-2020)

Ref Expression
Hypotheses nbupgruvtxres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
nbupgruvtxres.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
nbupgruvtxres.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
nbupgruvtxres.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
Assertion uvtxupgrres ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝐾 ∈ ( UnivVtx ‘ 𝐺 ) → 𝐾 ∈ ( UnivVtx ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 nbupgruvtxres.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 nbupgruvtxres.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 nbupgruvtxres.f ⊢ 𝐹 = { 𝑒 ∈ 𝐸 ∣ 𝑁 ∉ 𝑒 }
4 nbupgruvtxres.s ⊢ 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( I ↾ 𝐹 ) ⟩
5 1 uvtxnbgr ⊢ ( 𝐾 ∈ ( UnivVtx ‘ 𝐺 ) → ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) )
6 1 2 3 4 nbupgruvtxres ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) → ( 𝑆 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝑁 , 𝐾 } ) ) )
7 6 imp ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → ( 𝑆 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝑁 , 𝐾 } ) )
8 difpr ⊢ ( 𝑉 ∖ { 𝑁 , 𝐾 } ) = ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } )
9 1 2 3 4 upgrres1lem2 ⊢ ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
10 9 difeq1i ⊢ ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) = ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } )
11 10 a1i ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) = ( ( 𝑉 ∖ { 𝑁 } ) ∖ { 𝐾 } ) )
12 8 11 eqtr4id ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝑉 ∖ { 𝑁 , 𝐾 } ) = ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) )
13 12 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → ( 𝑉 ∖ { 𝑁 , 𝐾 } ) = ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) )
14 7 13 eqtrd ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → ( 𝑆 NeighbVtx 𝐾 ) = ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) )
15 simpr ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) )
16 15 9 eleqtrrdi ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → 𝐾 ∈ ( Vtx ‘ 𝑆 ) )
17 16 adantr ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → 𝐾 ∈ ( Vtx ‘ 𝑆 ) )
18 eqid ⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 )
19 18 uvtxnbgrb ⊢ ( 𝐾 ∈ ( Vtx ‘ 𝑆 ) → ( 𝐾 ∈ ( UnivVtx ‘ 𝑆 ) ↔ ( 𝑆 NeighbVtx 𝐾 ) = ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) ) )
20 17 19 syl ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → ( 𝐾 ∈ ( UnivVtx ‘ 𝑆 ) ↔ ( 𝑆 NeighbVtx 𝐾 ) = ( ( Vtx ‘ 𝑆 ) ∖ { 𝐾 } ) ) )
21 14 20 mpbird ⊢ ( ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) ∧ ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) ) → 𝐾 ∈ ( UnivVtx ‘ 𝑆 ) )
22 21 ex ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( ( 𝐺 NeighbVtx 𝐾 ) = ( 𝑉 ∖ { 𝐾 } ) → 𝐾 ∈ ( UnivVtx ‘ 𝑆 ) ) )
23 5 22 syl5 ⊢ ( ( ( 𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) ) → ( 𝐾 ∈ ( UnivVtx ‘ 𝐺 ) → 𝐾 ∈ ( UnivVtx ‘ 𝑆 ) ) )