Metamath Proof Explorer

Theorem subupgr

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

Ref Expression
Assertion subupgr ⊢ G ∈ UPGraph ∧ S SubGraph G → S ∈ UPGraph

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 upgruhgr ⊢ G ∈ UPGraph → G ∈ UHGraph
8 subgruhgrfun ⊢ G ∈ UHGraph ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S
9 7 8 sylan ⊢ G ∈ UPGraph ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S
10 9 ancoms ⊢ S SubGraph G ∧ G ∈ UPGraph → Fun ⁡ iEdg ⁡ S
11 10 funfnd ⊢ S SubGraph G ∧ G ∈ UPGraph → 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 ∈ UPGraph → iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S
13 fveq2 ⊢ e = iEdg ⁡ S ⁡ x → e = iEdg ⁡ S ⁡ x
14 13 breq1d ⊢ e = iEdg ⁡ S ⁡ x → e ≤ 2 ↔ iEdg ⁡ S ⁡ x ≤ 2
15 7 anim2i ⊢ S SubGraph G ∧ G ∈ UPGraph → S SubGraph G ∧ G ∈ UHGraph
16 15 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → S SubGraph G ∧ G ∈ UHGraph
17 16 ancomd ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → G ∈ UHGraph ∧ S SubGraph G
18 17 anim1i ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → G ∈ UHGraph ∧ S SubGraph G ∧ x ∈ dom ⁡ iEdg ⁡ S
19 18 simplld ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → G ∈ UHGraph
20 simpl ⊢ S SubGraph G ∧ G ∈ UPGraph → S SubGraph G
21 20 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → S SubGraph G
22 21 adantr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → S SubGraph G
23 simpr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → x ∈ dom ⁡ iEdg ⁡ S
24 1 3 19 22 23 subgruhgredgd ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x ∈ 𝒫 Vtx ⁡ S ∖ ∅
25 4 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ iEdg ⁡ G
26 7 25 syl ⊢ G ∈ UPGraph → Fun ⁡ iEdg ⁡ G
27 26 ad2antll ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → Fun ⁡ iEdg ⁡ G
28 27 adantr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → Fun ⁡ iEdg ⁡ G
29 simpll2 ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⊆ iEdg ⁡ G
30 funssfv ⊢ Fun ⁡ iEdg ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ G ⁡ x = iEdg ⁡ S ⁡ x
31 28 29 23 30 syl3anc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ G ⁡ x = iEdg ⁡ S ⁡ x
32 31 eqcomd ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x = iEdg ⁡ G ⁡ x
33 32 fveq2d ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x = iEdg ⁡ G ⁡ x
34 subgreldmiedg ⊢ S SubGraph G ∧ x ∈ dom ⁡ iEdg ⁡ S → x ∈ dom ⁡ iEdg ⁡ G
35 34 ex ⊢ S SubGraph G → x ∈ dom ⁡ iEdg ⁡ S → x ∈ dom ⁡ iEdg ⁡ G
36 35 adantr ⊢ S SubGraph G ∧ G ∈ UPGraph → x ∈ dom ⁡ iEdg ⁡ S → x ∈ dom ⁡ iEdg ⁡ G
37 36 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → x ∈ dom ⁡ iEdg ⁡ S → x ∈ dom ⁡ iEdg ⁡ G
38 simpr ⊢ x ∈ dom ⁡ iEdg ⁡ G ∧ G ∈ UPGraph → G ∈ UPGraph
39 26 funfnd ⊢ G ∈ UPGraph → iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G
40 39 adantl ⊢ x ∈ dom ⁡ iEdg ⁡ G ∧ G ∈ UPGraph → iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G
41 simpl ⊢ x ∈ dom ⁡ iEdg ⁡ G ∧ G ∈ UPGraph → x ∈ dom ⁡ iEdg ⁡ G
42 2 4 upgrle ⊢ G ∈ UPGraph ∧ iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G ∧ x ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ G ⁡ x ≤ 2
43 38 40 41 42 syl3anc ⊢ x ∈ dom ⁡ iEdg ⁡ G ∧ G ∈ UPGraph → iEdg ⁡ G ⁡ x ≤ 2
44 43 expcom ⊢ G ∈ UPGraph → x ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ G ⁡ x ≤ 2
45 44 ad2antll ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → x ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ G ⁡ x ≤ 2
46 37 45 syld ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ G ⁡ x ≤ 2
47 46 imp ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ G ⁡ x ≤ 2
48 33 47 eqbrtrd ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x ≤ 2
49 14 24 48 elrabd ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
50 49 ralrimiva ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → ∀ x ∈ dom ⁡ iEdg ⁡ S iEdg ⁡ S ⁡ x ∈ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
51 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
52 12 50 51 syl2anc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → ran ⁡ iEdg ⁡ S ⊆ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
53 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
54 12 52 53 sylanbrc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
55 subgrv ⊢ S SubGraph G → S ∈ V ∧ G ∈ V
56 1 3 isupgr ⊢ S ∈ V → S ∈ UPGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
57 56 adantr ⊢ S ∈ V ∧ G ∈ V → S ∈ UPGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
58 55 57 syl ⊢ S SubGraph G → S ∈ UPGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
59 58 adantr ⊢ S SubGraph G ∧ G ∈ UPGraph → S ∈ UPGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
60 59 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → S ∈ UPGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ e ∈ 𝒫 Vtx ⁡ S ∖ ∅ | e ≤ 2
61 54 60 mpbird ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UPGraph → S ∈ UPGraph
62 61 ex ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S → S SubGraph G ∧ G ∈ UPGraph → S ∈ UPGraph
63 6 62 syl ⊢ S SubGraph G → S SubGraph G ∧ G ∈ UPGraph → S ∈ UPGraph
64 63 anabsi8 ⊢ G ∈ UPGraph ∧ S SubGraph G → S ∈ UPGraph