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

Metamath Proof Explorer

Theorem subupgr

Proof