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
|
syl5bb |
⊢ ( 𝐺 ∈ 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 ) → ¬ ∃ 𝑣 ∈ 𝑉 { 𝑈 , 𝑣 } ∈ 𝐸 ) |