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 \in USGraph \land S SubGraph G) \to S \in 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 \to (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S))$
7		usgruhgr	$⊢ G \in USGraph \to G \in UHGraph$
8		subgruhgrfun	$⊢ (G \in UHGraph \land S SubGraph G) \to Fun iEdg (S)$
9	7 8	sylan	$⊢ (G \in USGraph \land S SubGraph G) \to Fun iEdg (S)$
10	9	ancoms	$⊢ (S SubGraph G \land G \in USGraph) \to Fun iEdg (S)$
11	10	funfnd	$⊢ (S SubGraph G \land G \in USGraph) \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 USGraph)) \to iEdg (S) Fn dom iEdg (S)$
13		simplrl	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in USGraph)) \land x \in dom iEdg (S)) \to S SubGraph G$
14		usgrumgr	$⊢ G \in USGraph \to G \in UMGraph$
15	14	adantl	$⊢ (S SubGraph G \land G \in USGraph) \to G \in UMGraph$
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 USGraph)) \to G \in UMGraph$
17	16	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 USGraph)) \land x \in dom iEdg (S)) \to G \in UMGraph$
18		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 USGraph)) \land x \in dom iEdg (S)) \to x \in dom iEdg (S)$
19	1 3	subumgredg2	$⊢ (S SubGraph G \land G \in UMGraph \land x \in dom iEdg (S)) \to iEdg (S) (x) \in \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
20	13 17 18 19	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 USGraph)) \land x \in dom iEdg (S)) \to iEdg (S) (x) \in \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
21	20	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 USGraph)) \to \forall x \in dom iEdg (S) iEdg (S) (x) \in \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
22		fnfvrnss	$⊢ (iEdg (S) Fn dom iEdg (S) \land \forall x \in dom iEdg (S) iEdg (S) (x) \in \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}) \to ran iEdg (S) \subseteq \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
23	12 21 22	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 USGraph)) \to ran iEdg (S) \subseteq \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
24		df-f	$⊢ iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\} \leftrightarrow (iEdg (S) Fn dom iEdg (S) \land ran iEdg (S) \subseteq \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
25	12 23 24	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 USGraph)) \to iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
26		simp2	$⊢ (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \to iEdg (S) \subseteq iEdg (G)$
27	2 4	usgrfs	$⊢ G \in USGraph \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{y \in 𝒫 Vtx (G) \| \|y\| = 2\}$
28		df-f1	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{y \in 𝒫 Vtx (G) \| \|y\| = 2\} \leftrightarrow (iEdg (G) : dom iEdg (G) ⟶ \{y \in 𝒫 Vtx (G) \| \|y\| = 2\} \land Fun {iEdg (G)}^{-1})$
29		ffun	$⊢ iEdg (G) : dom iEdg (G) ⟶ \{y \in 𝒫 Vtx (G) \| \|y\| = 2\} \to Fun iEdg (G)$
30	29	anim1i	$⊢ (iEdg (G) : dom iEdg (G) ⟶ \{y \in 𝒫 Vtx (G) \| \|y\| = 2\} \land Fun {iEdg (G)}^{-1}) \to (Fun iEdg (G) \land Fun {iEdg (G)}^{-1})$
31	28 30	sylbi	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{y \in 𝒫 Vtx (G) \| \|y\| = 2\} \to (Fun iEdg (G) \land Fun {iEdg (G)}^{-1})$
32	27 31	syl	$⊢ G \in USGraph \to (Fun iEdg (G) \land Fun {iEdg (G)}^{-1})$
33	32	adantl	$⊢ (S SubGraph G \land G \in USGraph) \to (Fun iEdg (G) \land Fun {iEdg (G)}^{-1})$
34	26 33	anim12ci	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in USGraph)) \to ((Fun iEdg (G) \land Fun {iEdg (G)}^{-1}) \land iEdg (S) \subseteq iEdg (G))$
35		df-3an	$⊢ (Fun iEdg (G) \land Fun {iEdg (G)}^{-1} \land iEdg (S) \subseteq iEdg (G)) \leftrightarrow ((Fun iEdg (G) \land Fun {iEdg (G)}^{-1}) \land iEdg (S) \subseteq iEdg (G))$
36	34 35	sylibr	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in USGraph)) \to (Fun iEdg (G) \land Fun {iEdg (G)}^{-1} \land iEdg (S) \subseteq iEdg (G))$
37		f1ssf1	$⊢ (Fun iEdg (G) \land Fun {iEdg (G)}^{-1} \land iEdg (S) \subseteq iEdg (G)) \to Fun {iEdg (S)}^{-1}$
38	36 37	syl	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in USGraph)) \to Fun {iEdg (S)}^{-1}$
39		df-f1	$⊢ iEdg (S) : dom iEdg (S) \underset{1-1}{⟶} \{e \in 𝒫 Vtx (S) \| \|e\| = 2\} \leftrightarrow (iEdg (S) : dom iEdg (S) ⟶ \{e \in 𝒫 Vtx (S) \| \|e\| = 2\} \land Fun {iEdg (S)}^{-1})$
40	25 38 39	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 USGraph)) \to iEdg (S) : dom iEdg (S) \underset{1-1}{⟶} \{e \in 𝒫 Vtx (S) \| \|e\| = 2\}$
41		subgrv	$⊢ S SubGraph G \to (S \in V \land G \in V)$
42	1 3	isusgrs	$⊢ S \in V \to (S \in USGraph \leftrightarrow iEdg (S) : dom iEdg (S) \underset{1-1}{⟶} \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
43	42	adantr	$⊢ (S \in V \land G \in V) \to (S \in USGraph \leftrightarrow iEdg (S) : dom iEdg (S) \underset{1-1}{⟶} \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
44	41 43	syl	$⊢ S SubGraph G \to (S \in USGraph \leftrightarrow iEdg (S) : dom iEdg (S) \underset{1-1}{⟶} \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
45	44	adantr	$⊢ (S SubGraph G \land G \in USGraph) \to (S \in USGraph \leftrightarrow iEdg (S) : dom iEdg (S) \underset{1-1}{⟶} \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
46	45	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 USGraph)) \to (S \in USGraph \leftrightarrow iEdg (S) : dom iEdg (S) \underset{1-1}{⟶} \{e \in 𝒫 Vtx (S) \| \|e\| = 2\})$
47	40 46	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 USGraph)) \to S \in USGraph$
48	47	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 USGraph) \to S \in USGraph)$
49	6 48	syl	$⊢ S SubGraph G \to ((S SubGraph G \land G \in USGraph) \to S \in USGraph)$
50	49	anabsi8	$⊢ (G \in USGraph \land S SubGraph G) \to S \in USGraph$

Metamath Proof Explorer

Theorem subusgr

Proof