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 | | usgruhgr 40413 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UHGraph
) |
8 | | subgruhgrfun 40506 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
9 | 7, 8 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
10 | 9 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → Fun
(iEdg‘𝑆)) |
11 | | funfn 5833 |
. . . . . . . . 9
⊢ (Fun
(iEdg‘𝑆) ↔
(iEdg‘𝑆) Fn dom
(iEdg‘𝑆)) |
12 | 10, 11 | sylib 207 |
. . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
13 | 12 | adantl 481 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
14 | | simplrl 796 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) |
15 | | usgrumgr 40409 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → 𝐺 ∈ UMGraph
) |
16 | 15 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → 𝐺 ∈ UMGraph ) |
17 | 16 | adantl 481 |
. . . . . . . . . . 11
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → 𝐺 ∈ UMGraph ) |
18 | 17 | adantr 480 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UMGraph ) |
19 | | simpr 476 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) |
20 | 1, 3 | subumgredg2 40509 |
. . . . . . . . . 10
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
21 | 14, 18, 19, 20 | syl3anc 1318 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
22 | 21 | ralrimiva 2949 |
. . . . . . . 8
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
23 | | fnfvrnss 6297 |
. . . . . . . 8
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ 𝒫
(Vtx‘𝑆) ∣
(#‘𝑒) =
2}) |
24 | 13, 22, 23 | syl2anc 691 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ 𝒫
(Vtx‘𝑆) ∣
(#‘𝑒) =
2}) |
25 | | df-f 5808 |
. . . . . . 7
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2} ↔ ((iEdg‘𝑆) Fn dom (iEdg‘𝑆) ∧ ran (iEdg‘𝑆) ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
26 | 13, 24, 25 | sylanbrc 695 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
27 | | simp2 1055 |
. . . . . . . . 9
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ (iEdg‘𝑆)
⊆ (iEdg‘𝐺)) |
28 | 2, 4 | usgrfs 40387 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑦) = 2}) |
29 | | df-f1 5809 |
. . . . . . . . . . . 12
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑦) = 2} ↔ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑦) = 2} ∧ Fun ◡(iEdg‘𝐺))) |
30 | | ffun 5961 |
. . . . . . . . . . . . 13
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑦) = 2} → Fun
(iEdg‘𝐺)) |
31 | 30 | anim1i 590 |
. . . . . . . . . . . 12
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑦) = 2} ∧ Fun ◡(iEdg‘𝐺)) → (Fun (iEdg‘𝐺) ∧ Fun ◡(iEdg‘𝐺))) |
32 | 29, 31 | sylbi 206 |
. . . . . . . . . . 11
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (#‘𝑦) = 2} → (Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺))) |
33 | 28, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → (Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺))) |
34 | 33 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → (Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺))) |
35 | 27, 34 | anim12ci 589 |
. . . . . . . 8
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → ((Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺)) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) |
36 | | df-3an 1033 |
. . . . . . . 8
⊢ ((Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺)) ↔ ((Fun (iEdg‘𝐺) ∧ Fun ◡(iEdg‘𝐺)) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) |
37 | 35, 36 | sylibr 223 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → (Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) |
38 | | f1ssf1 40328 |
. . . . . . 7
⊢ ((Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺)) → Fun ◡(iEdg‘𝑆)) |
39 | 37, 38 | syl 17 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → Fun ◡(iEdg‘𝑆)) |
40 | | df-f1 5809 |
. . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2} ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2} ∧ Fun ◡(iEdg‘𝑆))) |
41 | 26, 39, 40 | sylanbrc 695 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → (iEdg‘𝑆):dom (iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2}) |
42 | | subgrv 40494 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
43 | 1, 3 | isusgrs 40386 |
. . . . . . . . 9
⊢ (𝑆 ∈ V → (𝑆 ∈ USGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
44 | 43 | adantr 480 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ∈ USGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
45 | 42, 44 | syl 17 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ USGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
46 | 45 | adantr 480 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → (𝑆 ∈ USGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
47 | 46 | adantl 481 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → (𝑆 ∈ USGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (#‘𝑒) = 2})) |
48 | 41, 47 | mpbird 246 |
. . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph )) → 𝑆 ∈ USGraph ) |
49 | 48 | ex 449 |
. . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → 𝑆 ∈ USGraph )) |
50 | 6, 49 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → 𝑆 ∈ USGraph )) |
51 | 50 | anabsi8 857 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ USGraph ) |