Step |
Hyp |
Ref |
Expression |
1 |
|
edgval |
⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) |
2 |
1
|
a1i |
⊢ ( 𝐺 ∈ 𝑊 → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) ) |
3 |
2
|
eqeq1d |
⊢ ( 𝐺 ∈ 𝑊 → ( ( Edg ‘ 𝐺 ) = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ ) ) |
4 |
|
funrel |
⊢ ( Fun ( iEdg ‘ 𝐺 ) → Rel ( iEdg ‘ 𝐺 ) ) |
5 |
|
relrn0 |
⊢ ( Rel ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) = ∅ ↔ ran ( iEdg ‘ 𝐺 ) = ∅ ) ) |
6 |
5
|
bicomd |
⊢ ( Rel ( iEdg ‘ 𝐺 ) → ( ran ( iEdg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) ) |
7 |
4 6
|
syl |
⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( ran ( iEdg ‘ 𝐺 ) = ∅ ↔ ( iEdg ‘ 𝐺 ) = ∅ ) ) |
8 |
|
simpr |
⊢ ( ( ( iEdg ‘ 𝐺 ) = ∅ ∧ 𝐺 ∈ 𝑊 ) → 𝐺 ∈ 𝑊 ) |
9 |
|
simpl |
⊢ ( ( ( iEdg ‘ 𝐺 ) = ∅ ∧ 𝐺 ∈ 𝑊 ) → ( iEdg ‘ 𝐺 ) = ∅ ) |
10 |
8 9
|
usgr0e |
⊢ ( ( ( iEdg ‘ 𝐺 ) = ∅ ∧ 𝐺 ∈ 𝑊 ) → 𝐺 ∈ USGraph ) |
11 |
10
|
ex |
⊢ ( ( iEdg ‘ 𝐺 ) = ∅ → ( 𝐺 ∈ 𝑊 → 𝐺 ∈ USGraph ) ) |
12 |
7 11
|
syl6bi |
⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( ran ( iEdg ‘ 𝐺 ) = ∅ → ( 𝐺 ∈ 𝑊 → 𝐺 ∈ USGraph ) ) ) |
13 |
12
|
com13 |
⊢ ( 𝐺 ∈ 𝑊 → ( ran ( iEdg ‘ 𝐺 ) = ∅ → ( Fun ( iEdg ‘ 𝐺 ) → 𝐺 ∈ USGraph ) ) ) |
14 |
3 13
|
sylbid |
⊢ ( 𝐺 ∈ 𝑊 → ( ( Edg ‘ 𝐺 ) = ∅ → ( Fun ( iEdg ‘ 𝐺 ) → 𝐺 ∈ USGraph ) ) ) |
15 |
14
|
3imp |
⊢ ( ( 𝐺 ∈ 𝑊 ∧ ( Edg ‘ 𝐺 ) = ∅ ∧ Fun ( iEdg ‘ 𝐺 ) ) → 𝐺 ∈ USGraph ) |