| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eqid |
⊢ ( Vtx ‘ 𝑆 ) = ( Vtx ‘ 𝑆 ) |
| 2 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
| 3 |
|
eqid |
⊢ ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 ) |
| 4 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
| 5 |
|
eqid |
⊢ ( Edg ‘ 𝑆 ) = ( Edg ‘ 𝑆 ) |
| 6 |
1 2 3 4 5
|
subgrprop2 |
⊢ ( 𝑆 SubGraph 𝐺 → ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ) |
| 7 |
|
umgruhgr |
⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UHGraph ) |
| 8 |
|
subgruhgrfun |
⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺 ) → Fun ( iEdg ‘ 𝑆 ) ) |
| 9 |
7 8
|
sylan |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺 ) → Fun ( iEdg ‘ 𝑆 ) ) |
| 10 |
9
|
ancoms |
⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) → Fun ( iEdg ‘ 𝑆 ) ) |
| 11 |
10
|
funfnd |
⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) → ( iEdg ‘ 𝑆 ) Fn dom ( iEdg ‘ 𝑆 ) ) |
| 12 |
11
|
adantl |
⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) → ( iEdg ‘ 𝑆 ) Fn dom ( iEdg ‘ 𝑆 ) ) |
| 13 |
|
simplrl |
⊢ ( ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑆 SubGraph 𝐺 ) |
| 14 |
|
simplrr |
⊢ ( ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝐺 ∈ UMGraph ) |
| 15 |
|
simpr |
⊢ ( ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) |
| 16 |
1 3
|
subumgredg2 |
⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) |
| 17 |
13 14 15 16
|
syl3anc |
⊢ ( ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) |
| 18 |
17
|
ralrimiva |
⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) |
| 19 |
|
fnfvrnss |
⊢ ( ( ( iEdg ‘ 𝑆 ) Fn dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) → ran ( iEdg ‘ 𝑆 ) ⊆ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) |
| 20 |
12 18 19
|
syl2anc |
⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) → ran ( iEdg ‘ 𝑆 ) ⊆ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) |
| 21 |
|
df-f |
⊢ ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( ( iEdg ‘ 𝑆 ) Fn dom ( iEdg ‘ 𝑆 ) ∧ ran ( iEdg ‘ 𝑆 ) ⊆ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) ) |
| 22 |
12 20 21
|
sylanbrc |
⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) → ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) |
| 23 |
|
subgrv |
⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) ) |
| 24 |
1 3
|
isumgrs |
⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ UMGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) ) |
| 25 |
24
|
adantr |
⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( 𝑆 ∈ UMGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) ) |
| 26 |
23 25
|
syl |
⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ UMGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) ) |
| 27 |
26
|
ad2antrl |
⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) → ( 𝑆 ∈ UMGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) ) |
| 28 |
22 27
|
mpbird |
⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) ) → 𝑆 ∈ UMGraph ) |
| 29 |
28
|
ex |
⊢ ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) → ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) → 𝑆 ∈ UMGraph ) ) |
| 30 |
6 29
|
syl |
⊢ ( 𝑆 SubGraph 𝐺 → ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ) → 𝑆 ∈ UMGraph ) ) |
| 31 |
30
|
anabsi8 |
⊢ ( ( 𝐺 ∈ UMGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ UMGraph ) |