fpwwe2cbv

		Ref	Expression
	Hypothesis	fpwwe2.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\}$
	Assertion	fpwwe2cbv	$⊢ W = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = z))\}$

Proof

Step	Hyp	Ref	Expression
1		fpwwe2.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = 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		id	$⊢ u = v \to u = v$
10	9	sqxpeqd	$⊢ u = v \to u \times u = v \times v$
11	10	ineq2d	$⊢ u = v \to r \cap (u \times u) = r \cap (v \times v)$
12	9 11	oveq12d	$⊢ u = v \to u F (r \cap (u \times u)) = v F (r \cap (v \times v))$
13	12	eqeq1d	$⊢ u = v \to (u F (r \cap (u \times u)) = y \leftrightarrow v F (r \cap (v \times v)) = y)$
14	13	cbvsbcvw	$⊢ \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y \leftrightarrow \underset{˙}{[} r^{-1} [\{y\}] / v \underset{˙}{]} v F (r \cap (v \times v)) = y$
15		sneq	$⊢ y = z \to \{y\} = \{z\}$
16	15	imaeq2d	$⊢ y = z \to r^{-1} [\{y\}] = r^{-1} [\{z\}]$
17		eqeq2	$⊢ y = z \to (v F (r \cap (v \times v)) = y \leftrightarrow v F (r \cap (v \times v)) = z)$
18	16 17	sbceqbid	$⊢ y = z \to (\underset{˙}{[} r^{-1} [\{y\}] / v \underset{˙}{]} v F (r \cap (v \times v)) = y \leftrightarrow \underset{˙}{[} r^{-1} [\{z\}] / v \underset{˙}{]} v F (r \cap (v \times v)) = z)$
19	14 18	bitrid	$⊢ y = z \to (\underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y \leftrightarrow \underset{˙}{[} r^{-1} [\{z\}] / v \underset{˙}{]} v F (r \cap (v \times v)) = z)$
20	19	cbvralvw	$⊢ \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y \leftrightarrow \forall z \in x \underset{˙}{[} r^{-1} [\{z\}] / v \underset{˙}{]} v F (r \cap (v \times v)) = z$
21	4	cnveqd	$⊢ (x = a \land r = s) \to r^{-1} = s^{-1}$
22	21	imaeq1d	$⊢ (x = a \land r = s) \to r^{-1} [\{z\}] = s^{-1} [\{z\}]$
23	4	ineq1d	$⊢ (x = a \land r = s) \to r \cap (v \times v) = s \cap (v \times v)$
24	23	oveq2d	$⊢ (x = a \land r = s) \to v F (r \cap (v \times v)) = v F (s \cap (v \times v))$
25	24	eqeq1d	$⊢ (x = a \land r = s) \to (v F (r \cap (v \times v)) = z \leftrightarrow v F (s \cap (v \times v)) = z)$
26	22 25	sbceqbid	$⊢ (x = a \land r = s) \to (\underset{˙}{[} r^{-1} [\{z\}] / v \underset{˙}{]} v F (r \cap (v \times v)) = z \leftrightarrow \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = z)$
27	2 26	raleqbidv	$⊢ (x = a \land r = s) \to (\forall z \in x \underset{˙}{[} r^{-1} [\{z\}] / v \underset{˙}{]} v F (r \cap (v \times v)) = z \leftrightarrow \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = z)$
28	20 27	bitrid	$⊢ (x = a \land r = s) \to (\forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y \leftrightarrow \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = z)$
29	8 28	anbi12d	$⊢ (x = a \land r = s) \to ((r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y) \leftrightarrow (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = z))$
30	7 29	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 \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y)) \leftrightarrow ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = z)))$
31	30	cbvopabv	$⊢ \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\} = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = z))\}$
32	1 31	eqtri	$⊢ W = \{⟨a, s⟩ \| ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall z \in a \underset{˙}{[} s^{-1} [\{z\}] / v \underset{˙}{]} v F (s \cap (v \times v)) = z))\}$

Metamath Proof Explorer

Theorem fpwwe2cbv

Proof