Metamath Proof Explorer

Theorem sprbisymrel

Description: There is a bijection between the subsets of the set of pairs over a fixed set V and the symmetric relations R on the fixed set V . (Contributed by AV, 23-Nov-2021)

		Ref	Expression
	Hypotheses	sprsymrelf.p	$⊢ P = 𝒫 Pairs (V)$
		sprsymrelf.r	$⊢ R = \{r \in 𝒫 (V \times V) \| \forall x \in V \forall y \in V (x r y \leftrightarrow y r x)\}$
	Assertion	sprbisymrel	$⊢ V \in W \to \exists f f : P \underset{1-1 onto}{⟶} R$

Proof

Step	Hyp	Ref	Expression
1		sprsymrelf.p	$⊢ P = 𝒫 Pairs (V)$
2		sprsymrelf.r	$⊢ R = \{r \in 𝒫 (V \times V) \| \forall x \in V \forall y \in V (x r y \leftrightarrow y r x)\}$
3		fvex	$⊢ Pairs (V) \in V$
4	3	pwex	$⊢ 𝒫 Pairs (V) \in V$
5	1 4	eqeltri	$⊢ P \in V$
6		mptexg	$⊢ P \in V \to (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}) \in V$
7	5 6	mp1i	$⊢ V \in W \to (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}) \in V$
8		eqid	$⊢ (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}) = (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\})$
9	1 2 8	sprsymrelf1o	$⊢ V \in W \to (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}) : P \underset{1-1 onto}{⟶} R$
10		f1oeq1	$⊢ f = (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}) \to (f : P \underset{1-1 onto}{⟶} R \leftrightarrow (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}) : P \underset{1-1 onto}{⟶} R)$
11	10	spcegv	$⊢ (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}) \in V \to ((p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}) : P \underset{1-1 onto}{⟶} R \to \exists f f : P \underset{1-1 onto}{⟶} R)$
12	7 9 11	sylc	$⊢ V \in W \to \exists f f : P \underset{1-1 onto}{⟶} R$