fpwwe2lem12

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-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$
	fpwwe2.4	$⊢ X = ⋃ dom W$
Assertion	fpwwe2lem12	$⊢ φ \to X F W (X) \in X$

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		fpwwe2.4	$⊢ X = ⋃ dom W$
5		ssun2	$⊢ \{X F W (X)\} \subseteq X \cup \{X F W (X)\}$
6	2	adantr	$⊢ (φ \land \neg X F W (X) \in X) \to A \in V$
7	3	adantlr	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
8	1 6 7 4	fpwwe2lem11	$⊢ (φ \land \neg X F W (X) \in X) \to X \in dom W$
9	1 6 7 4	fpwwe2lem10	$⊢ (φ \land \neg X F W (X) \in X) \to W : dom W ⟶ 𝒫 (X \times X)$
10		ffun	$⊢ W : dom W ⟶ 𝒫 (X \times X) \to Fun W$
11		funfvbrb	$⊢ Fun W \to (X \in dom W \leftrightarrow X W W (X))$
12	9 10 11	3syl	$⊢ (φ \land \neg X F W (X) \in X) \to (X \in dom W \leftrightarrow X W W (X))$
13	8 12	mpbid	$⊢ (φ \land \neg X F W (X) \in X) \to X W W (X)$
14	1 6	fpwwe2lem2	$⊢ (φ \land \neg X F W (X) \in X) \to (X W W (X) \leftrightarrow ((X \subseteq A \land W (X) \subseteq X \times X) \land (W (X) We X \land \forall y \in X \underset{˙}{[} {W (X)}^{-1} [\{y\}] / u \underset{˙}{]} u F (W (X) \cap (u \times u)) = y)))$
15	13 14	mpbid	$⊢ (φ \land \neg X F W (X) \in X) \to ((X \subseteq A \land W (X) \subseteq X \times X) \land (W (X) We X \land \forall y \in X \underset{˙}{[} {W (X)}^{-1} [\{y\}] / u \underset{˙}{]} u F (W (X) \cap (u \times u)) = y))$
16	15	simpld	$⊢ (φ \land \neg X F W (X) \in X) \to (X \subseteq A \land W (X) \subseteq X \times X)$
17	16	simpld	$⊢ (φ \land \neg X F W (X) \in X) \to X \subseteq A$
18	16	simprd	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) \subseteq X \times X$
19	15	simprd	$⊢ (φ \land \neg X F W (X) \in X) \to (W (X) We X \land \forall y \in X \underset{˙}{[} {W (X)}^{-1} [\{y\}] / u \underset{˙}{]} u F (W (X) \cap (u \times u)) = y)$
20	19	simpld	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) We X$
21	17 18 20	3jca	$⊢ (φ \land \neg X F W (X) \in X) \to (X \subseteq A \land W (X) \subseteq X \times X \land W (X) We X)$
22	1 2 3	fpwwe2lem4	$⊢ (φ \land (X \subseteq A \land W (X) \subseteq X \times X \land W (X) We X)) \to X F W (X) \in A$
23	21 22	syldan	$⊢ (φ \land \neg X F W (X) \in X) \to X F W (X) \in A$
24	23	snssd	$⊢ (φ \land \neg X F W (X) \in X) \to \{X F W (X)\} \subseteq A$
25	17 24	unssd	$⊢ (φ \land \neg X F W (X) \in X) \to X \cup \{X F W (X)\} \subseteq A$
26		ssun1	$⊢ X \subseteq X \cup \{X F W (X)\}$
27		xpss12	$⊢ (X \subseteq X \cup \{X F W (X)\} \land X \subseteq X \cup \{X F W (X)\}) \to X \times X \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})$
28	26 26 27	mp2an	$⊢ X \times X \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})$
29	18 28	sstrdi	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})$
30		xpss12	$⊢ (X \subseteq X \cup \{X F W (X)\} \land \{X F W (X)\} \subseteq X \cup \{X F W (X)\}) \to X \times \{X F W (X)\} \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})$
31	26 5 30	mp2an	$⊢ X \times \{X F W (X)\} \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})$
32	31	a1i	$⊢ (φ \land \neg X F W (X) \in X) \to X \times \{X F W (X)\} \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})$
33	29 32	unssd	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) \cup (X \times \{X F W (X)\}) \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})$
34	25 33	jca	$⊢ (φ \land \neg X F W (X) \in X) \to (X \cup \{X F W (X)\} \subseteq A \land W (X) \cup (X \times \{X F W (X)\}) \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\}))$
35		ssdif0	$⊢ x \subseteq \{X F W (X)\} \leftrightarrow x ∖ \{X F W (X)\} = \emptyset$
36		simpllr	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to \neg X F W (X) \in X$
37	18	ad2antrr	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to W (X) \subseteq X \times X$
38	37	ssbrd	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to ((X F W (X)) W (X) (X F W (X)) \to (X F W (X)) (X \times X) (X F W (X)))$
39		brxp	$⊢ (X F W (X)) (X \times X) (X F W (X)) \leftrightarrow (X F W (X) \in X \land X F W (X) \in X)$
40	39	simplbi	$⊢ (X F W (X)) (X \times X) (X F W (X)) \to X F W (X) \in X$
41	38 40	syl6	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to ((X F W (X)) W (X) (X F W (X)) \to X F W (X) \in X)$
42	36 41	mtod	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to \neg (X F W (X)) W (X) (X F W (X))$
43		brxp	$⊢ (X F W (X)) (X \times \{X F W (X)\}) (X F W (X)) \leftrightarrow (X F W (X) \in X \land X F W (X) \in \{X F W (X)\})$
44	43	simplbi	$⊢ (X F W (X)) (X \times \{X F W (X)\}) (X F W (X)) \to X F W (X) \in X$
45	36 44	nsyl	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to \neg (X F W (X)) (X \times \{X F W (X)\}) (X F W (X))$
46		ovex	$⊢ X F W (X) \in V$
47		breq2	$⊢ y = X F W (X) \to ((X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) (X F W (X)))$
48		brun	$⊢ (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) (X F W (X)) \leftrightarrow ((X F W (X)) W (X) (X F W (X)) \lor (X F W (X)) (X \times \{X F W (X)\}) (X F W (X)))$
49	47 48	bitrdi	$⊢ y = X F W (X) \to ((X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow ((X F W (X)) W (X) (X F W (X)) \lor (X F W (X)) (X \times \{X F W (X)\}) (X F W (X))))$
50	49	notbid	$⊢ y = X F W (X) \to (\neg (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \neg ((X F W (X)) W (X) (X F W (X)) \lor (X F W (X)) (X \times \{X F W (X)\}) (X F W (X))))$
51	46 50	rexsn	$⊢ \exists y \in \{X F W (X)\} \neg (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \neg ((X F W (X)) W (X) (X F W (X)) \lor (X F W (X)) (X \times \{X F W (X)\}) (X F W (X)))$
52		ioran	$⊢ \neg ((X F W (X)) W (X) (X F W (X)) \lor (X F W (X)) (X \times \{X F W (X)\}) (X F W (X))) \leftrightarrow (\neg (X F W (X)) W (X) (X F W (X)) \land \neg (X F W (X)) (X \times \{X F W (X)\}) (X F W (X)))$
53	51 52	bitri	$⊢ \exists y \in \{X F W (X)\} \neg (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow (\neg (X F W (X)) W (X) (X F W (X)) \land \neg (X F W (X)) (X \times \{X F W (X)\}) (X F W (X)))$
54	42 45 53	sylanbrc	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to \exists y \in \{X F W (X)\} \neg (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y$
55		simpr	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to x \subseteq \{X F W (X)\}$
56		sssn	$⊢ x \subseteq \{X F W (X)\} \leftrightarrow (x = \emptyset \lor x = \{X F W (X)\})$
57	55 56	sylib	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to (x = \emptyset \lor x = \{X F W (X)\})$
58		simplrr	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to x \neq \emptyset$
59	58	neneqd	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to \neg x = \emptyset$
60	57 59	orcnd	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to x = \{X F W (X)\}$
61	60	raleqdv	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to (\forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \forall z \in \{X F W (X)\} \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
62		breq1	$⊢ z = X F W (X) \to (z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y)$
63	62	notbid	$⊢ z = X F W (X) \to (\neg z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \neg (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y)$
64	46 63	ralsn	$⊢ \forall z \in \{X F W (X)\} \neg z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \neg (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y$
65	61 64	bitrdi	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to (\forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \neg (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y)$
66	60 65	rexeqbidv	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to (\exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \exists y \in \{X F W (X)\} \neg (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y)$
67	54 66	mpbird	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x \subseteq \{X F W (X)\}) \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y$
68	67	ex	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \to (x \subseteq \{X F W (X)\} \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
69	35 68	syl5bir	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \to (x ∖ \{X F W (X)\} = \emptyset \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
70		vex	$⊢ x \in V$
71		difexg	$⊢ x \in V \to x ∖ \{X F W (X)\} \in V$
72	70 71	mp1i	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to x ∖ \{X F W (X)\} \in V$
73		wefr	$⊢ W (X) We X \to W (X) Fr X$
74	20 73	syl	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) Fr X$
75	74	ad2antrr	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to W (X) Fr X$
76		simplrl	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to x \subseteq X \cup \{X F W (X)\}$
77		uncom	$⊢ X \cup \{X F W (X)\} = \{X F W (X)\} \cup X$
78	76 77	sseqtrdi	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to x \subseteq \{X F W (X)\} \cup X$
79		ssundif	$⊢ x \subseteq \{X F W (X)\} \cup X \leftrightarrow x ∖ \{X F W (X)\} \subseteq X$
80	78 79	sylib	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to x ∖ \{X F W (X)\} \subseteq X$
81		simpr	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to x ∖ \{X F W (X)\} \neq \emptyset$
82		fri	$⊢ ((x ∖ \{X F W (X)\} \in V \land W (X) Fr X) \land (x ∖ \{X F W (X)\} \subseteq X \land x ∖ \{X F W (X)\} \neq \emptyset)) \to \exists y \in (x ∖ \{X F W (X)\}) \forall z \in (x ∖ \{X F W (X)\}) \neg z W (X) y$
83	72 75 80 81 82	syl22anc	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to \exists y \in (x ∖ \{X F W (X)\}) \forall z \in (x ∖ \{X F W (X)\}) \neg z W (X) y$
84		brun	$⊢ z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow (z W (X) y \lor z (X \times \{X F W (X)\}) y)$
85		idd	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (z W (X) y \to z W (X) y)$
86		brxp	$⊢ z (X \times \{X F W (X)\}) y \leftrightarrow (z \in X \land y \in \{X F W (X)\})$
87	86	simprbi	$⊢ z (X \times \{X F W (X)\}) y \to y \in \{X F W (X)\}$
88		eldifn	$⊢ y \in (x ∖ \{X F W (X)\}) \to \neg y \in \{X F W (X)\}$
89	88	adantl	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to \neg y \in \{X F W (X)\}$
90	89	pm2.21d	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (y \in \{X F W (X)\} \to z W (X) y)$
91	87 90	syl5	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (z (X \times \{X F W (X)\}) y \to z W (X) y)$
92	85 91	jaod	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to ((z W (X) y \lor z (X \times \{X F W (X)\}) y) \to z W (X) y)$
93	84 92	syl5bi	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (z (W (X) \cup (X \times \{X F W (X)\})) y \to z W (X) y)$
94	93	con3d	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (\neg z W (X) y \to \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
95	94	ralimdv	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (\forall z \in (x ∖ \{X F W (X)\}) \neg z W (X) y \to \forall z \in (x ∖ \{X F W (X)\}) \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
96		simpr	$⊢ (φ \land \neg X F W (X) \in X) \to \neg X F W (X) \in X$
97	96	ad3antrrr	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to \neg X F W (X) \in X$
98	18	ad3antrrr	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to W (X) \subseteq X \times X$
99	98	ssbrd	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to ((X F W (X)) W (X) y \to (X F W (X)) (X \times X) y)$
100		brxp	$⊢ (X F W (X)) (X \times X) y \leftrightarrow (X F W (X) \in X \land y \in X)$
101	100	simplbi	$⊢ (X F W (X)) (X \times X) y \to X F W (X) \in X$
102	99 101	syl6	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to ((X F W (X)) W (X) y \to X F W (X) \in X)$
103	97 102	mtod	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to \neg (X F W (X)) W (X) y$
104		brxp	$⊢ (X F W (X)) (X \times \{X F W (X)\}) y \leftrightarrow (X F W (X) \in X \land y \in \{X F W (X)\})$
105	104	simprbi	$⊢ (X F W (X)) (X \times \{X F W (X)\}) y \to y \in \{X F W (X)\}$
106	89 105	nsyl	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to \neg (X F W (X)) (X \times \{X F W (X)\}) y$
107		brun	$⊢ (X F W (X)) (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow ((X F W (X)) W (X) y \lor (X F W (X)) (X \times \{X F W (X)\}) y)$
108	62 107	bitrdi	$⊢ z = X F W (X) \to (z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow ((X F W (X)) W (X) y \lor (X F W (X)) (X \times \{X F W (X)\}) y))$
109	108	notbid	$⊢ z = X F W (X) \to (\neg z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \neg ((X F W (X)) W (X) y \lor (X F W (X)) (X \times \{X F W (X)\}) y))$
110	46 109	ralsn	$⊢ \forall z \in \{X F W (X)\} \neg z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow \neg ((X F W (X)) W (X) y \lor (X F W (X)) (X \times \{X F W (X)\}) y)$
111		ioran	$⊢ \neg ((X F W (X)) W (X) y \lor (X F W (X)) (X \times \{X F W (X)\}) y) \leftrightarrow (\neg (X F W (X)) W (X) y \land \neg (X F W (X)) (X \times \{X F W (X)\}) y)$
112	110 111	bitri	$⊢ \forall z \in \{X F W (X)\} \neg z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow (\neg (X F W (X)) W (X) y \land \neg (X F W (X)) (X \times \{X F W (X)\}) y)$
113	103 106 112	sylanbrc	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to \forall z \in \{X F W (X)\} \neg z (W (X) \cup (X \times \{X F W (X)\})) y$
114	95 113	jctird	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (\forall z \in (x ∖ \{X F W (X)\}) \neg z W (X) y \to (\forall z \in (x ∖ \{X F W (X)\}) \neg z (W (X) \cup (X \times \{X F W (X)\})) y \land \forall z \in \{X F W (X)\} \neg z (W (X) \cup (X \times \{X F W (X)\})) y))$
115		ssun1	$⊢ x \subseteq x \cup \{X F W (X)\}$
116		undif1	$⊢ (x ∖ \{X F W (X)\}) \cup \{X F W (X)\} = x \cup \{X F W (X)\}$
117	115 116	sseqtrri	$⊢ x \subseteq (x ∖ \{X F W (X)\}) \cup \{X F W (X)\}$
118		ralun	$⊢ (\forall z \in (x ∖ \{X F W (X)\}) \neg z (W (X) \cup (X \times \{X F W (X)\})) y \land \forall z \in \{X F W (X)\} \neg z (W (X) \cup (X \times \{X F W (X)\})) y) \to \forall z \in ((x ∖ \{X F W (X)\}) \cup \{X F W (X)\}) \neg z (W (X) \cup (X \times \{X F W (X)\})) y$
119		ssralv	$⊢ x \subseteq (x ∖ \{X F W (X)\}) \cup \{X F W (X)\} \to (\forall z \in ((x ∖ \{X F W (X)\}) \cup \{X F W (X)\}) \neg z (W (X) \cup (X \times \{X F W (X)\})) y \to \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
120	117 118 119	mpsyl	$⊢ (\forall z \in (x ∖ \{X F W (X)\}) \neg z (W (X) \cup (X \times \{X F W (X)\})) y \land \forall z \in \{X F W (X)\} \neg z (W (X) \cup (X \times \{X F W (X)\})) y) \to \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y$
121	114 120	syl6	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (\forall z \in (x ∖ \{X F W (X)\}) \neg z W (X) y \to \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
122		eldifi	$⊢ y \in (x ∖ \{X F W (X)\}) \to y \in x$
123	122	adantl	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to y \in x$
124	121 123	jctild	$⊢ ((((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \land y \in (x ∖ \{X F W (X)\})) \to (\forall z \in (x ∖ \{X F W (X)\}) \neg z W (X) y \to (y \in x \land \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y))$
125	124	expimpd	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to ((y \in (x ∖ \{X F W (X)\}) \land \forall z \in (x ∖ \{X F W (X)\}) \neg z W (X) y) \to (y \in x \land \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y))$
126	125	reximdv2	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to (\exists y \in (x ∖ \{X F W (X)\}) \forall z \in (x ∖ \{X F W (X)\}) \neg z W (X) y \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
127	83 126	mpd	$⊢ (((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \land x ∖ \{X F W (X)\} \neq \emptyset) \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y$
128	127	ex	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \to (x ∖ \{X F W (X)\} \neq \emptyset \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
129	69 128	pm2.61dne	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset)) \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y$
130	129	ex	$⊢ (φ \land \neg X F W (X) \in X) \to ((x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
131	130	alrimiv	$⊢ (φ \land \neg X F W (X) \in X) \to \forall x ((x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
132		df-fr	$⊢ (W (X) \cup (X \times \{X F W (X)\})) Fr (X \cup \{X F W (X)\}) \leftrightarrow \forall x ((x \subseteq X \cup \{X F W (X)\} \land x \neq \emptyset) \to \exists y \in x \forall z \in x \neg z (W (X) \cup (X \times \{X F W (X)\})) y)$
133	131 132	sylibr	$⊢ (φ \land \neg X F W (X) \in X) \to (W (X) \cup (X \times \{X F W (X)\})) Fr (X \cup \{X F W (X)\})$
134		elun	$⊢ x \in (X \cup \{X F W (X)\}) \leftrightarrow (x \in X \lor x \in \{X F W (X)\})$
135		elun	$⊢ y \in (X \cup \{X F W (X)\}) \leftrightarrow (y \in X \lor y \in \{X F W (X)\})$
136	134 135	anbi12i	$⊢ (x \in (X \cup \{X F W (X)\}) \land y \in (X \cup \{X F W (X)\})) \leftrightarrow ((x \in X \lor x \in \{X F W (X)\}) \land (y \in X \lor y \in \{X F W (X)\}))$
137		weso	$⊢ W (X) We X \to W (X) Or X$
138	20 137	syl	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) Or X$
139		solin	$⊢ (W (X) Or X \land (x \in X \land y \in X)) \to (x W (X) y \lor x = y \lor y W (X) x)$
140	138 139	sylan	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in X)) \to (x W (X) y \lor x = y \lor y W (X) x)$
141		ssun1	$⊢ W (X) \subseteq W (X) \cup (X \times \{X F W (X)\})$
142	141	a1i	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in X)) \to W (X) \subseteq W (X) \cup (X \times \{X F W (X)\})$
143	142	ssbrd	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in X)) \to (x W (X) y \to x (W (X) \cup (X \times \{X F W (X)\})) y)$
144		idd	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in X)) \to (x = y \to x = y)$
145	142	ssbrd	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in X)) \to (y W (X) x \to y (W (X) \cup (X \times \{X F W (X)\})) x)$
146	143 144 145	3orim123d	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in X)) \to ((x W (X) y \lor x = y \lor y W (X) x) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x))$
147	140 146	mpd	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in X)) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x)$
148	147	ex	$⊢ (φ \land \neg X F W (X) \in X) \to ((x \in X \land y \in X) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x))$
149		simpr	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in \{X F W (X)\} \land y \in X)) \to (x \in \{X F W (X)\} \land y \in X)$
150	149	ancomd	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in \{X F W (X)\} \land y \in X)) \to (y \in X \land x \in \{X F W (X)\})$
151		brxp	$⊢ y (X \times \{X F W (X)\}) x \leftrightarrow (y \in X \land x \in \{X F W (X)\})$
152	150 151	sylibr	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in \{X F W (X)\} \land y \in X)) \to y (X \times \{X F W (X)\}) x$
153		ssun2	$⊢ X \times \{X F W (X)\} \subseteq W (X) \cup (X \times \{X F W (X)\})$
154	153	ssbri	$⊢ y (X \times \{X F W (X)\}) x \to y (W (X) \cup (X \times \{X F W (X)\})) x$
155		3mix3	$⊢ y (W (X) \cup (X \times \{X F W (X)\})) x \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x)$
156	152 154 155	3syl	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in \{X F W (X)\} \land y \in X)) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x)$
157	156	ex	$⊢ (φ \land \neg X F W (X) \in X) \to ((x \in \{X F W (X)\} \land y \in X) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x))$
158		simpr	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in \{X F W (X)\})) \to (x \in X \land y \in \{X F W (X)\})$
159		brxp	$⊢ x (X \times \{X F W (X)\}) y \leftrightarrow (x \in X \land y \in \{X F W (X)\})$
160	158 159	sylibr	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in \{X F W (X)\})) \to x (X \times \{X F W (X)\}) y$
161	153	ssbri	$⊢ x (X \times \{X F W (X)\}) y \to x (W (X) \cup (X \times \{X F W (X)\})) y$
162		3mix1	$⊢ x (W (X) \cup (X \times \{X F W (X)\})) y \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x)$
163	160 161 162	3syl	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in \{X F W (X)\})) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x)$
164	163	ex	$⊢ (φ \land \neg X F W (X) \in X) \to ((x \in X \land y \in \{X F W (X)\}) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x))$
165		elsni	$⊢ x \in \{X F W (X)\} \to x = X F W (X)$
166		elsni	$⊢ y \in \{X F W (X)\} \to y = X F W (X)$
167		eqtr3	$⊢ (x = X F W (X) \land y = X F W (X)) \to x = y$
168	165 166 167	syl2an	$⊢ (x \in \{X F W (X)\} \land y \in \{X F W (X)\}) \to x = y$
169	168	3mix2d	$⊢ (x \in \{X F W (X)\} \land y \in \{X F W (X)\}) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x)$
170	169	a1i	$⊢ (φ \land \neg X F W (X) \in X) \to ((x \in \{X F W (X)\} \land y \in \{X F W (X)\}) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x))$
171	148 157 164 170	ccased	$⊢ (φ \land \neg X F W (X) \in X) \to (((x \in X \lor x \in \{X F W (X)\}) \land (y \in X \lor y \in \{X F W (X)\})) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x))$
172	136 171	syl5bi	$⊢ (φ \land \neg X F W (X) \in X) \to ((x \in (X \cup \{X F W (X)\}) \land y \in (X \cup \{X F W (X)\})) \to (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x))$
173	172	ralrimivv	$⊢ (φ \land \neg X F W (X) \in X) \to \forall x \in (X \cup \{X F W (X)\}) \forall y \in (X \cup \{X F W (X)\}) (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x)$
174		dfwe2	$⊢ (W (X) \cup (X \times \{X F W (X)\})) We (X \cup \{X F W (X)\}) \leftrightarrow ((W (X) \cup (X \times \{X F W (X)\})) Fr (X \cup \{X F W (X)\}) \land \forall x \in (X \cup \{X F W (X)\}) \forall y \in (X \cup \{X F W (X)\}) (x (W (X) \cup (X \times \{X F W (X)\})) y \lor x = y \lor y (W (X) \cup (X \times \{X F W (X)\})) x))$
175	133 173 174	sylanbrc	$⊢ (φ \land \neg X F W (X) \in X) \to (W (X) \cup (X \times \{X F W (X)\})) We (X \cup \{X F W (X)\})$
176	1	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\}] / b \underset{˙}{]} b F (s \cap (b \times b)) = z))\}$
177	176 6 13	fpwwe2lem3	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to {W (X)}^{-1} [\{y\}] F (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) = y$
178		cnvimass	$⊢ {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \subseteq dom (W (X) \cup (X \times \{X F W (X)\}))$
179		fvex	$⊢ W (X) \in V$
180		snex	$⊢ \{X F W (X)\} \in V$
181		xpexg	$⊢ (X \in dom W \land \{X F W (X)\} \in V) \to X \times \{X F W (X)\} \in V$
182	8 180 181	sylancl	$⊢ (φ \land \neg X F W (X) \in X) \to X \times \{X F W (X)\} \in V$
183		unexg	$⊢ (W (X) \in V \land X \times \{X F W (X)\} \in V) \to W (X) \cup (X \times \{X F W (X)\}) \in V$
184	179 182 183	sylancr	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) \cup (X \times \{X F W (X)\}) \in V$
185	184	dmexd	$⊢ (φ \land \neg X F W (X) \in X) \to dom (W (X) \cup (X \times \{X F W (X)\})) \in V$
186		ssexg	$⊢ ({(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \subseteq dom (W (X) \cup (X \times \{X F W (X)\})) \land dom (W (X) \cup (X \times \{X F W (X)\})) \in V) \to {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \in V$
187	178 185 186	sylancr	$⊢ (φ \land \neg X F W (X) \in X) \to {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \in V$
188	187	adantr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \in V$
189		id	$⊢ u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \to u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]$
190		simpr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to y \in X$
191		simplr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to \neg X F W (X) \in X$
192		nelne2	$⊢ (y \in X \land \neg X F W (X) \in X) \to y \neq X F W (X)$
193	190 191 192	syl2anc	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to y \neq X F W (X)$
194	87 166	syl	$⊢ z (X \times \{X F W (X)\}) y \to y = X F W (X)$
195	194	necon3ai	$⊢ y \neq X F W (X) \to \neg z (X \times \{X F W (X)\}) y$
196		biorf	$⊢ \neg z (X \times \{X F W (X)\}) y \to (z W (X) y \leftrightarrow (z (X \times \{X F W (X)\}) y \lor z W (X) y))$
197	193 195 196	3syl	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (z W (X) y \leftrightarrow (z (X \times \{X F W (X)\}) y \lor z W (X) y))$
198		orcom	$⊢ (z (X \times \{X F W (X)\}) y \lor z W (X) y) \leftrightarrow (z W (X) y \lor z (X \times \{X F W (X)\}) y)$
199	198 84	bitr4i	$⊢ (z (X \times \{X F W (X)\}) y \lor z W (X) y) \leftrightarrow z (W (X) \cup (X \times \{X F W (X)\})) y$
200	197 199	bitr2di	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (z (W (X) \cup (X \times \{X F W (X)\})) y \leftrightarrow z W (X) y)$
201		vex	$⊢ z \in V$
202	201	eliniseg	$⊢ y \in V \to (z \in {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \leftrightarrow z (W (X) \cup (X \times \{X F W (X)\})) y)$
203	202	elv	$⊢ z \in {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \leftrightarrow z (W (X) \cup (X \times \{X F W (X)\})) y$
204	201	eliniseg	$⊢ y \in V \to (z \in {W (X)}^{-1} [\{y\}] \leftrightarrow z W (X) y)$
205	204	elv	$⊢ z \in {W (X)}^{-1} [\{y\}] \leftrightarrow z W (X) y$
206	200 203 205	3bitr4g	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (z \in {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \leftrightarrow z \in {W (X)}^{-1} [\{y\}])$
207	206	eqrdv	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] = {W (X)}^{-1} [\{y\}]$
208	189 207	sylan9eqr	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in X) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to u = {W (X)}^{-1} [\{y\}]$
209	208	sqxpeqd	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in X) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to u \times u = {W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]$
210	209	ineq2d	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in X) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to (W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u) = (W (X) \cup (X \times \{X F W (X)\})) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])$
211		indir	$⊢ (W (X) \cup (X \times \{X F W (X)\})) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]) = (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) \cup ((X \times \{X F W (X)\}) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]))$
212		inxp	$⊢ (X \times \{X F W (X)\}) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]) = (X \cap {W (X)}^{-1} [\{y\}]) \times (\{X F W (X)\} \cap {W (X)}^{-1} [\{y\}])$
213		incom	$⊢ \{X F W (X)\} \cap {W (X)}^{-1} [\{y\}] = {W (X)}^{-1} [\{y\}] \cap \{X F W (X)\}$
214		cnvimass	$⊢ {W (X)}^{-1} [\{y\}] \subseteq dom W (X)$
215	18	adantr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to W (X) \subseteq X \times X$
216		dmss	$⊢ W (X) \subseteq X \times X \to dom W (X) \subseteq dom (X \times X)$
217	215 216	syl	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to dom W (X) \subseteq dom (X \times X)$
218		dmxpid	$⊢ dom (X \times X) = X$
219	217 218	sseqtrdi	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to dom W (X) \subseteq X$
220	214 219	sstrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to {W (X)}^{-1} [\{y\}] \subseteq X$
221	220 191	ssneldd	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to \neg X F W (X) \in {W (X)}^{-1} [\{y\}]$
222		disjsn	$⊢ {W (X)}^{-1} [\{y\}] \cap \{X F W (X)\} = \emptyset \leftrightarrow \neg X F W (X) \in {W (X)}^{-1} [\{y\}]$
223	221 222	sylibr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to {W (X)}^{-1} [\{y\}] \cap \{X F W (X)\} = \emptyset$
224	213 223	eqtrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to \{X F W (X)\} \cap {W (X)}^{-1} [\{y\}] = \emptyset$
225	224	xpeq2d	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (X \cap {W (X)}^{-1} [\{y\}]) \times (\{X F W (X)\} \cap {W (X)}^{-1} [\{y\}]) = (X \cap {W (X)}^{-1} [\{y\}]) \times \emptyset$
226		xp0	$⊢ (X \cap {W (X)}^{-1} [\{y\}]) \times \emptyset = \emptyset$
227	225 226	eqtrdi	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (X \cap {W (X)}^{-1} [\{y\}]) \times (\{X F W (X)\} \cap {W (X)}^{-1} [\{y\}]) = \emptyset$
228	212 227	eqtrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (X \times \{X F W (X)\}) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]) = \emptyset$
229	228	uneq2d	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) \cup ((X \times \{X F W (X)\}) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) = (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) \cup \emptyset$
230	211 229	eqtrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (W (X) \cup (X \times \{X F W (X)\})) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]) = (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) \cup \emptyset$
231		un0	$⊢ (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) \cup \emptyset = W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])$
232	230 231	eqtrdi	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (W (X) \cup (X \times \{X F W (X)\})) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]) = W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])$
233	232	adantr	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in X) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to (W (X) \cup (X \times \{X F W (X)\})) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]) = W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])$
234	210 233	eqtrd	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in X) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to (W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u) = W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])$
235	208 234	oveq12d	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in X) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = {W (X)}^{-1} [\{y\}] F (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}]))$
236	235	eqeq1d	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in X) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to (u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y \leftrightarrow {W (X)}^{-1} [\{y\}] F (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) = y)$
237	188 236	sbcied	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to (\underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y \leftrightarrow {W (X)}^{-1} [\{y\}] F (W (X) \cap ({W (X)}^{-1} [\{y\}] \times {W (X)}^{-1} [\{y\}])) = y)$
238	177 237	mpbird	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to \underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y$
239	166	adantl	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to y = X F W (X)$
240	239	eqcomd	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to X F W (X) = y$
241	187	adantr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \in V$
242		simplr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \neg X F W (X) \in X$
243	239	eleq1d	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to (y \in dom {W (X)}^{-1} \leftrightarrow X F W (X) \in dom {W (X)}^{-1})$
244	18	adantr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to W (X) \subseteq X \times X$
245		rnss	$⊢ W (X) \subseteq X \times X \to ran W (X) \subseteq ran (X \times X)$
246	244 245	syl	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to ran W (X) \subseteq ran (X \times X)$
247		df-rn	$⊢ ran W (X) = dom {W (X)}^{-1}$
248		rnxpid	$⊢ ran (X \times X) = X$
249	246 247 248	3sstr3g	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to dom {W (X)}^{-1} \subseteq X$
250	249	sseld	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to (X F W (X) \in dom {W (X)}^{-1} \to X F W (X) \in X)$
251	243 250	sylbid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to (y \in dom {W (X)}^{-1} \to X F W (X) \in X)$
252	242 251	mtod	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \neg y \in dom {W (X)}^{-1}$
253		ndmima	$⊢ \neg y \in dom {W (X)}^{-1} \to {W (X)}^{-1} [\{y\}] = \emptyset$
254	252 253	syl	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to {W (X)}^{-1} [\{y\}] = \emptyset$
255	239	sneqd	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \{y\} = \{X F W (X)\}$
256	255	imaeq2d	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to {(X \times \{X F W (X)\})}^{-1} [\{y\}] = {(X \times \{X F W (X)\})}^{-1} [\{X F W (X)\}]$
257		df-ima	$⊢ {(X \times \{X F W (X)\})}^{-1} [\{X F W (X)\}] = ran ({{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}})$
258		cnvxp	$⊢ {(X \times \{X F W (X)\})}^{-1} = \{X F W (X)\} \times X$
259	258	reseq1i	$⊢ {{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}} = {(\{X F W (X)\} \times X) ↾}_{\{X F W (X)\}}$
260		ssid	$⊢ \{X F W (X)\} \subseteq \{X F W (X)\}$
261		xpssres	$⊢ \{X F W (X)\} \subseteq \{X F W (X)\} \to {(\{X F W (X)\} \times X) ↾}_{\{X F W (X)\}} = \{X F W (X)\} \times X$
262	260 261	ax-mp	$⊢ {(\{X F W (X)\} \times X) ↾}_{\{X F W (X)\}} = \{X F W (X)\} \times X$
263	259 262	eqtri	$⊢ {{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}} = \{X F W (X)\} \times X$
264	263	rneqi	$⊢ ran ({{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}}) = ran (\{X F W (X)\} \times X)$
265	46	snnz	$⊢ \{X F W (X)\} \neq \emptyset$
266		rnxp	$⊢ \{X F W (X)\} \neq \emptyset \to ran (\{X F W (X)\} \times X) = X$
267	265 266	ax-mp	$⊢ ran (\{X F W (X)\} \times X) = X$
268	264 267	eqtri	$⊢ ran ({{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}}) = X$
269	257 268	eqtri	$⊢ {(X \times \{X F W (X)\})}^{-1} [\{X F W (X)\}] = X$
270	256 269	eqtrdi	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to {(X \times \{X F W (X)\})}^{-1} [\{y\}] = X$
271	254 270	uneq12d	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to {W (X)}^{-1} [\{y\}] \cup {(X \times \{X F W (X)\})}^{-1} [\{y\}] = \emptyset \cup X$
272		cnvun	$⊢ {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} = {W (X)}^{-1} \cup {(X \times \{X F W (X)\})}^{-1}$
273	272	imaeq1i	$⊢ {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] = ({W (X)}^{-1} \cup {(X \times \{X F W (X)\})}^{-1}) [\{y\}]$
274		imaundir	$⊢ ({W (X)}^{-1} \cup {(X \times \{X F W (X)\})}^{-1}) [\{y\}] = {W (X)}^{-1} [\{y\}] \cup {(X \times \{X F W (X)\})}^{-1} [\{y\}]$
275	273 274	eqtri	$⊢ {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] = {W (X)}^{-1} [\{y\}] \cup {(X \times \{X F W (X)\})}^{-1} [\{y\}]$
276		un0	$⊢ X \cup \emptyset = X$
277		uncom	$⊢ X \cup \emptyset = \emptyset \cup X$
278	276 277	eqtr3i	$⊢ X = \emptyset \cup X$
279	271 275 278	3eqtr4g	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] = X$
280	189 279	sylan9eqr	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to u = X$
281	280	sqxpeqd	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to u \times u = X \times X$
282	281	ineq2d	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to (W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u) = (W (X) \cup (X \times \{X F W (X)\})) \cap (X \times X)$
283		indir	$⊢ (W (X) \cup (X \times \{X F W (X)\})) \cap (X \times X) = (W (X) \cap (X \times X)) \cup ((X \times \{X F W (X)\}) \cap (X \times X))$
284		df-ss	$⊢ W (X) \subseteq X \times X \leftrightarrow W (X) \cap (X \times X) = W (X)$
285	244 284	sylib	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to W (X) \cap (X \times X) = W (X)$
286		incom	$⊢ \{X F W (X)\} \cap X = X \cap \{X F W (X)\}$
287		disjsn	$⊢ X \cap \{X F W (X)\} = \emptyset \leftrightarrow \neg X F W (X) \in X$
288	242 287	sylibr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to X \cap \{X F W (X)\} = \emptyset$
289	286 288	eqtrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \{X F W (X)\} \cap X = \emptyset$
290	289	xpeq2d	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to X \times (\{X F W (X)\} \cap X) = X \times \emptyset$
291		xpindi	$⊢ X \times (\{X F W (X)\} \cap X) = (X \times \{X F W (X)\}) \cap (X \times X)$
292		xp0	$⊢ X \times \emptyset = \emptyset$
293	290 291 292	3eqtr3g	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to (X \times \{X F W (X)\}) \cap (X \times X) = \emptyset$
294	285 293	uneq12d	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to (W (X) \cap (X \times X)) \cup ((X \times \{X F W (X)\}) \cap (X \times X)) = W (X) \cup \emptyset$
295	283 294	eqtrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to (W (X) \cup (X \times \{X F W (X)\})) \cap (X \times X) = W (X) \cup \emptyset$
296		un0	$⊢ W (X) \cup \emptyset = W (X)$
297	295 296	eqtrdi	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to (W (X) \cup (X \times \{X F W (X)\})) \cap (X \times X) = W (X)$
298	297	adantr	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to (W (X) \cup (X \times \{X F W (X)\})) \cap (X \times X) = W (X)$
299	282 298	eqtrd	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to (W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u) = W (X)$
300	280 299	oveq12d	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = X F W (X)$
301	300	eqeq1d	$⊢ (((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \land u = {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}]) \to (u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y \leftrightarrow X F W (X) = y)$
302	241 301	sbcied	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to (\underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y \leftrightarrow X F W (X) = y)$
303	240 302	mpbird	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y$
304	238 303	jaodan	$⊢ ((φ \land \neg X F W (X) \in X) \land (y \in X \lor y \in \{X F W (X)\})) \to \underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y$
305	135 304	sylan2b	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in (X \cup \{X F W (X)\})) \to \underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y$
306	305	ralrimiva	$⊢ (φ \land \neg X F W (X) \in X) \to \forall y \in (X \cup \{X F W (X)\}) \underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y$
307	175 306	jca	$⊢ (φ \land \neg X F W (X) \in X) \to ((W (X) \cup (X \times \{X F W (X)\})) We (X \cup \{X F W (X)\}) \land \forall y \in (X \cup \{X F W (X)\}) \underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y)$
308	1 2	fpwwe2lem2	$⊢ φ \to ((X \cup \{X F W (X)\}) W (W (X) \cup (X \times \{X F W (X)\})) \leftrightarrow ((X \cup \{X F W (X)\} \subseteq A \land W (X) \cup (X \times \{X F W (X)\}) \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})) \land ((W (X) \cup (X \times \{X F W (X)\})) We (X \cup \{X F W (X)\}) \land \forall y \in (X \cup \{X F W (X)\}) \underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y)))$
309	308	adantr	$⊢ (φ \land \neg X F W (X) \in X) \to ((X \cup \{X F W (X)\}) W (W (X) \cup (X \times \{X F W (X)\})) \leftrightarrow ((X \cup \{X F W (X)\} \subseteq A \land W (X) \cup (X \times \{X F W (X)\}) \subseteq (X \cup \{X F W (X)\}) \times (X \cup \{X F W (X)\})) \land ((W (X) \cup (X \times \{X F W (X)\})) We (X \cup \{X F W (X)\}) \land \forall y \in (X \cup \{X F W (X)\}) \underset{˙}{[} {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] / u \underset{˙}{]} u F ((W (X) \cup (X \times \{X F W (X)\})) \cap (u \times u)) = y)))$
310	34 307 309	mpbir2and	$⊢ (φ \land \neg X F W (X) \in X) \to (X \cup \{X F W (X)\}) W (W (X) \cup (X \times \{X F W (X)\}))$
311	1	relopabiv	$⊢ Rel W$
312	311	releldmi	$⊢ (X \cup \{X F W (X)\}) W (W (X) \cup (X \times \{X F W (X)\})) \to X \cup \{X F W (X)\} \in dom W$
313		elssuni	$⊢ X \cup \{X F W (X)\} \in dom W \to X \cup \{X F W (X)\} \subseteq ⋃ dom W$
314	310 312 313	3syl	$⊢ (φ \land \neg X F W (X) \in X) \to X \cup \{X F W (X)\} \subseteq ⋃ dom W$
315	314 4	sseqtrrdi	$⊢ (φ \land \neg X F W (X) \in X) \to X \cup \{X F W (X)\} \subseteq X$
316	5 315	sstrid	$⊢ (φ \land \neg X F W (X) \in X) \to \{X F W (X)\} \subseteq X$
317	46	snss	$⊢ X F W (X) \in X \leftrightarrow \{X F W (X)\} \subseteq X$
318	316 317	sylibr	$⊢ (φ \land \neg X F W (X) \in X) \to X F W (X) \in X$
319	318	pm2.18da	$⊢ φ \to X F W (X) \in X$

Metamath Proof Explorer

Theorem fpwwe2lem12

Proof