usgrexi

Description: An arbitrary set regarded as vertices together with the set of pairs of elements of this set regarded as edges is a simple graph. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 5-Nov-2020) (Proof shortened by AV, 10-Nov-2021)

		Ref	Expression
	Hypothesis	usgrexi.p	$⊢ P = \{x \in 𝒫 V \| \|x\| = 2\}$
	Assertion	usgrexi	$⊢ V \in W \to ⟨V, {I ↾}_{P}⟩ \in USGraph$

Proof

Step	Hyp	Ref	Expression
1		usgrexi.p	$⊢ P = \{x \in 𝒫 V \| \|x\| = 2\}$
2	1	usgrexilem	$⊢ V \in W \to ({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\}$
3	1	cusgrexilem1	$⊢ V \in W \to {I ↾}_{P} \in V$
4		opiedgfv	$⊢ (V \in W \land {I ↾}_{P} \in V) \to iEdg (⟨V, {I ↾}_{P}⟩) = {I ↾}_{P}$
5	3 4	mpdan	$⊢ V \in W \to iEdg (⟨V, {I ↾}_{P}⟩) = {I ↾}_{P}$
6	5	dmeqd	$⊢ V \in W \to dom iEdg (⟨V, {I ↾}_{P}⟩) = dom ({I ↾}_{P})$
7		opvtxfv	$⊢ (V \in W \land {I ↾}_{P} \in V) \to Vtx (⟨V, {I ↾}_{P}⟩) = V$
8	3 7	mpdan	$⊢ V \in W \to Vtx (⟨V, {I ↾}_{P}⟩) = V$
9	8	pweqd	$⊢ V \in W \to 𝒫 Vtx (⟨V, {I ↾}_{P}⟩) = 𝒫 V$
10	9	rabeqdv	$⊢ V \in W \to \{x \in 𝒫 Vtx (⟨V, {I ↾}_{P}⟩) \| \|x\| = 2\} = \{x \in 𝒫 V \| \|x\| = 2\}$
11	5 6 10	f1eq123d	$⊢ V \in W \to (iEdg (⟨V, {I ↾}_{P}⟩) : dom iEdg (⟨V, {I ↾}_{P}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{P}⟩) \| \|x\| = 2\} \leftrightarrow ({I ↾}_{P}) : dom ({I ↾}_{P}) \underset{1-1}{⟶} \{x \in 𝒫 V \| \|x\| = 2\})$
12	2 11	mpbird	$⊢ V \in W \to iEdg (⟨V, {I ↾}_{P}⟩) : dom iEdg (⟨V, {I ↾}_{P}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{P}⟩) \| \|x\| = 2\}$
13		opex	$⊢ ⟨V, {I ↾}_{P}⟩ \in V$
14		eqid	$⊢ Vtx (⟨V, {I ↾}_{P}⟩) = Vtx (⟨V, {I ↾}_{P}⟩)$
15		eqid	$⊢ iEdg (⟨V, {I ↾}_{P}⟩) = iEdg (⟨V, {I ↾}_{P}⟩)$
16	14 15	isusgrs	$⊢ ⟨V, {I ↾}_{P}⟩ \in V \to (⟨V, {I ↾}_{P}⟩ \in USGraph \leftrightarrow iEdg (⟨V, {I ↾}_{P}⟩) : dom iEdg (⟨V, {I ↾}_{P}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{P}⟩) \| \|x\| = 2\})$
17	13 16	mp1i	$⊢ V \in W \to (⟨V, {I ↾}_{P}⟩ \in USGraph \leftrightarrow iEdg (⟨V, {I ↾}_{P}⟩) : dom iEdg (⟨V, {I ↾}_{P}⟩) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (⟨V, {I ↾}_{P}⟩) \| \|x\| = 2\})$
18	12 17	mpbird	$⊢ V \in W \to ⟨V, {I ↾}_{P}⟩ \in USGraph$

Metamath Proof Explorer

Theorem usgrexi

Proof