fpwwe2lem2

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 19-May-2015) (Revised by AV, 20-Jul-2024)

	Ref	Expression
Hypotheses	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))\}$
	fpwwe2.2	$⊢ φ \to A \in V$
Assertion	fpwwe2lem2	$⊢ φ \to (X W R \leftrightarrow ((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)))$

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		fpwwe2.2	$⊢ φ \to A \in V$
3	1	relopabiv	$⊢ Rel W$
4	3	a1i	$⊢ φ \to Rel W$
5		brrelex12	$⊢ (Rel W \land X W R) \to (X \in V \land R \in V)$
6	4 5	sylan	$⊢ (φ \land X W R) \to (X \in V \land R \in V)$
7	2	adantr	$⊢ (φ \land ((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))) \to A \in V$
8		simprll	$⊢ (φ \land ((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))) \to X \subseteq A$
9	7 8	ssexd	$⊢ (φ \land ((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))) \to X \in V$
10	9 9	xpexd	$⊢ (φ \land ((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))) \to X \times X \in V$
11		simprlr	$⊢ (φ \land ((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))) \to R \subseteq X \times X$
12	10 11	ssexd	$⊢ (φ \land ((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))) \to R \in V$
13	9 12	jca	$⊢ (φ \land ((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))) \to (X \in V \land R \in V)$
14		simpl	$⊢ (x = X \land r = R) \to x = X$
15	14	sseq1d	$⊢ (x = X \land r = R) \to (x \subseteq A \leftrightarrow X \subseteq A)$
16		simpr	$⊢ (x = X \land r = R) \to r = R$
17	14	sqxpeqd	$⊢ (x = X \land r = R) \to x \times x = X \times X$
18	16 17	sseq12d	$⊢ (x = X \land r = R) \to (r \subseteq x \times x \leftrightarrow R \subseteq X \times X)$
19	15 18	anbi12d	$⊢ (x = X \land r = R) \to ((x \subseteq A \land r \subseteq x \times x) \leftrightarrow (X \subseteq A \land R \subseteq X \times X))$
20	16 14	weeq12d	$⊢ (x = X \land r = R) \to (r We x \leftrightarrow R We X)$
21	16	cnveqd	$⊢ (x = X \land r = R) \to r^{-1} = R^{-1}$
22	21	imaeq1d	$⊢ (x = X \land r = R) \to r^{-1} [\{y\}] = R^{-1} [\{y\}]$
23	16	ineq1d	$⊢ (x = X \land r = R) \to r \cap (u \times u) = R \cap (u \times u)$
24	23	oveq2d	$⊢ (x = X \land r = R) \to u F (r \cap (u \times u)) = u F (R \cap (u \times u))$
25	24	eqeq1d	$⊢ (x = X \land r = R) \to (u F (r \cap (u \times u)) = y \leftrightarrow u F (R \cap (u \times u)) = y)$
26	22 25	sbceqbid	$⊢ (x = X \land r = R) \to (\underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y \leftrightarrow \underset{˙}{[} R^{-1} [\{y\}] / u \underset{˙}{]} u F (R \cap (u \times u)) = y)$
27	14 26	raleqbidv	$⊢ (x = X \land r = R) \to (\forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y \leftrightarrow \forall y \in X \underset{˙}{[} R^{-1} [\{y\}] / u \underset{˙}{]} u F (R \cap (u \times u)) = y)$
28	20 27	anbi12d	$⊢ (x = X \land r = R) \to ((r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y) \leftrightarrow (R We X \land \forall y \in X \underset{˙}{[} R^{-1} [\{y\}] / u \underset{˙}{]} u F (R \cap (u \times u)) = y))$
29	19 28	anbi12d	$⊢ (x = X \land r = R) \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 ((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)))$
30	29 1	brabga	$⊢ (X \in V \land R \in V) \to (X W R \leftrightarrow ((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)))$
31	6 13 30	pm5.21nd	$⊢ φ \to (X W R \leftrightarrow ((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)))$

Metamath Proof Explorer

Theorem fpwwe2lem2

Proof