| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝑆) =
(Vtx‘𝑆) |
| 2 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
| 3 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
| 4 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
| 5 | | eqid 2737 |
. . . 4
⊢
(Edg‘𝑆) =
(Edg‘𝑆) |
| 6 | 1, 2, 3, 4, 5 | subgrprop2 29291 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → ((Vtx‘𝑆) ⊆ (Vtx‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺) ∧ (Edg‘𝑆) ⊆ 𝒫 (Vtx‘𝑆))) |
| 7 | | usgruhgr 29203 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UHGraph) |
| 8 | | subgruhgrfun 29299 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
| 9 | 7, 8 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺) → Fun (iEdg‘𝑆)) |
| 10 | 9 | ancoms 458 |
. . . . . . . . 9
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph) → Fun
(iEdg‘𝑆)) |
| 11 | 10 | funfnd 6597 |
. . . . . . . 8
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
| 12 | 11 | adantl 481 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → (iEdg‘𝑆) Fn dom (iEdg‘𝑆)) |
| 13 | | simplrl 777 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑆 SubGraph 𝐺) |
| 14 | | usgrumgr 29198 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ USGraph → 𝐺 ∈
UMGraph) |
| 15 | 14 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph) → 𝐺 ∈ UMGraph) |
| 16 | 15 | adantl 481 |
. . . . . . . . . . 11
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → 𝐺 ∈ UMGraph) |
| 17 | 16 | adantr 480 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝐺 ∈ UMGraph) |
| 18 | | simpr 484 |
. . . . . . . . . 10
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → 𝑥 ∈ dom (iEdg‘𝑆)) |
| 19 | 1, 3 | subumgredg2 29302 |
. . . . . . . . . 10
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
| 20 | 13, 17, 18, 19 | syl3anc 1373 |
. . . . . . . . 9
⊢
(((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) ∧ 𝑥 ∈ dom (iEdg‘𝑆)) → ((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
| 21 | 20 | ralrimiva 3146 |
. . . . . . . 8
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → ∀𝑥 ∈ dom (iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
| 22 | | fnfvrnss 7141 |
. . . . . . . 8
⊢
(((iEdg‘𝑆) Fn
dom (iEdg‘𝑆) ∧
∀𝑥 ∈ dom
(iEdg‘𝑆)((iEdg‘𝑆)‘𝑥) ∈ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ 𝒫
(Vtx‘𝑆) ∣
(♯‘𝑒) =
2}) |
| 23 | 12, 21, 22 | syl2anc 584 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → ran
(iEdg‘𝑆) ⊆
{𝑒 ∈ 𝒫
(Vtx‘𝑆) ∣
(♯‘𝑒) =
2}) |
| 24 | | df-f 6565 |
. . . . . . 7
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2} ↔ ((iEdg‘𝑆) Fn dom (iEdg‘𝑆) ∧ ran (iEdg‘𝑆) ⊆ {𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
| 25 | 12, 23, 24 | sylanbrc 583 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → (iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
| 26 | | simp2 1138 |
. . . . . . . . 9
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ (iEdg‘𝑆)
⊆ (iEdg‘𝐺)) |
| 27 | 2, 4 | usgrfs 29174 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ USGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑦) = 2}) |
| 28 | | df-f1 6566 |
. . . . . . . . . . . 12
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑦) = 2} ↔ ((iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑦) = 2} ∧ Fun ◡(iEdg‘𝐺))) |
| 29 | | ffun 6739 |
. . . . . . . . . . . . 13
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑦) = 2} → Fun
(iEdg‘𝐺)) |
| 30 | 29 | anim1i 615 |
. . . . . . . . . . . 12
⊢
(((iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑦) = 2} ∧ Fun ◡(iEdg‘𝐺)) → (Fun (iEdg‘𝐺) ∧ Fun ◡(iEdg‘𝐺))) |
| 31 | 28, 30 | sylbi 217 |
. . . . . . . . . . 11
⊢
((iEdg‘𝐺):dom
(iEdg‘𝐺)–1-1→{𝑦 ∈ 𝒫 (Vtx‘𝐺) ∣ (♯‘𝑦) = 2} → (Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺))) |
| 32 | 27, 31 | syl 17 |
. . . . . . . . . 10
⊢ (𝐺 ∈ USGraph → (Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺))) |
| 33 | 32 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph) → (Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺))) |
| 34 | 26, 33 | anim12ci 614 |
. . . . . . . 8
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → ((Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺)) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) |
| 35 | | df-3an 1089 |
. . . . . . . 8
⊢ ((Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺)) ↔ ((Fun (iEdg‘𝐺) ∧ Fun ◡(iEdg‘𝐺)) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) |
| 36 | 34, 35 | sylibr 234 |
. . . . . . 7
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → (Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) |
| 37 | | f1ssf1 6880 |
. . . . . . 7
⊢ ((Fun
(iEdg‘𝐺) ∧ Fun
◡(iEdg‘𝐺) ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺)) → Fun ◡(iEdg‘𝑆)) |
| 38 | 36, 37 | syl 17 |
. . . . . 6
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → Fun ◡(iEdg‘𝑆)) |
| 39 | | df-f1 6566 |
. . . . . 6
⊢
((iEdg‘𝑆):dom
(iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2} ↔ ((iEdg‘𝑆):dom (iEdg‘𝑆)⟶{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2} ∧ Fun ◡(iEdg‘𝑆))) |
| 40 | 25, 38, 39 | sylanbrc 583 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → (iEdg‘𝑆):dom (iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2}) |
| 41 | | subgrv 29287 |
. . . . . . . 8
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
| 42 | 1, 3 | isusgrs 29173 |
. . . . . . . . 9
⊢ (𝑆 ∈ V → (𝑆 ∈ USGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
| 43 | 42 | adantr 480 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝑆 ∈ USGraph ↔
(iEdg‘𝑆):dom
(iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
| 44 | 41, 43 | syl 17 |
. . . . . . 7
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ USGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
| 45 | 44 | adantr 480 |
. . . . . 6
⊢ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph) → (𝑆 ∈ USGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
| 46 | 45 | adantl 481 |
. . . . 5
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → (𝑆 ∈ USGraph ↔ (iEdg‘𝑆):dom (iEdg‘𝑆)–1-1→{𝑒 ∈ 𝒫 (Vtx‘𝑆) ∣ (♯‘𝑒) = 2})) |
| 47 | 40, 46 | mpbird 257 |
. . . 4
⊢
((((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
∧ (𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph)) → 𝑆 ∈ USGraph) |
| 48 | 47 | ex 412 |
. . 3
⊢
(((Vtx‘𝑆)
⊆ (Vtx‘𝐺) ∧
(iEdg‘𝑆) ⊆
(iEdg‘𝐺) ∧
(Edg‘𝑆) ⊆
𝒫 (Vtx‘𝑆))
→ ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph) → 𝑆 ∈ USGraph)) |
| 49 | 6, 48 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → ((𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph) → 𝑆 ∈ USGraph)) |
| 50 | 49 | anabsi8 672 |
1
⊢ ((𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺) → 𝑆 ∈ USGraph) |