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 | | umgruhgr 25770 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph
) |
8 | | subgruhgrfun 40506 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
9 | 7, 8 | sylan 487 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
10 | 9 | ancoms 468 |
. . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) → Fun
(iEdg‘𝑆)) |
11 | | funfn 5833 |
. . . . . . . 8
⊢ (Fun
(iEdg‘𝑆) ↔
(iEdg‘𝑆) Fn dom
(iEdg‘𝑆)) |
12 | 10, 11 | sylib 207 |
. . . . . . 7
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
13 | 12 | adantl 481 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
14 | | simplrl 796 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) |
15 | | simplrr 797 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UMGraph ) |
16 | | simpr 476 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) |
17 | 1, 3 | subumgredg2 40509 |
. . . . . . . . 9
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
18 | 14, 15, 16, 17 | syl3anc 1318 |
. . . . . . . 8
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
19 | 18 | ralrimiva 2949 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
20 | | fnfvrnss 6297 |
. . . . . . 7
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ 𝒫
(Vtx‘𝑆) ∣
(#‘𝑒) =
2}) |
21 | 13, 19, 20 | syl2anc 691 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ 𝒫
(Vtx‘𝑆) ∣
(#‘𝑒) =
2}) |
22 | | df-f 5808 |
. . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2} ↔ ((iEdg‘𝑆) Fn dom (iEdg‘𝑆) ∧ ran (iEdg‘𝑆) ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
23 | 13, 21, 22 | sylanbrc 695 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
24 | | subgrv 40494 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
25 | 1, 3 | isumgrs 25762 |
. . . . . . . 8
⊢ (𝑆 ∈ V → (𝑆 ∈ UMGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ∈ UMGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
27 | 24, 26 | syl 17 |
. . . . . 6
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ UMGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
28 | 27 | ad2antrl 760 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) → (𝑆 ∈ UMGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
29 | 23, 28 | mpbird 246 |
. . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph )) → 𝑆 ∈ UMGraph ) |
30 | 29 | ex 449 |
. . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) → 𝑆 ∈ UMGraph )) |
31 | 6, 30 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) → 𝑆 ∈ UMGraph )) |
32 | 31 | anabsi8 857 |
1
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UMGraph ) |