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 ⊢ G ∈ USGraph ∧ S SubGraph G → S ∈ USGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ S = Vtx ⁡ S
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ iEdg ⁡ S = iEdg ⁡ S
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 eqid ⊢ Edg ⁡ S = Edg ⁡ S
6 1 2 3 4 5 subgrprop2 ⊢ S SubGraph G → Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
7 usgruhgr ⊢ G ∈ USGraph → G ∈ UHGraph
8 subgruhgrfun ⊢ G ∈ UHGraph ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S
9 7 8 sylan ⊢ G ∈ USGraph ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S
10 9 ancoms ⊢ S SubGraph G ∧ G ∈ USGraph → Fun ⁡ iEdg ⁡ S
11 10 funfnd ⊢ S SubGraph G ∧ G ∈ USGraph → iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S
12 11 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S
13 simplrl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → S SubGraph G
14 usgrumgr ⊢ G ∈ USGraph → G ∈ UMGraph
15 14 adantl ⊢ S SubGraph G ∧ G ∈ USGraph → G ∈ UMGraph
16 15 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → G ∈ UMGraph
17 16 adantr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → G ∈ UMGraph
18 simpr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → x ∈ dom ⁡ iEdg ⁡ S
19 1 3 subumgredg2 ⊢ S SubGraph G ∧ G ∈ UMGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S | e = 2
20 13 17 18 19 syl3anc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S | e = 2
21 20 ralrimiva ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → ∀ x ∈ dom ⁡ iEdg ⁡ S iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S | e = 2
22 fnfvrnss ⊢ iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S ∧ ∀ x ∈ dom ⁡ iEdg ⁡ S iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S | e = 2 → ran ⁡ iEdg ⁡ S ⊆ e ∈ 𝒫 Vtx ⁡ S | e = 2
23 12 21 22 syl2anc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → ran ⁡ iEdg ⁡ S ⊆ e ∈ 𝒫 Vtx ⁡ S | e = 2
24 df-f ⊢ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2 ↔ iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S ∧ ran ⁡ iEdg ⁡ S ⊆ e ∈ 𝒫 Vtx ⁡ S | e = 2
25 12 23 24 sylanbrc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2
26 simp2 ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S → iEdg ⁡ S ⊆ iEdg ⁡ G
27 2 4 usgrfs ⊢ G ∈ USGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 y ∈ 𝒫 Vtx ⁡ G | y = 2
28 df-f1 ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 y ∈ 𝒫 Vtx ⁡ G | y = 2 ↔ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ y ∈ 𝒫 Vtx ⁡ G | y = 2 ∧ Fun ⁡ iEdg ⁡ G -1
29 ffun ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ y ∈ 𝒫 Vtx ⁡ G | y = 2 → Fun ⁡ iEdg ⁡ G
30 29 anim1i ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ y ∈ 𝒫 Vtx ⁡ G | y = 2 ∧ Fun ⁡ iEdg ⁡ G -1 → Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1
31 28 30 sylbi ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 y ∈ 𝒫 Vtx ⁡ G | y = 2 → Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1
32 27 31 syl ⊢ G ∈ USGraph → Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1
33 32 adantl ⊢ S SubGraph G ∧ G ∈ USGraph → Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1
34 26 33 anim12ci ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1 ∧ iEdg ⁡ S ⊆ iEdg ⁡ G
35 df-3an ⊢ Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1 ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ↔ Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1 ∧ iEdg ⁡ S ⊆ iEdg ⁡ G
36 34 35 sylibr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1 ∧ iEdg ⁡ S ⊆ iEdg ⁡ G
37 f1ssf1 ⊢ Fun ⁡ iEdg ⁡ G ∧ Fun ⁡ iEdg ⁡ G -1 ∧ iEdg ⁡ S ⊆ iEdg ⁡ G → Fun ⁡ iEdg ⁡ S -1
38 36 37 syl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → Fun ⁡ iEdg ⁡ S -1
39 df-f1 ⊢ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ S | e = 2 ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S | e = 2 ∧ Fun ⁡ iEdg ⁡ S -1
40 25 38 39 sylanbrc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ S | e = 2
41 subgrv ⊢ S SubGraph G → S ∈ V ∧ G ∈ V
42 1 3 isusgrs ⊢ S ∈ V → S ∈ USGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ S | e = 2
43 42 adantr ⊢ S ∈ V ∧ G ∈ V → S ∈ USGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ S | e = 2
44 41 43 syl ⊢ S SubGraph G → S ∈ USGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ S | e = 2
45 44 adantr ⊢ S SubGraph G ∧ G ∈ USGraph → S ∈ USGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ S | e = 2
46 45 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → S ∈ USGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 1-1 e ∈ 𝒫 Vtx ⁡ S | e = 2
47 40 46 mpbird ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ USGraph → S ∈ USGraph
48 47 ex ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S → S SubGraph G ∧ G ∈ USGraph → S ∈ USGraph
49 6 48 syl ⊢ S SubGraph G → S SubGraph G ∧ G ∈ USGraph → S ∈ USGraph
50 49 anabsi8 ⊢ G ∈ USGraph ∧ S SubGraph G → S ∈ USGraph