fpwwecbv

		Ref	Expression
	Hypothesis	fpwwe.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
	Assertion	fpwwecbv	$⊢ W = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a F (s^{-1} [\{z\}]) = z))\}$

Proof

Step	Hyp	Ref	Expression
1		fpwwe.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
2		simpl	$⊢ (x = a \land r = s) \to x = a$
3	2	sseq1d	$⊢ (x = a \land r = s) \to (x \subseteq A \leftrightarrow a \subseteq A)$
4		simpr	$⊢ (x = a \land r = s) \to r = s$
5	2	sqxpeqd	$⊢ (x = a \land r = s) \to x \times x = a \times a$
6	4 5	sseq12d	$⊢ (x = a \land r = s) \to (r \subseteq x \times x \leftrightarrow s \subseteq a \times a)$
7	3 6	anbi12d	$⊢ (x = a \land r = s) \to ((x \subseteq A \land r \subseteq x \times x) \leftrightarrow (a \subseteq A \land s \subseteq a \times a))$
8		weeq2	$⊢ x = a \to (r We x \leftrightarrow r We a)$
9		weeq1	$⊢ r = s \to (r We a \leftrightarrow s We a)$
10	8 9	sylan9bb	$⊢ (x = a \land r = s) \to (r We x \leftrightarrow s We a)$
11		sneq	$⊢ y = z \to \{y\} = \{z\}$
12	11	imaeq2d	$⊢ y = z \to r^{-1} [\{y\}] = r^{-1} [\{z\}]$
13	12	fveq2d	$⊢ y = z \to F (r^{-1} [\{y\}]) = F (r^{-1} [\{z\}])$
14		id	$⊢ y = z \to y = z$
15	13 14	eqeq12d	$⊢ y = z \to (F (r^{-1} [\{y\}]) = y \leftrightarrow F (r^{-1} [\{z\}]) = z)$
16	15	cbvralvw	$⊢ \forall y \in x F (r^{-1} [\{y\}]) = y \leftrightarrow \forall z \in x F (r^{-1} [\{z\}]) = z$
17	4	cnveqd	$⊢ (x = a \land r = s) \to r^{-1} = s^{-1}$
18	17	imaeq1d	$⊢ (x = a \land r = s) \to r^{-1} [\{z\}] = s^{-1} [\{z\}]$
19	18	fveqeq2d	$⊢ (x = a \land r = s) \to (F (r^{-1} [\{z\}]) = z \leftrightarrow F (s^{-1} [\{z\}]) = z)$
20	2 19	raleqbidv	$⊢ (x = a \land r = s) \to (\forall z \in x F (r^{-1} [\{z\}]) = z \leftrightarrow \forall z \in a F (s^{-1} [\{z\}]) = z)$
21	16 20	bitrid	$⊢ (x = a \land r = s) \to (\forall y \in x F (r^{-1} [\{y\}]) = y \leftrightarrow \forall z \in a F (s^{-1} [\{z\}]) = z)$
22	10 21	anbi12d	$⊢ (x = a \land r = s) \to ((r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y) \leftrightarrow (s We a \land \forall z \in a F (s^{-1} [\{z\}]) = z))$
23	7 22	anbi12d	$⊢ (x = a \land r = s) \to (((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y)) \leftrightarrow ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a F (s^{-1} [\{z\}]) = z)))$
24	23	cbvopabv	$⊢ \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\} = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a F (s^{-1} [\{z\}]) = z))\}$
25	1 24	eqtri	$⊢ W = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a F (s^{-1} [\{z\}]) = z))\}$

Metamath Proof Explorer

Theorem fpwwecbv

Proof