Metamath Proof Explorer

Theorem subusgr

Description: A subgraph of a simple graph is a simple graph. (Contributed by AV, 16-Nov-2020) (Proof shortened by AV, 27-Nov-2020)

Ref Expression
Assertion subusgr ( ( 𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ USGraph )

Proof

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 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
8 subgruhgrfun ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺 ) → Fun ( iEdg ‘ 𝑆 ) )
9 7 8 sylan ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺 ) → Fun ( iEdg ‘ 𝑆 ) )
10 9 ancoms ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → Fun ( iEdg ‘ 𝑆 ) )
11 10 funfnd ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → ( iEdg ‘ 𝑆 ) Fn dom ( iEdg ‘ 𝑆 ) )
12 11 adantl ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → ( iEdg ‘ 𝑆 ) Fn dom ( iEdg ‘ 𝑆 ) )
13 simplrl ⊢ ( ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑆 SubGraph 𝐺 )
14 usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
15 14 adantl ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → 𝐺 ∈ UMGraph )
16 15 adantl ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → 𝐺 ∈ UMGraph )
17 16 adantr ⊢ ( ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝐺 ∈ UMGraph )
18 simpr ⊢ ( ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) )
19 1 3 subumgredg2 ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ UMGraph ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
20 13 17 18 19 syl3anc ⊢ ( ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
21 20 ralrimiva ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
22 fnfvrnss ⊢ ( ( ( iEdg ‘ 𝑆 ) Fn dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) → ran ( iEdg ‘ 𝑆 ) ⊆ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
23 12 21 22 syl2anc ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → ran ( iEdg ‘ 𝑆 ) ⊆ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
24 df-f ⊢ ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( ( iEdg ‘ 𝑆 ) Fn dom ( iEdg ‘ 𝑆 ) ∧ ran ( iEdg ‘ 𝑆 ) ⊆ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
25 12 23 24 sylanbrc ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
26 simp2 ⊢ ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) → ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) )
27 2 4 usgrfs ⊢ ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑦 ) = 2 } )
28 df-f1 ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑦 ) = 2 } ↔ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑦 ) = 2 } ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ) )
29 ffun ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑦 ) = 2 } → Fun ( iEdg ‘ 𝐺 ) )
30 29 anim1i ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ { 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑦 ) = 2 } ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ) → ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ) )
31 28 30 sylbi ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑦 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑦 ) = 2 } → ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ) )
32 27 31 syl ⊢ ( 𝐺 ∈ USGraph → ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ) )
33 32 adantl ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ) )
34 26 33 anim12ci ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → ( ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) )
35 df-3an ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) ↔ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) )
36 34 35 sylibr ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) )
37 f1ssf1 ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ Fun ◡ ( iEdg ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ) → Fun ◡ ( iEdg ‘ 𝑆 ) )
38 36 37 syl ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → Fun ◡ ( iEdg ‘ 𝑆 ) )
39 df-f1 ⊢ ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ( ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) ⟶ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ∧ Fun ◡ ( iEdg ‘ 𝑆 ) ) )
40 25 38 39 sylanbrc ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } )
41 subgrv ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) )
42 1 3 isusgrs ⊢ ( 𝑆 ∈ V → ( 𝑆 ∈ USGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
43 42 adantr ⊢ ( ( 𝑆 ∈ V ∧ 𝐺 ∈ V ) → ( 𝑆 ∈ USGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
44 41 43 syl ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑆 ∈ USGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
45 44 adantr ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → ( 𝑆 ∈ USGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
46 45 adantl ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → ( 𝑆 ∈ USGraph ↔ ( iEdg ‘ 𝑆 ) : dom ( iEdg ‘ 𝑆 ) –1-1→ { 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
47 40 46 mpbird ⊢ ( ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) ∧ ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) ) → 𝑆 ∈ USGraph )
48 47 ex ⊢ ( ( ( Vtx ‘ 𝑆 ) ⊆ ( Vtx ‘ 𝐺 ) ∧ ( iEdg ‘ 𝑆 ) ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 ( Vtx ‘ 𝑆 ) ) → ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → 𝑆 ∈ USGraph ) )
49 6 48 syl ⊢ ( 𝑆 SubGraph 𝐺 → ( ( 𝑆 SubGraph 𝐺 ∧ 𝐺 ∈ USGraph ) → 𝑆 ∈ USGraph ) )
50 49 anabsi8 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ USGraph )