Proof of Theorem subgrprop3
Step | Hyp | Ref
| Expression |
1 | | subgrprop3.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝑆) |
2 | | subgrprop3.a |
. . . 4
⊢ 𝐴 = (Vtx‘𝐺) |
3 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝑆) =
(iEdg‘𝑆) |
4 | | eqid 2610 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
5 | | subgrprop3.e |
. . . 4
⊢ 𝐸 = (Edg‘𝑆) |
6 | 1, 2, 3, 4, 5 | subgrprop2 40498 |
. . 3
⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺) ∧ 𝐸 ⊆ 𝒫 𝑉)) |
7 | | 3simpa 1051 |
. . 3
⊢ ((𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺) ∧ 𝐸 ⊆ 𝒫 𝑉) → (𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) |
8 | 6, 7 | syl 17 |
. 2
⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) |
9 | | simprl 790 |
. . 3
⊢ ((𝑆 SubGraph 𝐺 ∧ (𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) → 𝑉 ⊆ 𝐴) |
10 | | rnss 5275 |
. . . . . 6
⊢
((iEdg‘𝑆)
⊆ (iEdg‘𝐺)
→ ran (iEdg‘𝑆)
⊆ ran (iEdg‘𝐺)) |
11 | 10 | adantl 481 |
. . . . 5
⊢ ((𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺)) → ran (iEdg‘𝑆) ⊆ ran (iEdg‘𝐺)) |
12 | 11 | adantl 481 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ (𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) → ran (iEdg‘𝑆) ⊆ ran (iEdg‘𝐺)) |
13 | | subgrv 40494 |
. . . . . 6
⊢ (𝑆 SubGraph 𝐺 → (𝑆 ∈ V ∧ 𝐺 ∈ V)) |
14 | | edgaval 25794 |
. . . . . . . . 9
⊢ (𝑆 ∈ V →
(Edg‘𝑆) = ran
(iEdg‘𝑆)) |
15 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) →
(Edg‘𝑆) = ran
(iEdg‘𝑆)) |
16 | 5, 15 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → 𝐸 = ran (iEdg‘𝑆)) |
17 | | subgrprop3.b |
. . . . . . . 8
⊢ 𝐵 = (Edg‘𝐺) |
18 | | edgaval 25794 |
. . . . . . . . 9
⊢ (𝐺 ∈ V →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
19 | 18 | adantl 481 |
. . . . . . . 8
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) →
(Edg‘𝐺) = ran
(iEdg‘𝐺)) |
20 | 17, 19 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → 𝐵 = ran (iEdg‘𝐺)) |
21 | 16, 20 | sseq12d 3597 |
. . . . . 6
⊢ ((𝑆 ∈ V ∧ 𝐺 ∈ V) → (𝐸 ⊆ 𝐵 ↔ ran (iEdg‘𝑆) ⊆ ran (iEdg‘𝐺))) |
22 | 13, 21 | syl 17 |
. . . . 5
⊢ (𝑆 SubGraph 𝐺 → (𝐸 ⊆ 𝐵 ↔ ran (iEdg‘𝑆) ⊆ ran (iEdg‘𝐺))) |
23 | 22 | adantr 480 |
. . . 4
⊢ ((𝑆 SubGraph 𝐺 ∧ (𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) → (𝐸 ⊆ 𝐵 ↔ ran (iEdg‘𝑆) ⊆ ran (iEdg‘𝐺))) |
24 | 12, 23 | mpbird 246 |
. . 3
⊢ ((𝑆 SubGraph 𝐺 ∧ (𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) → 𝐸 ⊆ 𝐵) |
25 | 9, 24 | jca 553 |
. 2
⊢ ((𝑆 SubGraph 𝐺 ∧ (𝑉 ⊆ 𝐴 ∧ (iEdg‘𝑆) ⊆ (iEdg‘𝐺))) → (𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵)) |
26 | 8, 25 | mpdan 699 |
1
⊢ (𝑆 SubGraph 𝐺 → (𝑉 ⊆ 𝐴 ∧ 𝐸 ⊆ 𝐵)) |