sprsymrelf1

Description: The mapping F is a one-to-one function from the subsets of the set of pairs over a fixed set V into the symmetric relations R on the fixed set V . (Contributed by AV, 19-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)\}$
	sprsymrelf.f	$⊢ F = (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\})$
Assertion	sprsymrelf1	$⊢ F : P \underset{1-1}{⟶} 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		sprsymrelf.f	$⊢ F = (p \in P ⟼ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\})$
4	1 2 3	sprsymrelf	$⊢ F : P ⟶ R$
5	1 2 3	sprsymrelfv	$⊢ a \in P \to F (a) = \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\}$
6	1 2 3	sprsymrelfv	$⊢ b \in P \to F (b) = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}$
7	5 6	eqeqan12d	$⊢ (a \in P \land b \in P) \to (F (a) = F (b) \leftrightarrow \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\})$
8	1	eleq2i	$⊢ a \in P \leftrightarrow a \in 𝒫 Pairs (V)$
9		vex	$⊢ a \in V$
10	9	elpw	$⊢ a \in 𝒫 Pairs (V) \leftrightarrow a \subseteq Pairs (V)$
11	8 10	bitri	$⊢ a \in P \leftrightarrow a \subseteq Pairs (V)$
12	1	eleq2i	$⊢ b \in P \leftrightarrow b \in 𝒫 Pairs (V)$
13		vex	$⊢ b \in V$
14	13	elpw	$⊢ b \in 𝒫 Pairs (V) \leftrightarrow b \subseteq Pairs (V)$
15	12 14	bitri	$⊢ b \in P \leftrightarrow b \subseteq Pairs (V)$
16		sprsymrelf1lem	$⊢ (a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \to (\{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to a \subseteq b)$
17	16	imp	$⊢ ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \to a \subseteq b$
18		eqcom	$⊢ \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \leftrightarrow \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\}$
19		sprsymrelf1lem	$⊢ (b \subseteq Pairs (V) \land a \subseteq Pairs (V)) \to (\{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} \to b \subseteq a)$
20	18 19	syl5bi	$⊢ (b \subseteq Pairs (V) \land a \subseteq Pairs (V)) \to (\{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to b \subseteq a)$
21	20	ancoms	$⊢ (a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \to (\{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to b \subseteq a)$
22	21	imp	$⊢ ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \to b \subseteq a$
23	17 22	eqssd	$⊢ ((a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \land \{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\}) \to a = b$
24	23	ex	$⊢ (a \subseteq Pairs (V) \land b \subseteq Pairs (V)) \to (\{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to a = b)$
25	11 15 24	syl2anb	$⊢ (a \in P \land b \in P) \to (\{⟨x, y⟩ \| \exists c \in a c = \{x, y\}\} = \{⟨x, y⟩ \| \exists c \in b c = \{x, y\}\} \to a = b)$
26	7 25	sylbid	$⊢ (a \in P \land b \in P) \to (F (a) = F (b) \to a = b)$
27	26	rgen2	$⊢ \forall a \in P \forall b \in P (F (a) = F (b) \to a = b)$
28		dff13	$⊢ F : P \underset{1-1}{⟶} R \leftrightarrow (F : P ⟶ R \land \forall a \in P \forall b \in P (F (a) = F (b) \to a = b))$
29	4 27 28	mpbir2an	$⊢ F : P \underset{1-1}{⟶} R$

Metamath Proof Explorer

Theorem sprsymrelf1

Proof