fpwwelem

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

	Ref	Expression
Hypotheses	fpwwe.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
	fpwwe.2	$⊢ φ \to A \in V$
Assertion	fpwwelem	$⊢ φ \to (X W R \leftrightarrow ((X \subseteq A \land R \subseteq X \times X) \land (R We X \land \forall y \in X F (R^{-1} [\{y\}]) = y)))$

Proof

Step	Hyp	Ref	Expression
1		fpwwe.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
2		fpwwe.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 F (R^{-1} [\{y\}]) = 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 F (R^{-1} [\{y\}]) = 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 F (R^{-1} [\{y\}]) = 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 F (R^{-1} [\{y\}]) = 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 F (R^{-1} [\{y\}]) = 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 F (R^{-1} [\{y\}]) = 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 F (R^{-1} [\{y\}]) = 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		weeq2	$⊢ x = X \to (r We x \leftrightarrow r We X)$
21		weeq1	$⊢ r = R \to (r We X \leftrightarrow R We X)$
22	20 21	sylan9bb	$⊢ (x = X \land r = R) \to (r We x \leftrightarrow R We X)$
23	16	cnveqd	$⊢ (x = X \land r = R) \to r^{-1} = R^{-1}$
24	23	imaeq1d	$⊢ (x = X \land r = R) \to r^{-1} [\{y\}] = R^{-1} [\{y\}]$
25	24	fveqeq2d	$⊢ (x = X \land r = R) \to (F (r^{-1} [\{y\}]) = y \leftrightarrow F (R^{-1} [\{y\}]) = y)$
26	14 25	raleqbidv	$⊢ (x = X \land r = R) \to (\forall y \in x F (r^{-1} [\{y\}]) = y \leftrightarrow \forall y \in X F (R^{-1} [\{y\}]) = y)$
27	22 26	anbi12d	$⊢ (x = X \land r = R) \to ((r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y) \leftrightarrow (R We X \land \forall y \in X F (R^{-1} [\{y\}]) = y))$
28	19 27	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 F (r^{-1} [\{y\}]) = y)) \leftrightarrow ((X \subseteq A \land R \subseteq X \times X) \land (R We X \land \forall y \in X F (R^{-1} [\{y\}]) = y)))$
29	28 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 F (R^{-1} [\{y\}]) = y)))$
30	6 13 29	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 F (R^{-1} [\{y\}]) = y)))$

Metamath Proof Explorer

Theorem fpwwelem

Proof