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 ( ( 𝐺 ∈ UPGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ UPGraph )

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