Step | Hyp | Ref
| Expression |
1 | | eqid 2825 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
2 | | eqid 2825 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2825 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
4 | | eqid 2825 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
5 | | eqid 2825 |
. . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
6 | 1, 2, 3, 4, 5 | subgrprop2 26578 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))) |
7 | | upgruhgr 26407 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈
UHGraph) |
8 | | subgruhgrfun 26586 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
9 | 7, 8 | sylan 575 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
10 | 9 | ancoms 452 |
. . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → Fun
(iEdg‘𝑆)) |
11 | | funfn 6157 |
. . . . . . . 8
⊢ (Fun
(iEdg‘𝑆) ↔
(iEdg‘𝑆) Fn dom
(iEdg‘𝑆)) |
12 | 10, 11 | sylib 210 |
. . . . . . 7
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
13 | 12 | adantl 475 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
14 | 7 | anim2i 610 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) |
15 | 14 | adantl 475 |
. . . . . . . . . . . . 13
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph)) |
16 | 15 | ancomd 455 |
. . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺)) |
17 | 16 | anim1i 608 |
. . . . . . . . . . 11
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝑆))) |
18 | 17 | simplld 784 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UHGraph) |
19 | | simpl 476 |
. . . . . . . . . . . 12
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → 𝑆 SubGraph 𝐺) |
20 | 19 | adantl 475 |
. . . . . . . . . . 11
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → 𝑆 SubGraph 𝐺) |
21 | 20 | adantr 474 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) |
22 | | simpr 479 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) |
23 | 1, 3, 18, 21, 22 | subgruhgredgd 26588 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖
{∅})) |
24 | 4 | uhgrfun 26371 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
25 | 7, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UPGraph → Fun
(iEdg‘𝐺)) |
26 | 25 | ad2antll 720 |
. . . . . . . . . . . . . 14
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → Fun
(iEdg‘𝐺)) |
27 | 26 | adantr 474 |
. . . . . . . . . . . . 13
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → Fun (iEdg‘𝐺)) |
28 | | simpll2 1275 |
. . . . . . . . . . . . 13
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (iEdg‘𝑆) ⊆ (iEdg‘𝐺)) |
29 | | funssfv 6458 |
. . . . . . . . . . . . 13
⊢ ((Fun
(iEdg‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝑆)‘𝑥)) |
30 | 27, 28, 22, 29 | syl3anc 1494 |
. . . . . . . . . . . 12
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝑆)‘𝑥)) |
31 | 30 | eqcomd 2831 |
. . . . . . . . . . 11
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) = ((iEdg‘𝐺)‘𝑥)) |
32 | 31 | fveq2d 6441 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (♯‘((iEdg‘𝑆)‘𝑥)) = (♯‘((iEdg‘𝐺)‘𝑥))) |
33 | | subgreldmiedg 26587 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝐺)) |
34 | 33 | ex 403 |
. . . . . . . . . . . . . 14
⊢ (𝑆 SubGraph 𝐺 → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) |
35 | 34 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) |
36 | 35 | adantl 475 |
. . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) |
37 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → 𝐺 ∈ UPGraph) |
38 | | funfn 6157 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
39 | 25, 38 | sylib 210 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
40 | 39 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
41 | | simpl 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) → 𝑥 ∈ dom (iEdg‘𝐺)) |
42 | 2, 4 | upgrle 26395 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ UPGraph ∧
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝐺)) →
(♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2) |
43 | 37, 40, 41, 42 | syl3anc 1494 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph) →
(♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2) |
44 | 43 | expcom 404 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ UPGraph → (𝑥 ∈ dom (iEdg‘𝐺) →
(♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) |
45 | 44 | ad2antll 720 |
. . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑥 ∈ dom (iEdg‘𝐺) → (♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) |
46 | 36, 45 | syld 47 |
. . . . . . . . . . 11
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑥 ∈ dom (iEdg‘𝑆) → (♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) |
47 | 46 | imp 397 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (♯‘((iEdg‘𝐺)‘𝑥)) ≤ 2) |
48 | 32, 47 | eqbrtrd 4897 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (♯‘((iEdg‘𝑆)‘𝑥)) ≤ 2) |
49 | | fveq2 6437 |
. . . . . . . . . . 11
⊢ (𝑒 = ((iEdg‘𝑆)‘𝑥) → (♯‘𝑒) = (♯‘((iEdg‘𝑆)‘𝑥))) |
50 | 49 | breq1d 4885 |
. . . . . . . . . 10
⊢ (𝑒 = ((iEdg‘𝑆)‘𝑥) → ((♯‘𝑒) ≤ 2 ↔
(♯‘((iEdg‘𝑆)‘𝑥)) ≤ 2)) |
51 | 50 | elrab 3585 |
. . . . . . . . 9
⊢
(((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤ 2}
↔ (((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∧
(♯‘((iEdg‘𝑆)‘𝑥)) ≤ 2)) |
52 | 23, 48, 51 | sylanbrc 578 |
. . . . . . . 8
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2}) |
53 | 52 | ralrimiva 3175 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2}) |
54 | | fnfvrnss 6644 |
. . . . . . 7
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤ 2})
→ ran (iEdg‘𝑆)
⊆ {𝑒 ∈
(𝒫 (Vtx‘𝑆)
∖ {∅}) ∣ (♯‘𝑒) ≤ 2}) |
55 | 13, 53, 54 | syl2anc 579 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}) ∣ (♯‘𝑒) ≤ 2}) |
56 | | df-f 6131 |
. . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤ 2}
↔ ((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
ran (iEdg‘𝑆) ⊆
{𝑒 ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}) ∣ (♯‘𝑒) ≤ 2})) |
57 | 13, 55, 56 | sylanbrc 578 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2}) |
58 | | subgrv 26574 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
59 | 1, 3 | isupgr 26389 |
. . . . . . . . 9
⊢ (𝑆 ∈ V → (𝑆 ∈ UPGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) |
60 | 59 | adantr 474 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ∈ UPGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) |
61 | 58, 60 | syl 17 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ UPGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) |
62 | 61 | adantr 474 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → (𝑆 ∈ UPGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) |
63 | 62 | adantl 475 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → (𝑆 ∈ UPGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(♯‘𝑒) ≤
2})) |
64 | 57, 63 | mpbird 249 |
. . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph)) → 𝑆 ∈ UPGraph) |
65 | 64 | ex 403 |
. . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → 𝑆 ∈ UPGraph)) |
66 | 6, 65 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph) → 𝑆 ∈ UPGraph)) |
67 | 66 | anabsi8 662 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UPGraph) |