Step |
Hyp |
Ref |
Expression |
1 |
|
0ss |
⊢ ∅ ⊆ ( Vtx ‘ 𝐺 ) |
2 |
|
dm0 |
⊢ dom ∅ = ∅ |
3 |
2
|
reseq2i |
⊢ ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) = ( ( iEdg ‘ 𝐺 ) ↾ ∅ ) |
4 |
|
res0 |
⊢ ( ( iEdg ‘ 𝐺 ) ↾ ∅ ) = ∅ |
5 |
3 4
|
eqtr2i |
⊢ ∅ = ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) |
6 |
|
0ss |
⊢ ∅ ⊆ 𝒫 ∅ |
7 |
1 5 6
|
3pm3.2i |
⊢ ( ∅ ⊆ ( Vtx ‘ 𝐺 ) ∧ ∅ = ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) ∧ ∅ ⊆ 𝒫 ∅ ) |
8 |
|
0ex |
⊢ ∅ ∈ V |
9 |
|
vtxval0 |
⊢ ( Vtx ‘ ∅ ) = ∅ |
10 |
9
|
eqcomi |
⊢ ∅ = ( Vtx ‘ ∅ ) |
11 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
12 |
|
iedgval0 |
⊢ ( iEdg ‘ ∅ ) = ∅ |
13 |
12
|
eqcomi |
⊢ ∅ = ( iEdg ‘ ∅ ) |
14 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
15 |
|
edgval |
⊢ ( Edg ‘ ∅ ) = ran ( iEdg ‘ ∅ ) |
16 |
12
|
rneqi |
⊢ ran ( iEdg ‘ ∅ ) = ran ∅ |
17 |
|
rn0 |
⊢ ran ∅ = ∅ |
18 |
15 16 17
|
3eqtrri |
⊢ ∅ = ( Edg ‘ ∅ ) |
19 |
10 11 13 14 18
|
issubgr |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ∅ ∈ V ) → ( ∅ SubGraph 𝐺 ↔ ( ∅ ⊆ ( Vtx ‘ 𝐺 ) ∧ ∅ = ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) ∧ ∅ ⊆ 𝒫 ∅ ) ) ) |
20 |
8 19
|
mpan2 |
⊢ ( 𝐺 ∈ 𝑊 → ( ∅ SubGraph 𝐺 ↔ ( ∅ ⊆ ( Vtx ‘ 𝐺 ) ∧ ∅ = ( ( iEdg ‘ 𝐺 ) ↾ dom ∅ ) ∧ ∅ ⊆ 𝒫 ∅ ) ) ) |
21 |
7 20
|
mpbiri |
⊢ ( 𝐺 ∈ 𝑊 → ∅ SubGraph 𝐺 ) |