fpwwe2lem4

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-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$
	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	6 9	jca	$⊢ (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to (X \in V \land R \in V)$
11		sseq1	$⊢ x = X \to (x \subseteq A \leftrightarrow X \subseteq A)$
12		xpeq12	$⊢ (x = X \land x = X) \to x \times x = X \times X$
13	12	anidms	$⊢ x = X \to x \times x = X \times X$
14	13	sseq2d	$⊢ x = X \to (r \subseteq x \times x \leftrightarrow r \subseteq X \times X)$
15		weeq2	$⊢ x = X \to (r We x \leftrightarrow r We X)$
16	11 14 15	3anbi123d	$⊢ x = X \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	16	anbi2d	$⊢ x = X \to ((φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \leftrightarrow (φ \land (X \subseteq A \land r \subseteq X \times X \land r We X)))$
18		oveq1	$⊢ x = X \to x F r = X F r$
19	18	eleq1d	$⊢ x = X \to (x F r \in A \leftrightarrow X F r \in A)$
20	17 19	imbi12d	$⊢ x = X \to (((φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A) \leftrightarrow ((φ \land (X \subseteq A \land r \subseteq X \times X \land r We X)) \to X F r \in A))$
21		sseq1	$⊢ r = R \to (r \subseteq X \times X \leftrightarrow R \subseteq X \times X)$
22		weeq1	$⊢ r = R \to (r We X \leftrightarrow R We X)$
23	21 22	3anbi23d	$⊢ 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))$
24	23	anbi2d	$⊢ r = R \to ((φ \land (X \subseteq A \land r \subseteq X \times X \land r We X)) \leftrightarrow (φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)))$
25		oveq2	$⊢ r = R \to X F r = X F R$
26	25	eleq1d	$⊢ r = R \to (X F r \in A \leftrightarrow X F R \in A)$
27	24 26	imbi12d	$⊢ r = R \to (((φ \land (X \subseteq A \land r \subseteq X \times X \land r We X)) \to X F r \in A) \leftrightarrow ((φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to X F R \in A))$
28	20 27 3	vtocl2g	$⊢ (X \in V \land R \in V) \to ((φ \land (X \subseteq A \land R \subseteq X \times X \land R We X)) \to X F R \in A)$
29	10 28	mpcom	$⊢ (φ \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