ausgrusgrb

Description: The equivalence of the definitions of a simple graph. (Contributed by Alexander van der Vekens, 28-Aug-2017) (Revised by AV, 14-Oct-2020)

		Ref	Expression
	Hypothesis	ausgr.1	$⊢ G = \{⟨v, e⟩ \| e \subseteq \{x \in 𝒫 v \| \|x\| = 2\}\}$
	Assertion	ausgrusgrb	$⊢ (V \in X \land E \in Y) \to (V G E \leftrightarrow ⟨V, {I ↾}_{E}⟩ \in USGraph)$

Proof

Step	Hyp	Ref	Expression
1		ausgr.1	$⊢ G = \{⟨v, e⟩ \| e \subseteq \{x \in 𝒫 v \| \|x\| = 2\}\}$
2	1	isausgr	$⊢ (V \in X \land E \in Y) \to (V G E \leftrightarrow E \subseteq \{x \in 𝒫 V \| \|x\| = 2\})$
3		f1oi	$⊢ ({I ↾}_{E}) : E \underset{1-1 onto}{⟶} E$
4		dff1o5	$⊢ ({I ↾}_{E}) : E \underset{1-1 onto}{⟶} E \leftrightarrow (({I ↾}_{E}) : E \underset{1-1}{⟶} E \land ran ({I ↾}_{E}) = E)$
5		f1ss	$⊢ (({I ↾}_{E}) : E \underset{1-1}{⟶} E \land E \subseteq \{x \in 𝒫 V \| \|x\| = 2\}) \to ({I ↾}_{E}) : E \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}$
6		dmresi	$⊢ dom ({I ↾}_{E}) = E$
7	6	eqcomi	$⊢ E = dom ({I ↾}_{E})$
8		f1eq2	$⊢ E = dom ({I ↾}_{E}) \to (({I ↾}_{E}) : E \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\})$
9	7 8	ax-mp	$⊢ ({I ↾}_{E}) : E \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}$
10	5 9	sylib	$⊢ (({I ↾}_{E}) : E \underset{1-1}{⟶} E \land E \subseteq \{x \in 𝒫 V \| \|x\| = 2\}) \to ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}$
11	10	ex	$⊢ ({I ↾}_{E}) : E \underset{1-1}{⟶} E \to (E \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \to ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\})$
12	11	a1d	$⊢ ({I ↾}_{E}) : E \underset{1-1}{⟶} E \to ((V \in X \land E \in Y) \to (E \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \to ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}))$
13	12	adantr	$⊢ (({I ↾}_{E}) : E \underset{1-1}{⟶} E \land ran ({I ↾}_{E}) = E) \to ((V \in X \land E \in Y) \to (E \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \to ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}))$
14	4 13	sylbi	$⊢ ({I ↾}_{E}) : E \underset{1-1 onto}{⟶} E \to ((V \in X \land E \in Y) \to (E \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \to ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}))$
15	3 14	ax-mp	$⊢ (V \in X \land E \in Y) \to (E \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \to ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\})$
16		df-f	$⊢ ({I ↾}_{E}) : dom ({I ↾}_{E}) ⟶ \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow (({I ↾}_{E}) Fn dom ({I ↾}_{E}) \land ran ({I ↾}_{E}) \subseteq \{x \in 𝒫 V \| \|x\| = 2\})$
17		rnresi	$⊢ ran ({I ↾}_{E}) = E$
18	17	sseq1i	$⊢ ran ({I ↾}_{E}) \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow E \subseteq \{x \in 𝒫 V \| \|x\| = 2\}$
19	18	biimpi	$⊢ ran ({I ↾}_{E}) \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \to E \subseteq \{x \in 𝒫 V \| \|x\| = 2\}$
20	19	a1d	$⊢ ran ({I ↾}_{E}) \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \to ((V \in X \land E \in Y) \to E \subseteq \{x \in 𝒫 V \| \|x\| = 2\})$
21	16 20	simplbiim	$⊢ ({I ↾}_{E}) : dom ({I ↾}_{E}) ⟶ \{x \in 𝒫 V \| \|x\| = 2\} \to ((V \in X \land E \in Y) \to E \subseteq \{x \in 𝒫 V \| \|x\| = 2\})$
22		f1f	$⊢ ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\} \to ({I ↾}_{E}) : dom ({I ↾}_{E}) ⟶ \{x \in 𝒫 V \| \|x\| = 2\}$
23	21 22	syl11	$⊢ (V \in X \land E \in Y) \to (({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\} \to E \subseteq \{x \in 𝒫 V \| \|x\| = 2\})$
24	15 23	impbid	$⊢ (V \in X \land E \in Y) \to (E \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\})$
25		resiexg	$⊢ E \in Y \to {I ↾}_{E} \in V$
26		opiedgfv	$⊢ (V \in X \land {I ↾}_{E} \in V) \to iEdg (⟨V, {I ↾}_{E}⟩) = {I ↾}_{E}$
27	25 26	sylan2	$⊢ (V \in X \land E \in Y) \to iEdg (⟨V, {I ↾}_{E}⟩) = {I ↾}_{E}$
28	27	dmeqd	$⊢ (V \in X \land E \in Y) \to dom iEdg (⟨V, {I ↾}_{E}⟩) = dom ({I ↾}_{E})$
29		opvtxfv	$⊢ (V \in X \land {I ↾}_{E} \in V) \to Vtx (⟨V, {I ↾}_{E}⟩) = V$
30	25 29	sylan2	$⊢ (V \in X \land E \in Y) \to Vtx (⟨V, {I ↾}_{E}⟩) = V$
31	30	pweqd	$⊢ (V \in X \land E \in Y) \to 𝒫 Vtx (⟨V, {I ↾}_{E}⟩) = 𝒫 V$
32	31	rabeqdv	$⊢ (V \in X \land E \in Y) \to \{x \in 𝒫 Vtx (⟨V, {I ↾}_{E}⟩) \| \|x\| = 2\} = \{x \in 𝒫 V \| \|x\| = 2\}$
33	27 28 32	f1eq123d	$⊢ (V \in X \land E \in Y) \to (iEdg (⟨V, {I ↾}_{E}⟩) : dom iEdg (⟨V, {I ↾}_{E}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{E}⟩) \| \|x\| = 2\} \leftrightarrow ({I ↾}_{E}) : dom ({I ↾}_{E}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\})$
34	24 33	bitr4d	$⊢ (V \in X \land E \in Y) \to (E \subseteq \{x \in 𝒫 V \| \|x\| = 2\} \leftrightarrow iEdg (⟨V, {I ↾}_{E}⟩) : dom iEdg (⟨V, {I ↾}_{E}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{E}⟩) \| \|x\| = 2\})$
35		opex	$⊢ ⟨V, {I ↾}_{E}⟩ \in V$
36		eqid	$⊢ Vtx (⟨V, {I ↾}_{E}⟩) = Vtx (⟨V, {I ↾}_{E}⟩)$
37		eqid	$⊢ iEdg (⟨V, {I ↾}_{E}⟩) = iEdg (⟨V, {I ↾}_{E}⟩)$
38	36 37	isusgrs	$⊢ ⟨V, {I ↾}_{E}⟩ \in V \to (⟨V, {I ↾}_{E}⟩ \in USGraph \leftrightarrow iEdg (⟨V, {I ↾}_{E}⟩) : dom iEdg (⟨V, {I ↾}_{E}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{E}⟩) \| \|x\| = 2\})$
39	35 38	ax-mp	$⊢ ⟨V, {I ↾}_{E}⟩ \in USGraph \leftrightarrow iEdg (⟨V, {I ↾}_{E}⟩) : dom iEdg (⟨V, {I ↾}_{E}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{E}⟩) \| \|x\| = 2\}$
40	39	bicomi	$⊢ iEdg (⟨V, {I ↾}_{E}⟩) : dom iEdg (⟨V, {I ↾}_{E}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{E}⟩) \| \|x\| = 2\} \leftrightarrow ⟨V, {I ↾}_{E}⟩ \in USGraph$
41	40	a1i	$⊢ (V \in X \land E \in Y) \to (iEdg (⟨V, {I ↾}_{E}⟩) : dom iEdg (⟨V, {I ↾}_{E}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{E}⟩) \| \|x\| = 2\} \leftrightarrow ⟨V, {I ↾}_{E}⟩ \in USGraph)$
42	2 34 41	3bitrd	$⊢ (V \in X \land E \in Y) \to (V G E \leftrightarrow ⟨V, {I ↾}_{E}⟩ \in USGraph)$

Metamath Proof Explorer

Theorem ausgrusgrb

Proof