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		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		id	$⊢ u = v \to u = v$
12	11	sqxpeqd	$⊢ u = v \to u \times u = v \times v$
13	12	ineq2d	$⊢ u = v \to r \cap (u \times u) = r \cap (v \times v)$
14	11 13	oveq12d	$⊢ u = v \to u F (r \cap (u \times u)) = v F (r \cap (v \times v))$
15	14	eqeq1d	$⊢ u = v \to (u F (r \cap (u \times u)) = y \leftrightarrow v F (r \cap (v \times v)) = y)$
16	15	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$
17		sneq	$⊢ y = z \to \{y\} = \{z\}$
18	17	imaeq2d	$⊢ y = z \to r^{-1} [\{y\}] = r^{-1} [\{z\}]$
19		eqeq2	$⊢ y = z \to (v F (r \cap (v \times v)) = y \leftrightarrow v F (r \cap (v \times v)) = z)$
20	18 19	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)$
21	16 20	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)$
22	21	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$
23	4	cnveqd	$⊢ (x = a \land r = s) \to r^{-1} = s^{-1}$
24	23	imaeq1d	$⊢ (x = a \land r = s) \to r^{-1} [\{z\}] = s^{-1} [\{z\}]$
25	4	ineq1d	$⊢ (x = a \land r = s) \to r \cap (v \times v) = s \cap (v \times v)$
26	25	oveq2d	$⊢ (x = a \land r = s) \to v F (r \cap (v \times v)) = v F (s \cap (v \times v))$
27	26	eqeq1d	$⊢ (x = a \land r = s) \to (v F (r \cap (v \times v)) = z \leftrightarrow v F (s \cap (v \times v)) = z)$
28	24 27	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)$
29	2 28	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)$
30	22 29	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)$
31	10 30	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))$
32	7 31	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)))$
33	32	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))\}$
34	1 33	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