fpwwe2lem4

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015) (Revised by AV, 20-Jul-2024) (Proof shortened by Matthew House, 10-Sep-2025)

	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$
	fpwwe2.3	$⊢ (φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
Assertion	fpwwe2lem4	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to X F R \in A$

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		fpwwe2.3	$⊢ (φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
4	2	adantr	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to A \in V$
5		simpr1	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to X \subseteq A$
6	4 5	ssexd	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to X \in V$
7	6 6	xpexd	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to X \times X \in V$
8		simpr2	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to R \subseteq X \times X$
9	7 8	ssexd	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to R \in V$
10		simpl	$⊢ (x = X \land r = R) \to x = X$
11	10	sseq1d	$⊢ (x = X \land r = R) \to (x \subseteq A \leftrightarrow X \subseteq A)$
12		simpr	$⊢ (x = X \land r = R) \to r = R$
13	10	sqxpeqd	$⊢ (x = X \land r = R) \to x \times x = X \times X$
14	12 13	sseq12d	$⊢ (x = X \land r = R) \to (r \subseteq x \times x \leftrightarrow R \subseteq X \times X)$
15	12 10	weeq12d	$⊢ (x = X \land r = R) \to (r We x \leftrightarrow R We X)$
16	11 14 15	3anbi123d	$⊢ (x = X \land r = R) \to ((x \subseteq A \land r \subseteq x \times x \land r We x) \leftrightarrow (X \subseteq A \land R \subseteq X \times X \land R We X))$
17		oveq12	$⊢ (x = X \land r = R) \to x F r = X F R$
18	17	eleq1d	$⊢ (x = X \land r = R) \to (x F r \in A \leftrightarrow X F R \in A)$
19	16 18	imbi12d	$⊢ (x = X \land r = R) \to (((x \subseteq A \land r \subseteq x \times x \land r We x) \to x F r \in A) \leftrightarrow ((X \subseteq A \land R \subseteq X \times X \land R We X) \to X F R \in A))$
20	3	ex	$⊢ φ \to ((x \subseteq A \land r \subseteq x \times x \land r We x) \to x F r \in A)$
21	20	adantr	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to ((x \subseteq A \land r \subseteq x \times x \land r We x) \to x F r \in A)$
22	6 9 19 21	vtocl2d	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to ((X \subseteq A \land R \subseteq X \times X \land R We X) \to X F R \in A)$
23	22	syldbl2	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to X F R \in A$

Metamath Proof Explorer

Theorem fpwwe2lem4

Proof