| Step | Hyp | Ref
| Expression |
| 1 | | uhgrissubgr.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝑆) |
| 2 | | uhgrissubgr.a |
. . . 4
⊢ 𝐴 = (Vtx‘𝐺) |
| 3 | | uhgrissubgr.i |
. . . 4
⊢ 𝐼 = (iEdg‘𝑆) |
| 4 | | uhgrissubgr.b |
. . . 4
⊢ 𝐵 = (iEdg‘𝐺) |
| 5 | | eqid 2737 |
. . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
| 6 | 1, 2, 3, 4, 5 | subgrprop2 29291 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉)) |
| 7 | | 3simpa 1149 |
. . 3
⊢ ((𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉) → (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)) |
| 8 | 6, 7 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)) |
| 9 | | simprl 771 |
. . . 4
⊢ (((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) ∧ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)) → 𝑉 ⊆ 𝐴) |
| 10 | | simp2 1138 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → Fun 𝐵) |
| 11 | | simpr 484 |
. . . . . 6
⊢ ((𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵) → 𝐼 ⊆ 𝐵) |
| 12 | | funssres 6610 |
. . . . . 6
⊢ ((Fun
𝐵 ∧ 𝐼 ⊆ 𝐵) → (𝐵 ↾ dom 𝐼) = 𝐼) |
| 13 | 10, 11, 12 | syl2an 596 |
. . . . 5
⊢ (((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) ∧ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)) → (𝐵 ↾ dom 𝐼) = 𝐼) |
| 14 | 13 | eqcomd 2743 |
. . . 4
⊢ (((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) ∧ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)) → 𝐼 = (𝐵 ↾ dom 𝐼)) |
| 15 | | edguhgr 29146 |
. . . . . . . . 9
⊢ ((𝑆 ∈ UHGraph ∧ 𝑒 ∈ (Edg‘𝑆)) → 𝑒 ∈ 𝒫 (Vtx‘𝑆)) |
| 16 | 15 | ex 412 |
. . . . . . . 8
⊢ (𝑆 ∈ UHGraph → (𝑒 ∈ (Edg‘𝑆) → 𝑒 ∈ 𝒫 (Vtx‘𝑆))) |
| 17 | 1 | pweqi 4616 |
. . . . . . . . 9
⊢ 𝒫
𝑉 = 𝒫
(Vtx‘𝑆) |
| 18 | 17 | eleq2i 2833 |
. . . . . . . 8
⊢ (𝑒 ∈ 𝒫 𝑉 ↔ 𝑒 ∈ 𝒫 (Vtx‘𝑆)) |
| 19 | 16, 18 | imbitrrdi 252 |
. . . . . . 7
⊢ (𝑆 ∈ UHGraph → (𝑒 ∈ (Edg‘𝑆) → 𝑒 ∈ 𝒫 𝑉)) |
| 20 | 19 | ssrdv 3989 |
. . . . . 6
⊢ (𝑆 ∈ UHGraph →
(Edg‘𝑆) ⊆
𝒫 𝑉) |
| 21 | 20 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → (Edg‘𝑆) ⊆ 𝒫 𝑉) |
| 22 | 21 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) ∧ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)) → (Edg‘𝑆) ⊆ 𝒫 𝑉) |
| 23 | 1, 2, 3, 4, 5 | issubgr 29288 |
. . . . . 6
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉))) |
| 24 | 23 | 3adant2 1132 |
. . . . 5
⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉))) |
| 25 | 24 | adantr 480 |
. . . 4
⊢ (((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) ∧ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 = (𝐵 ↾ dom 𝐼) ∧ (Edg‘𝑆) ⊆ 𝒫 𝑉))) |
| 26 | 9, 14, 22, 25 | mpbir3and 1343 |
. . 3
⊢ (((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) ∧ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵)) → 𝑆 SubGraph 𝐺) |
| 27 | 26 | ex 412 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → ((𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵) → 𝑆 SubGraph 𝐺)) |
| 28 | 8, 27 | impbid2 226 |
1
⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph) → (𝑆 SubGraph 𝐺 ↔ (𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵))) |