| 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 |  | upgruhgr 29120 | . . . . . . . . . 10
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈
UHGraph) | 
| 8 |  | subgruhgrfun 29300 | . . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) | 
| 9 | 7, 8 | sylan 580 | . . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) | 
| 10 | 9 | ancoms 458 | . . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → Fun
(iEdg‘𝑆)) | 
| 11 | 10 | funfnd 6596 | . . . . . . 7
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) | 
| 12 | 11 | adantl 481 | . . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) | 
| 13 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑒 = ((iEdg‘𝑆)‘𝑥) → (♯‘𝑒) = (♯‘((iEdg‘𝑆)‘𝑥))) | 
| 14 | 13 | breq1d 5152 | . . . . . . . . 9
⊢ (𝑒 = ((iEdg‘𝑆)‘𝑥) → ((♯‘𝑒) ≤ 2 ↔
(♯‘((iEdg‘𝑆)‘𝑥)) ≤ 2)) | 
| 15 | 7 | anim2i 617 | . . . . . . . . . . . . . 14
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) | 
| 16 | 15 | adantl 481 | . . . . . . . . . . . . 13
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) | 
| 17 | 16 | ancomd 461 | . . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺)) | 
| 18 | 17 | anim1i 615 | . . . . . . . . . . 11
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝑆))) | 
| 19 | 18 | simplld 767 | . . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UHGraph) | 
| 20 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → 𝑆 SubGraph 𝐺) | 
| 21 | 20 | adantl 481 | . . . . . . . . . . 11
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → 𝑆 SubGraph 𝐺) | 
| 22 | 21 | adantr 480 | . . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) | 
| 23 |  | simpr 484 | . . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) | 
| 24 | 1, 3, 19, 22, 23 | subgruhgredgd 29302 | . . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖
{∅})) | 
| 25 | 4 | uhgrfun 29084 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) | 
| 26 | 7, 25 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UPGraph → Fun
(iEdg‘𝐺)) | 
| 27 | 26 | ad2antll 729 | . . . . . . . . . . . . . 14
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → Fun
(iEdg‘𝐺)) | 
| 28 | 27 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → Fun (iEdg‘𝐺)) | 
| 29 |  | simpll2 1213 | . . . . . . . . . . . . 13
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (iEdg‘𝑆) ⊆ (iEdg‘𝐺)) | 
| 30 |  | funssfv 6926 | . . . . . . . . . . . . 13
⊢ ((Fun
(iEdg‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝑆)‘𝑥)) | 
| 31 | 28, 29, 23, 30 | syl3anc 1372 | . . . . . . . . . . . 12
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝑆)‘𝑥)) | 
| 32 | 31 | eqcomd 2742 | . . . . . . . . . . 11
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) = ((iEdg‘𝐺)‘𝑥)) | 
| 33 | 32 | fveq2d 6909 | . . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (♯‘((iEdg‘𝑆)‘𝑥)) = (♯‘((iEdg‘𝐺)‘𝑥))) | 
| 34 |  | subgreldmiedg 29301 | . . . . . . . . . . . . . . 15
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝐺)) | 
| 35 | 34 | ex 412 | . . . . . . . . . . . . . 14
⊢ (𝑆 SubGraph 𝐺 → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) | 
| 37 | 36 | adantl 481 | . . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) | 
| 38 |  | simpr 484 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → 𝐺 ∈ UPGraph) | 
| 39 | 26 | funfnd 6596 | . . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) | 
| 40 | 39 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) | 
| 41 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → 𝑥 ∈ dom (iEdg‘𝐺)) | 
| 42 | 2, 4 | upgrle 29108 | . . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ UPGraph ∧
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝐺)) →
(♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2) | 
| 43 | 38, 40, 41, 42 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) →
(♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2) | 
| 44 | 43 | expcom 413 | . . . . . . . . . . . . 13
⊢ (𝐺 ∈ UPGraph → (𝑥 ∈ dom (iEdg‘𝐺) →
(♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) | 
| 45 | 44 | ad2antll 729 | . . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑥 ∈ dom (iEdg‘𝐺) → (♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) | 
| 46 | 37, 45 | syld 47 | . . . . . . . . . . 11
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑥 ∈ dom (iEdg‘𝑆) → (♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) | 
| 47 | 46 | imp 406 | . . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2) | 
| 48 | 33, 47 | eqbrtrd 5164 | . . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (♯‘((iEdg‘𝑆)‘𝑥)) ≤ 2) | 
| 49 | 14, 24, 48 | elrabd 3693 | . . . . . . . 8
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2}) | 
| 50 | 49 | ralrimiva 3145 | . . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2}) | 
| 51 |  | fnfvrnss 7140 | . . . . . . 7
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤ 2})
→ ran (iEdg‘𝑆)
⊆ {𝑒 ∈
(𝒫 (Vtx‘𝑆)
∖ {∅}) ∣ (♯‘𝑒) ≤ 2}) | 
| 52 | 12, 50, 51 | syl2anc 584 | . . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}) ∣ (♯‘𝑒) ≤ 2}) | 
| 53 |  | df-f 6564 | . . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤ 2}
↔ ((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
ran (iEdg‘𝑆) ⊆
{𝑒 ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}) ∣ (♯‘𝑒) ≤ 2})) | 
| 54 | 12, 52, 53 | sylanbrc 583 | . . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2}) | 
| 55 |  | subgrv 29288 | . . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) | 
| 56 | 1, 3 | isupgr 29102 | . . . . . . . . 9
⊢ (𝑆 ∈ V → (𝑆 ∈ UPGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) | 
| 57 | 56 | adantr 480 | . . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ∈ UPGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) | 
| 58 | 55, 57 | syl 17 | . . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ UPGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) | 
| 59 | 58 | adantr 480 | . . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → (𝑆 ∈ UPGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) | 
| 60 | 59 | adantl 481 | . . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑆 ∈ UPGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) | 
| 61 | 54, 60 | mpbird 257 | . . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → 𝑆 ∈ UPGraph) | 
| 62 | 61 | ex 412 | . . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → 𝑆 ∈ UPGraph)) | 
| 63 | 6, 62 | syl 17 | . 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → 𝑆 ∈ UPGraph)) | 
| 64 | 63 | anabsi8 672 | 1
⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UPGraph) |