Metamath Proof Explorer


Theorem isuvtx

Description: The set of all universal vertices. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Revised by AV, 14-Feb-2022)

Ref Expression
Hypotheses uvtxel.v 𝑉 = ( Vtx ‘ 𝐺 )
isuvtx.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion isuvtx ( UnivVtx ‘ 𝐺 ) = { 𝑣𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒𝐸 { 𝑘 , 𝑣 } ⊆ 𝑒 }

Proof

Step Hyp Ref Expression
1 uvtxel.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isuvtx.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 uvtxval ( UnivVtx ‘ 𝐺 ) = { 𝑣𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑣 ) }
4 1 2 nbgrel ( 𝑘 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ( 𝑘𝑉𝑣𝑉 ) ∧ 𝑘𝑣 ∧ ∃ 𝑒𝐸 { 𝑣 , 𝑘 } ⊆ 𝑒 ) )
5 df-3an ( ( ( 𝑘𝑉𝑣𝑉 ) ∧ 𝑘𝑣 ∧ ∃ 𝑒𝐸 { 𝑣 , 𝑘 } ⊆ 𝑒 ) ↔ ( ( ( 𝑘𝑉𝑣𝑉 ) ∧ 𝑘𝑣 ) ∧ ∃ 𝑒𝐸 { 𝑣 , 𝑘 } ⊆ 𝑒 ) )
6 4 5 bitri ( 𝑘 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ( ( 𝑘𝑉𝑣𝑉 ) ∧ 𝑘𝑣 ) ∧ ∃ 𝑒𝐸 { 𝑣 , 𝑘 } ⊆ 𝑒 ) )
7 prcom { 𝑘 , 𝑣 } = { 𝑣 , 𝑘 }
8 7 sseq1i ( { 𝑘 , 𝑣 } ⊆ 𝑒 ↔ { 𝑣 , 𝑘 } ⊆ 𝑒 )
9 8 rexbii ( ∃ 𝑒𝐸 { 𝑘 , 𝑣 } ⊆ 𝑒 ↔ ∃ 𝑒𝐸 { 𝑣 , 𝑘 } ⊆ 𝑒 )
10 id ( 𝑣𝑉𝑣𝑉 )
11 eldifi ( 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) → 𝑘𝑉 )
12 10 11 anim12ci ( ( 𝑣𝑉𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝑘𝑉𝑣𝑉 ) )
13 eldifsni ( 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) → 𝑘𝑣 )
14 13 adantl ( ( 𝑣𝑉𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → 𝑘𝑣 )
15 12 14 jca ( ( 𝑣𝑉𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( ( 𝑘𝑉𝑣𝑉 ) ∧ 𝑘𝑣 ) )
16 15 biantrurd ( ( 𝑣𝑉𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( ∃ 𝑒𝐸 { 𝑣 , 𝑘 } ⊆ 𝑒 ↔ ( ( ( 𝑘𝑉𝑣𝑉 ) ∧ 𝑘𝑣 ) ∧ ∃ 𝑒𝐸 { 𝑣 , 𝑘 } ⊆ 𝑒 ) ) )
17 9 16 bitr2id ( ( 𝑣𝑉𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( ( ( ( 𝑘𝑉𝑣𝑉 ) ∧ 𝑘𝑣 ) ∧ ∃ 𝑒𝐸 { 𝑣 , 𝑘 } ⊆ 𝑒 ) ↔ ∃ 𝑒𝐸 { 𝑘 , 𝑣 } ⊆ 𝑒 ) )
18 6 17 syl5bb ( ( 𝑣𝑉𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝑘 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∃ 𝑒𝐸 { 𝑘 , 𝑣 } ⊆ 𝑒 ) )
19 18 ralbidva ( 𝑣𝑉 → ( ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒𝐸 { 𝑘 , 𝑣 } ⊆ 𝑒 ) )
20 19 rabbiia { 𝑣𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑣 ) } = { 𝑣𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒𝐸 { 𝑘 , 𝑣 } ⊆ 𝑒 }
21 3 20 eqtri ( UnivVtx ‘ 𝐺 ) = { 𝑣𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑣 } ) ∃ 𝑒𝐸 { 𝑘 , 𝑣 } ⊆ 𝑒 }