Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
2 | | eqid 2622 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
3 | | eqid 2622 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
4 | | eqid 2622 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
5 | | eqid 2622 |
. . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
6 | 1, 2, 3, 4, 5 | subgrprop2 26166 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))) |
7 | | subgruhgrfun 26174 |
. . . . . . . . 9
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
8 | 7 | ancoms 469 |
. . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph ) → Fun
(iEdg‘𝑆)) |
9 | 8 | adantl 482 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) → Fun
(iEdg‘𝑆)) |
10 | | funfn 5918 |
. . . . . . 7
⊢ (Fun
(iEdg‘𝑆) ↔
(iEdg‘𝑆) Fn dom
(iEdg‘𝑆)) |
11 | 9, 10 | sylib 208 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
12 | | simplrr 801 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UHGraph ) |
13 | | simplrl 800 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) |
14 | | simpr 477 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) |
15 | 1, 3, 12, 13, 14 | subgruhgredgd 26176 |
. . . . . . . 8
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖
{∅})) |
16 | 15 | ralrimiva 2966 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖
{∅})) |
17 | | fnfvrnss 6390 |
. . . . . . 7
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ (𝒫 (Vtx‘𝑆) ∖ {∅})) → ran
(iEdg‘𝑆) ⊆
(𝒫 (Vtx‘𝑆)
∖ {∅})) |
18 | 11, 16, 17 | syl2anc 693 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) → ran
(iEdg‘𝑆) ⊆
(𝒫 (Vtx‘𝑆)
∖ {∅})) |
19 | | df-f 5892 |
. . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖ {∅}) ↔
((iEdg‘𝑆) Fn dom
(iEdg‘𝑆) ∧ ran
(iEdg‘𝑆) ⊆
(𝒫 (Vtx‘𝑆)
∖ {∅}))) |
20 | 11, 18, 19 | sylanbrc 698 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅})) |
21 | | subgrv 26162 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
22 | 1, 3 | isuhgr 25955 |
. . . . . . . . 9
⊢ (𝑆 ∈ V → (𝑆 ∈ UHGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖
{∅}))) |
23 | 22 | adantr 481 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ∈ UHGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)⟶(𝒫 (Vtx‘𝑆) ∖
{∅}))) |
24 | 21, 23 | syl 17 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}))) |
25 | 24 | adantr 481 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph ) → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}))) |
26 | 25 | adantl 482 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) → (𝑆 ∈ UHGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)⟶(𝒫
(Vtx‘𝑆) ∖
{∅}))) |
27 | 20, 26 | mpbird 247 |
. . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph )) → 𝑆 ∈ UHGraph ) |
28 | 27 | ex 450 |
. . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph ) → 𝑆 ∈ UHGraph )) |
29 | 6, 28 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UHGraph ) → 𝑆 ∈ UHGraph )) |
30 | 29 | anabsi8 861 |
1
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ UHGraph ) |