Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
2 | | eqid 2610 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
4 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
5 | | eqid 2610 |
. . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
6 | 1, 2, 3, 4, 5 | subgrprop2 40498 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))) |
7 | | upgruhgr 25768 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph
) |
8 | | subgruhgrfun 40506 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
9 | 7, 8 | sylan 487 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
10 | 9 | ancoms 468 |
. . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph ) → Fun
(iEdg‘𝑆)) |
11 | | funfn 5833 |
. . . . . . . 8
⊢ (Fun
(iEdg‘𝑆) ↔
(iEdg‘𝑆) Fn dom
(iEdg‘𝑆)) |
12 | 10, 11 | sylib 207 |
. . . . . . 7
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph ) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
13 | 12 | adantl 481 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
14 | 7 | anim2i 591 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph ) → (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) |
15 | 14 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) |
16 | 15 | ancomd 466 |
. . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → (𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺)) |
17 | 16 | anim1i 590 |
. . . . . . . . . . 11
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝑆))) |
18 | 17 | simplld 787 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UHGraph ) |
19 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph ) → 𝑆 SubGraph 𝐺) |
20 | 19 | adantl 481 |
. . . . . . . . . . 11
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → 𝑆 SubGraph 𝐺) |
21 | 20 | adantr 480 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) |
22 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) |
23 | 1, 3, 18, 21, 22 | subgruhgredgd 40508 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖
{∅})) |
24 | 4 | uhgrfun 25732 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
25 | 7, 24 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐺 ∈ UPGraph → Fun
(iEdg‘𝐺)) |
26 | 25 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → Fun
(iEdg‘𝐺)) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → Fun (iEdg‘𝐺)) |
28 | | simpll2 1094 |
. . . . . . . . . . . . 13
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (iEdg‘𝑆) ⊆ (iEdg‘𝐺)) |
29 | | funssfv 6119 |
. . . . . . . . . . . . 13
⊢ ((Fun
(iEdg‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝑆)‘𝑥)) |
30 | 27, 28, 22, 29 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝐺)‘𝑥) = ((iEdg‘𝑆)‘𝑥)) |
31 | 30 | eqcomd 2616 |
. . . . . . . . . . 11
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) = ((iEdg‘𝐺)‘𝑥)) |
32 | 31 | fveq2d 6107 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (#‘((iEdg‘𝑆)‘𝑥)) = (#‘((iEdg‘𝐺)‘𝑥))) |
33 | | subgreldmiedg 40507 |
. . . . . . . . . . . . . . 15
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝐺)) |
34 | 33 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (𝑆 SubGraph 𝐺 → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph ) → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) |
36 | 35 | adantl 481 |
. . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → (𝑥 ∈ dom (iEdg‘𝑆) → 𝑥 ∈ dom (iEdg‘𝐺))) |
37 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) → 𝐺 ∈ UPGraph ) |
38 | | funfn 5833 |
. . . . . . . . . . . . . . . . 17
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
39 | 25, 38 | sylib 207 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
41 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) → 𝑥 ∈ dom (iEdg‘𝐺)) |
42 | 2, 4 | upgrle 25757 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 ∈ UPGraph ∧
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺) ∧ 𝑥 ∈ dom (iEdg‘𝐺)) →
(#‘((iEdg‘𝐺)‘𝑥)) ≤ 2) |
43 | 37, 40, 41, 42 | syl3anc 1318 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ dom (iEdg‘𝐺) ∧ 𝐺 ∈ UPGraph ) →
(#‘((iEdg‘𝐺)‘𝑥)) ≤ 2) |
44 | 43 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ UPGraph → (𝑥 ∈ dom (iEdg‘𝐺) →
(#‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) |
45 | 44 | ad2antll 761 |
. . . . . . . . . . . 12
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → (𝑥 ∈ dom (iEdg‘𝐺) →
(#‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) |
46 | 36, 45 | syld 46 |
. . . . . . . . . . 11
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → (𝑥 ∈ dom (iEdg‘𝑆) →
(#‘((iEdg‘𝐺)‘𝑥)) ≤ 2)) |
47 | 46 | imp 444 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (#‘((iEdg‘𝐺)‘𝑥)) ≤ 2) |
48 | 32, 47 | eqbrtrd 4605 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → (#‘((iEdg‘𝑆)‘𝑥)) ≤ 2) |
49 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑒 = ((iEdg‘𝑆)‘𝑥) → (#‘𝑒) = (#‘((iEdg‘𝑆)‘𝑥))) |
50 | 49 | breq1d 4593 |
. . . . . . . . . 10
⊢ (𝑒 = ((iEdg‘𝑆)‘𝑥) → ((#‘𝑒) ≤ 2 ↔ (#‘((iEdg‘𝑆)‘𝑥)) ≤ 2)) |
51 | 50 | elrab 3331 |
. . . . . . . . 9
⊢
(((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤ 2} ↔
(((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∧
(#‘((iEdg‘𝑆)‘𝑥)) ≤ 2)) |
52 | 23, 48, 51 | sylanbrc 695 |
. . . . . . . 8
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤
2}) |
53 | 52 | ralrimiva 2949 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤
2}) |
54 | | fnfvrnss 6297 |
. . . . . . 7
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤ 2}) →
ran (iEdg‘𝑆) ⊆
{𝑒 ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}) ∣ (#‘𝑒) ≤ 2}) |
55 | 13, 53, 54 | syl2anc 691 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}) ∣ (#‘𝑒) ≤ 2}) |
56 | | df-f 5808 |
. . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤ 2} ↔
((iEdg‘𝑆) Fn dom
(iEdg‘𝑆) ∧ ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ (𝒫
(Vtx‘𝑆) ∖
{∅}) ∣ (#‘𝑒) ≤ 2})) |
57 | 13, 55, 56 | sylanbrc 695 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤
2}) |
58 | | subgrv 40494 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
59 | 1, 3 | isupgr 25751 |
. . . . . . . . 9
⊢ (𝑆 ∈ V → (𝑆 ∈ UPGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤
2})) |
60 | 59 | adantr 480 |
. . . . . . . 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 480 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph ) → (𝑆 ∈ UPGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤
2})) |
63 | 62 | adantl 481 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → (𝑆 ∈ UPGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ (𝒫 (Vtx‘𝑆) ∖ {∅}) ∣
(#‘𝑒) ≤
2})) |
64 | 57, 63 | mpbird 246 |
. . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph )) → 𝑆 ∈ UPGraph ) |
65 | 64 | ex 449 |
. . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph ) → 𝑆 ∈ UPGraph )) |
66 | 6, 65 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UPGraph ) → 𝑆 ∈ UPGraph )) |
67 | 66 | anabsi8 857 |
1
⊢ ((𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UPGraph ) |