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	4 2	weeq12d	$⊢ (x = a \land r = s) \to (r We x \leftrightarrow s We a)$
9		sneq	$⊢ y = z \to \{y\} = \{z\}$
10	9	imaeq2d	$⊢ y = z \to r^{-1} [\{y\}] = r^{-1} [\{z\}]$
11	10	fveq2d	$⊢ y = z \to F (r^{-1} [\{y\}]) = F (r^{-1} [\{z\}])$
12		id	$⊢ y = z \to y = z$
13	11 12	eqeq12d	$⊢ y = z \to (F (r^{-1} [\{y\}]) = y \leftrightarrow F (r^{-1} [\{z\}]) = z)$
14	13	cbvralvw	$⊢ \forall y \in x F (r^{-1} [\{y\}]) = y \leftrightarrow \forall z \in x F (r^{-1} [\{z\}]) = z$
15	4	cnveqd	$⊢ (x = a \land r = s) \to r^{-1} = s^{-1}$
16	15	imaeq1d	$⊢ (x = a \land r = s) \to r^{-1} [\{z\}] = s^{-1} [\{z\}]$
17	16	fveqeq2d	$⊢ (x = a \land r = s) \to (F (r^{-1} [\{z\}]) = z \leftrightarrow F (s^{-1} [\{z\}]) = z)$
18	2 17	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)$
19	14 18	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)$
20	8 19	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))$
21	7 20	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)))$
22	21	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))\}$
23	1 22	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