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		sssn	$⊢ x \subseteq \{X F W (X)\} \leftrightarrow (x = \emptyset \lor x = \{X F W (X)\})$
56	55	bilani	$⊢ (((φ \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)\})$
57		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$
58	57	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$
59	56 58	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)\}$
60	59	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)$
61		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)$
62	61	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)$
63	46 62	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$
64	60 63	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)$
65	59 64	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)$
66	54 65	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$
67	66	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)$
68	35 67	biimtrrid	$⊢ ((φ \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)$
69		vex	$⊢ x \in V$
70		difexg	$⊢ x \in V \to x ∖ \{X F W (X)\} \in V$
71	69 70	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$
72		wefr	$⊢ W (X) We X \to W (X) Fr X$
73	20 72	syl	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) Fr X$
74	73	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$
75		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)\}$
76		uncom	$⊢ X \cup \{X F W (X)\} = \{X F W (X)\} \cup X$
77	75 76	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$
78		ssundif	$⊢ x \subseteq \{X F W (X)\} \cup X \leftrightarrow x ∖ \{X F W (X)\} \subseteq X$
79	77 78	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$
80		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$
81		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$
82	71 74 79 80 81	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$
83		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)$
84		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)$
85		brxp	$⊢ z (X \times \{X F W (X)\}) y \leftrightarrow (z \in X \land y \in \{X F W (X)\})$
86	85	simprbi	$⊢ z (X \times \{X F W (X)\}) y \to y \in \{X F W (X)\}$
87		eldifn	$⊢ y \in (x ∖ \{X F W (X)\}) \to \neg y \in \{X F W (X)\}$
88	87	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)\}$
89	88	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)$
90	86 89	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)$
91	84 90	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)$
92	83 91	biimtrid	$⊢ ((((φ \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)$
93	92	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)$
94	93	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)$
95		simpr	$⊢ (φ \land \neg X F W (X) \in X) \to \neg X F W (X) \in X$
96	95	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$
97	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$
98	97	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)$
99		brxp	$⊢ (X F W (X)) (X \times X) y \leftrightarrow (X F W (X) \in X \land y \in X)$
100	99	simplbi	$⊢ (X F W (X)) (X \times X) y \to X F W (X) \in X$
101	98 100	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)$
102	96 101	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$
103		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)\})$
104	103	simprbi	$⊢ (X F W (X)) (X \times \{X F W (X)\}) y \to y \in \{X F W (X)\}$
105	88 104	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$
106		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)$
107	61 106	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))$
108	107	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))$
109	46 108	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)$
110		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)$
111	109 110	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)$
112	102 105 111	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$
113	94 112	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))$
114		ssun1	$⊢ x \subseteq x \cup \{X F W (X)\}$
115		undif1	$⊢ (x ∖ \{X F W (X)\}) \cup \{X F W (X)\} = x \cup \{X F W (X)\}$
116	114 115	sseqtrri	$⊢ x \subseteq (x ∖ \{X F W (X)\}) \cup \{X F W (X)\}$
117		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$
118		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)$
119	116 117 118	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$
120	113 119	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)$
121		eldifi	$⊢ y \in (x ∖ \{X F W (X)\}) \to y \in x$
122	121	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$
123	120 122	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))$
124	123	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))$
125	124	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)$
126	82 125	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$
127	126	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)$
128	68 127	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$
129	128	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)$
130	129	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)$
131		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)$
132	130 131	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)\})$
133		elun	$⊢ x \in (X \cup \{X F W (X)\}) \leftrightarrow (x \in X \lor x \in \{X F W (X)\})$
134		elun	$⊢ y \in (X \cup \{X F W (X)\}) \leftrightarrow (y \in X \lor y \in \{X F W (X)\})$
135	133 134	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)\}))$
136		weso	$⊢ W (X) We X \to W (X) Or X$
137	20 136	syl	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) Or X$
138		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)$
139	137 138	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)$
140		ssun1	$⊢ W (X) \subseteq W (X) \cup (X \times \{X F W (X)\})$
141	140	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)\})$
142	141	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)$
143		idd	$⊢ ((φ \land \neg X F W (X) \in X) \land (x \in X \land y \in X)) \to (x = y \to x = y)$
144	141	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)$
145	142 143 144	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))$
146	139 145	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)$
147	146	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))$
148		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)$
149	148	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)\})$
150		brxp	$⊢ y (X \times \{X F W (X)\}) x \leftrightarrow (y \in X \land x \in \{X F W (X)\})$
151	149 150	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$
152		ssun2	$⊢ X \times \{X F W (X)\} \subseteq W (X) \cup (X \times \{X F W (X)\})$
153	152	ssbri	$⊢ y (X \times \{X F W (X)\}) x \to y (W (X) \cup (X \times \{X F W (X)\})) x$
154		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)$
155	151 153 154	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)$
156	155	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))$
157		brxp	$⊢ x (X \times \{X F W (X)\}) y \leftrightarrow (x \in X \land y \in \{X F W (X)\})$
158	157	bilanri	$⊢ ((φ \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$
159	152	ssbri	$⊢ x (X \times \{X F W (X)\}) y \to x (W (X) \cup (X \times \{X F W (X)\})) y$
160		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)$
161	158 159 160	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)$
162	161	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))$
163		elsni	$⊢ x \in \{X F W (X)\} \to x = X F W (X)$
164		elsni	$⊢ y \in \{X F W (X)\} \to y = X F W (X)$
165		eqtr3	$⊢ (x = X F W (X) \land y = X F W (X)) \to x = y$
166	163 164 165	syl2an	$⊢ (x \in \{X F W (X)\} \land y \in \{X F W (X)\}) \to x = y$
167	166	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)$
168	167	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))$
169	147 156 162 168	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))$
170	135 169	biimtrid	$⊢ (φ \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))$
171	170	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)$
172		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))$
173	132 171 172	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)\})$
174	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))\}$
175	174 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$
176		cnvimass	$⊢ {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \subseteq dom (W (X) \cup (X \times \{X F W (X)\}))$
177		fvex	$⊢ W (X) \in V$
178		snex	$⊢ \{X F W (X)\} \in V$
179		xpexg	$⊢ (X \in dom W \land \{X F W (X)\} \in V) \to X \times \{X F W (X)\} \in V$
180	8 178 179	sylancl	$⊢ (φ \land \neg X F W (X) \in X) \to X \times \{X F W (X)\} \in V$
181		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$
182	177 180 181	sylancr	$⊢ (φ \land \neg X F W (X) \in X) \to W (X) \cup (X \times \{X F W (X)\}) \in V$
183	182	dmexd	$⊢ (φ \land \neg X F W (X) \in X) \to dom (W (X) \cup (X \times \{X F W (X)\})) \in V$
184		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$
185	176 183 184	sylancr	$⊢ (φ \land \neg X F W (X) \in X) \to {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] \in V$
186	185	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$
187		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\}]$
188		simpr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to y \in X$
189		simplr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to \neg X F W (X) \in X$
190		nelne2	$⊢ (y \in X \land \neg X F W (X) \in X) \to y \neq X F W (X)$
191	188 189 190	syl2anc	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to y \neq X F W (X)$
192	86 164	syl	$⊢ z (X \times \{X F W (X)\}) y \to y = X F W (X)$
193	192	necon3ai	$⊢ y \neq X F W (X) \to \neg z (X \times \{X F W (X)\}) y$
194		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))$
195	191 193 194	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))$
196		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)$
197	196 83	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$
198	195 197	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)$
199		vex	$⊢ z \in V$
200	199	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)$
201	200	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$
202	199	eliniseg	$⊢ y \in V \to (z \in {W (X)}^{-1} [\{y\}] \leftrightarrow z W (X) y)$
203	202	elv	$⊢ z \in {W (X)}^{-1} [\{y\}] \leftrightarrow z W (X) y$
204	198 201 203	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\}])$
205	204	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\}]$
206	187 205	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\}]$
207	206	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\}]$
208	207	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\}])$
209		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\}]))$
210		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\}])$
211		incom	$⊢ \{X F W (X)\} \cap {W (X)}^{-1} [\{y\}] = {W (X)}^{-1} [\{y\}] \cap \{X F W (X)\}$
212		cnvimass	$⊢ {W (X)}^{-1} [\{y\}] \subseteq dom W (X)$
213	18	adantr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to W (X) \subseteq X \times X$
214		dmss	$⊢ W (X) \subseteq X \times X \to dom W (X) \subseteq dom (X \times X)$
215	213 214	syl	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to dom W (X) \subseteq dom (X \times X)$
216		dmxpid	$⊢ dom (X \times X) = X$
217	215 216	sseqtrdi	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to dom W (X) \subseteq X$
218	212 217	sstrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to {W (X)}^{-1} [\{y\}] \subseteq X$
219	218 189	ssneldd	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to \neg X F W (X) \in {W (X)}^{-1} [\{y\}]$
220		disjsn	$⊢ {W (X)}^{-1} [\{y\}] \cap \{X F W (X)\} = \emptyset \leftrightarrow \neg X F W (X) \in {W (X)}^{-1} [\{y\}]$
221	219 220	sylibr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to {W (X)}^{-1} [\{y\}] \cap \{X F W (X)\} = \emptyset$
222	211 221	eqtrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in X) \to \{X F W (X)\} \cap {W (X)}^{-1} [\{y\}] = \emptyset$
223	222	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$
224		xp0	$⊢ (X \cap {W (X)}^{-1} [\{y\}]) \times \emptyset = \emptyset$
225	223 224	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$
226	210 225	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$
227	226	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$
228	209 227	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$
229		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\}])$
230	228 229	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\}])$
231	230	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\}])$
232	208 231	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\}])$
233	206 232	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\}]))$
234	233	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)$
235	186 234	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)$
236	175 235	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$
237	164	adantl	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to y = X F W (X)$
238	237	eqcomd	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to X F W (X) = y$
239	185	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$
240		simplr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \neg X F W (X) \in X$
241	237	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})$
242	18	adantr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to W (X) \subseteq X \times X$
243		rnss	$⊢ W (X) \subseteq X \times X \to ran W (X) \subseteq ran (X \times X)$
244	242 243	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)$
245		df-rn	$⊢ ran W (X) = dom {W (X)}^{-1}$
246		rnxpid	$⊢ ran (X \times X) = X$
247	244 245 246	3sstr3g	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to dom {W (X)}^{-1} \subseteq X$
248	247	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)$
249	241 248	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)$
250	240 249	mtod	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \neg y \in dom {W (X)}^{-1}$
251		ndmima	$⊢ \neg y \in dom {W (X)}^{-1} \to {W (X)}^{-1} [\{y\}] = \emptyset$
252	250 251	syl	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to {W (X)}^{-1} [\{y\}] = \emptyset$
253	237	sneqd	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \{y\} = \{X F W (X)\}$
254	253	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)\}]$
255		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)\}})$
256		cnvxp	$⊢ {(X \times \{X F W (X)\})}^{-1} = \{X F W (X)\} \times X$
257	256	reseq1i	$⊢ {{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}} = {(\{X F W (X)\} \times X) ↾}_{\{X F W (X)\}}$
258		ssid	$⊢ \{X F W (X)\} \subseteq \{X F W (X)\}$
259		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$
260	258 259	ax-mp	$⊢ {(\{X F W (X)\} \times X) ↾}_{\{X F W (X)\}} = \{X F W (X)\} \times X$
261	257 260	eqtri	$⊢ {{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}} = \{X F W (X)\} \times X$
262	261	rneqi	$⊢ ran ({{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}}) = ran (\{X F W (X)\} \times X)$
263	46	snnz	$⊢ \{X F W (X)\} \neq \emptyset$
264		rnxp	$⊢ \{X F W (X)\} \neq \emptyset \to ran (\{X F W (X)\} \times X) = X$
265	263 264	ax-mp	$⊢ ran (\{X F W (X)\} \times X) = X$
266	262 265	eqtri	$⊢ ran ({{(X \times \{X F W (X)\})}^{-1} ↾}_{\{X F W (X)\}}) = X$
267	255 266	eqtri	$⊢ {(X \times \{X F W (X)\})}^{-1} [\{X F W (X)\}] = X$
268	254 267	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$
269	252 268	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$
270		cnvun	$⊢ {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} = {W (X)}^{-1} \cup {(X \times \{X F W (X)\})}^{-1}$
271	270	imaeq1i	$⊢ {(W (X) \cup (X \times \{X F W (X)\}))}^{-1} [\{y\}] = ({W (X)}^{-1} \cup {(X \times \{X F W (X)\})}^{-1}) [\{y\}]$
272		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\}]$
273	271 272	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\}]$
274		un0	$⊢ X \cup \emptyset = X$
275		uncom	$⊢ X \cup \emptyset = \emptyset \cup X$
276	274 275	eqtr3i	$⊢ X = \emptyset \cup X$
277	269 273 276	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$
278	187 277	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$
279	278	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$
280	279	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)$
281		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))$
282		dfss2	$⊢ W (X) \subseteq X \times X \leftrightarrow W (X) \cap (X \times X) = W (X)$
283	242 282	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)$
284		incom	$⊢ \{X F W (X)\} \cap X = X \cap \{X F W (X)\}$
285		disjsn	$⊢ X \cap \{X F W (X)\} = \emptyset \leftrightarrow \neg X F W (X) \in X$
286	240 285	sylibr	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to X \cap \{X F W (X)\} = \emptyset$
287	284 286	eqtrid	$⊢ ((φ \land \neg X F W (X) \in X) \land y \in \{X F W (X)\}) \to \{X F W (X)\} \cap X = \emptyset$
288	287	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$
289		xpindi	$⊢ X \times (\{X F W (X)\} \cap X) = (X \times \{X F W (X)\}) \cap (X \times X)$
290		xp0	$⊢ X \times \emptyset = \emptyset$
291	288 289 290	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$
292	283 291	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$
293	281 292	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$
294		un0	$⊢ W (X) \cup \emptyset = W (X)$
295	293 294	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)$
296	295	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)$
297	280 296	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)$
298	278 297	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)$
299	298	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)$
300	239 299	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)$
301	238 300	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$
302	236 301	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$
303	134 302	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$
304	303	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$
305	173 304	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)$
306	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)))$
307	306	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)))$
308	34 305 307	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)\}))$
309	1	relopabiv	$⊢ Rel W$
310	309	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$
311		elssuni	$⊢ X \cup \{X F W (X)\} \in dom W \to X \cup \{X F W (X)\} \subseteq ⋃ dom W$
312	308 310 311	3syl	$⊢ (φ \land \neg X F W (X) \in X) \to X \cup \{X F W (X)\} \subseteq ⋃ dom W$
313	312 4	sseqtrrdi	$⊢ (φ \land \neg X F W (X) \in X) \to X \cup \{X F W (X)\} \subseteq X$
314	5 313	sstrid	$⊢ (φ \land \neg X F W (X) \in X) \to \{X F W (X)\} \subseteq X$
315	46	snss	$⊢ X F W (X) \in X \leftrightarrow \{X F W (X)\} \subseteq X$
316	314 315	sylibr	$⊢ (φ \land \neg X F W (X) \in X) \to X F W (X) \in X$
317	316	pm2.18da	$⊢ φ \to X F W (X) \in X$

Metamath Proof Explorer

Theorem fpwwe2lem12

Proof