| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) | 
| 2 |  | eqid 2736 | . . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) | 
| 3 |  | eqid 2736 | . . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) | 
| 4 |  | eqid 2736 | . . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) | 
| 5 |  | eqid 2736 | . . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) | 
| 6 | 1, 2, 3, 4, 5 | subgrprop2 29292 | . . 3
⊢ (𝑆 SubGraph 𝐺 → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))) | 
| 7 |  | subgruhgrfun 29300 | . . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) | 
| 8 | 7 | ancoms 458 | . . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph) → Fun
(iEdg‘𝑆)) | 
| 9 | 8 | adantl 481 | . . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) → Fun
(iEdg‘𝑆)) | 
| 10 | 9 | funfnd 6596 | . . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) | 
| 11 |  | simplrr 777 | . . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UHGraph) | 
| 12 |  | simplrl 776 | . . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) | 
| 13 |  | simpr 484 | . . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) | 
| 14 | 1, 3, 11, 12, 13 | subgruhgredgd 29302 | . . . . . . . 8
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖
{∅})) | 
| 15 | 14 | ralrimiva 3145 | . . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖
{∅})) | 
| 16 |  | fnfvrnss 7140 | . . . . . . 7
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅})) → ran
(iEdg‘𝑆) ⊆
(𝒫 (Vtx‘𝑆)
∖ {∅})) | 
| 17 | 10, 15, 16 | syl2anc 584 | . . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) → ran
(iEdg‘𝑆) ⊆
(𝒫 (Vtx‘𝑆)
∖ {∅})) | 
| 18 |  | df-f 6564 | . . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) ↔
((iEdg‘𝑆) Fn dom
(iEdg‘𝑆) ∧ ran
(iEdg‘𝑆) ⊆
(𝒫 (Vtx‘𝑆)
∖ {∅}))) | 
| 19 | 10, 17, 18 | sylanbrc 583 | . . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅})) | 
| 20 |  | subgrv 29288 | . . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) | 
| 21 | 1, 3 | isuhgr 29078 | . . . . . . . . 9
⊢ (𝑆 ∈ V → (𝑆 ∈ UHGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖
{∅}))) | 
| 22 | 21 | adantr 480 | . . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ∈ UHGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖
{∅}))) | 
| 23 | 20, 22 | syl 17 | . . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}))) | 
| 24 | 23 | adantr 480 | . . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph) → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}))) | 
| 25 | 24 | adantl 481 | . . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}))) | 
| 26 | 19, 25 | mpbird 257 | . . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) → 𝑆 ∈ UHGraph) | 
| 27 | 26 | ex 412 | . . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph) → 𝑆 ∈ UHGraph)) | 
| 28 | 6, 27 | syl 17 | . 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph) → 𝑆 ∈ UHGraph)) | 
| 29 | 28 | anabsi8 672 | 1
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UHGraph) |