sprsymrelf

Description: The mapping F is a 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	sprsymrelf	$⊢ F : P ⟶ 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		sprsymrelfvlem	$⊢ p \subseteq Pairs (V) \to \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \in 𝒫 (V \times V)$
5		prcom	$⊢ \{x, y\} = \{y, x\}$
6	5	a1i	$⊢ ((p \subseteq Pairs (V) \land (x \in V \land y \in V)) \land c \in p) \to \{x, y\} = \{y, x\}$
7	6	eqeq2d	$⊢ ((p \subseteq Pairs (V) \land (x \in V \land y \in V)) \land c \in p) \to (c = \{x, y\} \leftrightarrow c = \{y, x\})$
8	7	rexbidva	$⊢ (p \subseteq Pairs (V) \land (x \in V \land y \in V)) \to (\exists c \in p c = \{x, y\} \leftrightarrow \exists c \in p c = \{y, x\})$
9		df-br	$⊢ x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}$
10		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \leftrightarrow \exists c \in p c = \{x, y\}$
11	9 10	bitri	$⊢ x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow \exists c \in p c = \{x, y\}$
12		vex	$⊢ y \in V$
13		vex	$⊢ x \in V$
14		preq12	$⊢ (a = y \land b = x) \to \{a, b\} = \{y, x\}$
15	14	eqeq2d	$⊢ (a = y \land b = x) \to (c = \{a, b\} \leftrightarrow c = \{y, x\})$
16	15	rexbidv	$⊢ (a = y \land b = x) \to (\exists c \in p c = \{a, b\} \leftrightarrow \exists c \in p c = \{y, x\})$
17		preq12	$⊢ (x = a \land y = b) \to \{x, y\} = \{a, b\}$
18	17	eqeq2d	$⊢ (x = a \land y = b) \to (c = \{x, y\} \leftrightarrow c = \{a, b\})$
19	18	rexbidv	$⊢ (x = a \land y = b) \to (\exists c \in p c = \{x, y\} \leftrightarrow \exists c \in p c = \{a, b\})$
20	19	cbvopabv	$⊢ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} = \{⟨a, b⟩ \| \exists c \in p c = \{a, b\}\}$
21	12 13 16 20	braba	$⊢ y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x \leftrightarrow \exists c \in p c = \{y, x\}$
22	8 11 21	3bitr4g	$⊢ (p \subseteq Pairs (V) \land (x \in V \land y \in V)) \to (x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x)$
23	22	ralrimivva	$⊢ p \subseteq Pairs (V) \to \forall x \in V \forall y \in V (x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x)$
24	4 23	jca	$⊢ p \subseteq Pairs (V) \to (\{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \in 𝒫 (V \times V) \land \forall x \in V \forall y \in V (x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x))$
25	1	eleq2i	$⊢ p \in P \leftrightarrow p \in 𝒫 Pairs (V)$
26		vex	$⊢ p \in V$
27	26	elpw	$⊢ p \in 𝒫 Pairs (V) \leftrightarrow p \subseteq Pairs (V)$
28	25 27	bitri	$⊢ p \in P \leftrightarrow p \subseteq Pairs (V)$
29		nfopab1	$⊢ \underline{Ⅎ} x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}$
30	29	nfeq2	$⊢ Ⅎ x r = \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}$
31		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}$
32	31	nfeq2	$⊢ Ⅎ y r = \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\}$
33		breq	$⊢ r = \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \to (x r y \leftrightarrow x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y)$
34		breq	$⊢ r = \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \to (y r x \leftrightarrow y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x)$
35	33 34	bibi12d	$⊢ r = \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \to ((x r y \leftrightarrow y r x) \leftrightarrow (x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x))$
36	32 35	ralbid	$⊢ r = \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \to (\forall y \in V (x r y \leftrightarrow y r x) \leftrightarrow \forall y \in V (x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x))$
37	30 36	ralbid	$⊢ r = \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \to (\forall x \in V \forall y \in V (x r y \leftrightarrow y r x) \leftrightarrow \forall x \in V \forall y \in V (x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x))$
38	37	elrab	$⊢ \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \in \{r \in 𝒫 (V \times V) \| \forall x \in V \forall y \in V (x r y \leftrightarrow y r x)\} \leftrightarrow (\{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \in 𝒫 (V \times V) \land \forall x \in V \forall y \in V (x \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} y \leftrightarrow y \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} x))$
39	24 28 38	3imtr4i	$⊢ p \in P \to \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \in \{r \in 𝒫 (V \times V) \| \forall x \in V \forall y \in V (x r y \leftrightarrow y r x)\}$
40	39 2	eleqtrrdi	$⊢ p \in P \to \{⟨x, y⟩ \| \exists c \in p c = \{x, y\}\} \in R$
41	3 40	fmpti	$⊢ F : P ⟶ R$

Metamath Proof Explorer

Theorem sprsymrelf

Proof