Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
2 | | eqid 2738 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2738 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
4 | | eqid 2738 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
5 | | eqid 2738 |
. . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
6 | 1, 2, 3, 4, 5 | subgrprop2 27641 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))) |
7 | | umgruhgr 27474 |
. . . . . . . . . 10
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UHGraph) |
8 | | subgruhgrfun 27649 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
9 | 7, 8 | sylan 580 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
10 | 9 | ancoms 459 |
. . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph) → Fun
(iEdg‘𝑆)) |
11 | 10 | funfnd 6465 |
. . . . . . 7
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
12 | 11 | adantl 482 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
13 | | simplrl 774 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) |
14 | | simplrr 775 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UMGraph) |
15 | | simpr 485 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) |
16 | 1, 3 | subumgredg2 27652 |
. . . . . . . . 9
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
17 | 13, 14, 15, 16 | syl3anc 1370 |
. . . . . . . 8
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
18 | 17 | ralrimiva 3103 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
19 | | fnfvrnss 6994 |
. . . . . . 7
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ 𝒫
(Vtx‘𝑆) ∣
(♯‘𝑒) =
2}) |
20 | 12, 18, 19 | syl2anc 584 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ 𝒫
(Vtx‘𝑆) ∣
(♯‘𝑒) =
2}) |
21 | | df-f 6437 |
. . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2} ↔ ((iEdg‘𝑆) Fn dom (iEdg‘𝑆) ∧ ran (iEdg‘𝑆) ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
22 | 12, 20, 21 | sylanbrc 583 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
23 | | subgrv 27637 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
24 | 1, 3 | isumgrs 27466 |
. . . . . . . 8
⊢ (𝑆 ∈ V → (𝑆 ∈ UMGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
25 | 24 | adantr 481 |
. . . . . . 7
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ∈ UMGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
26 | 23, 25 | syl 17 |
. . . . . 6
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ UMGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
27 | 26 | ad2antrl 725 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) → (𝑆 ∈ UMGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
28 | 22, 27 | mpbird 256 |
. . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph)) → 𝑆 ∈ UMGraph) |
29 | 28 | ex 413 |
. . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph) → 𝑆 ∈ UMGraph)) |
30 | 6, 29 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph) → 𝑆 ∈ UMGraph)) |
31 | 30 | anabsi8 669 |
1
⊢ ((𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UMGraph) |