Metamath Proof Explorer

Theorem vtxduhgr0nedg

Description: If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017) (Revised by AV, 15-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdushgrfvedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
vtxdushgrfvedg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
Assertion vtxduhgr0nedg ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑈 ) = 0 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdushgrfvedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 vtxdushgrfvedg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
4 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
5 1 4 3 vtxd0nedgb ⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
6 5 adantl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
7 2 eleq2i ⊢ ( { 𝑈 , 𝑣 } ∈ 𝐸 ↔ { 𝑈 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) )
8 4 uhgredgiedgb ⊢ ( 𝐺 ∈ UHGraph → ( { 𝑈 , 𝑣 } ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝑈 , 𝑣 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
9 7 8 bitrid ⊢ ( 𝐺 ∈ UHGraph → ( { 𝑈 , 𝑣 } ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝑈 , 𝑣 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
10 9 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑈 , 𝑣 } ∈ 𝐸 ↔ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝑈 , 𝑣 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
11 prid1g ⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ { 𝑈 , 𝑣 } )
12 eleq2 ⊢ ( { 𝑈 , 𝑣 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ( 𝑈 ∈ { 𝑈 , 𝑣 } ↔ 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
13 11 12 syl5ibcom ⊢ ( 𝑈 ∈ 𝑉 → ( { 𝑈 , 𝑣 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
14 13 adantl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑈 , 𝑣 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
15 14 reximdv ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) { 𝑈 , 𝑣 } = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
16 10 15 sylbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( { 𝑈 , 𝑣 } ∈ 𝐸 → ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
17 16 rexlimdvw ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 → ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
18 17 con3d ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝑈 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )
19 6 18 sylbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑈 ) = 0 → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) )
20 19 3impia ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑈 ∈ 𝑉 ∧ ( 𝐷 ‘ 𝑈 ) = 0 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 )