fpwwe2lem12

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 18-May-2015) (Proof shortened by Peter Mazsa, 23-Sep-2022)

	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 \in dom W$

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		vex	$⊢ a \in V$
6	5	eldm	$⊢ a \in dom W \leftrightarrow \exists s a W s$
7	1 2	fpwwe2lem2	$⊢ φ \to (a W s \leftrightarrow ((a \subseteq A \land s \subseteq a \times a) \land (s We a \land \forall y \in a \underset{˙}{[} s^{-1} [\{y\}] / u \underset{˙}{]} u F (s \cap (u \times u)) = y)))$
8	7	simprbda	$⊢ (φ \land a W s) \to (a \subseteq A \land s \subseteq a \times a)$
9	8	simpld	$⊢ (φ \land a W s) \to a \subseteq A$
10		velpw	$⊢ a \in 𝒫 A \leftrightarrow a \subseteq A$
11	9 10	sylibr	$⊢ (φ \land a W s) \to a \in 𝒫 A$
12	11	ex	$⊢ φ \to (a W s \to a \in 𝒫 A)$
13	12	exlimdv	$⊢ φ \to (\exists s a W s \to a \in 𝒫 A)$
14	6 13	syl5bi	$⊢ φ \to (a \in dom W \to a \in 𝒫 A)$
15	14	ssrdv	$⊢ φ \to dom W \subseteq 𝒫 A$
16		sspwuni	$⊢ dom W \subseteq 𝒫 A \leftrightarrow ⋃ dom W \subseteq A$
17	15 16	sylib	$⊢ φ \to ⋃ dom W \subseteq A$
18	4 17	eqsstrid	$⊢ φ \to X \subseteq A$
19		vex	$⊢ s \in V$
20	19	elrn	$⊢ s \in ran W \leftrightarrow \exists a a W s$
21	8	simprd	$⊢ (φ \land a W s) \to s \subseteq a \times a$
22	1	relopabi	$⊢ Rel W$
23	22	releldmi	$⊢ a W s \to a \in dom W$
24	23	adantl	$⊢ (φ \land a W s) \to a \in dom W$
25		elssuni	$⊢ a \in dom W \to a \subseteq ⋃ dom W$
26	24 25	syl	$⊢ (φ \land a W s) \to a \subseteq ⋃ dom W$
27	26 4	sseqtrrdi	$⊢ (φ \land a W s) \to a \subseteq X$
28		xpss12	$⊢ (a \subseteq X \land a \subseteq X) \to a \times a \subseteq X \times X$
29	27 27 28	syl2anc	$⊢ (φ \land a W s) \to a \times a \subseteq X \times X$
30	21 29	sstrd	$⊢ (φ \land a W s) \to s \subseteq X \times X$
31		velpw	$⊢ s \in 𝒫 (X \times X) \leftrightarrow s \subseteq X \times X$
32	30 31	sylibr	$⊢ (φ \land a W s) \to s \in 𝒫 (X \times X)$
33	32	ex	$⊢ φ \to (a W s \to s \in 𝒫 (X \times X))$
34	33	exlimdv	$⊢ φ \to (\exists a a W s \to s \in 𝒫 (X \times X))$
35	20 34	syl5bi	$⊢ φ \to (s \in ran W \to s \in 𝒫 (X \times X))$
36	35	ssrdv	$⊢ φ \to ran W \subseteq 𝒫 (X \times X)$
37		sspwuni	$⊢ ran W \subseteq 𝒫 (X \times X) \leftrightarrow ⋃ ran W \subseteq X \times X$
38	36 37	sylib	$⊢ φ \to ⋃ ran W \subseteq X \times X$
39	18 38	jca	$⊢ φ \to (X \subseteq A \land ⋃ ran W \subseteq X \times X)$
40		n0	$⊢ n \neq \emptyset \leftrightarrow \exists y y \in n$
41		ssel2	$⊢ (n \subseteq X \land y \in n) \to y \in X$
42	41	adantl	$⊢ (φ \land (n \subseteq X \land y \in n)) \to y \in X$
43	4	eleq2i	$⊢ y \in X \leftrightarrow y \in ⋃ dom W$
44		eluni2	$⊢ y \in ⋃ dom W \leftrightarrow \exists a \in dom W y \in a$
45	43 44	bitri	$⊢ y \in X \leftrightarrow \exists a \in dom W y \in a$
46	42 45	sylib	$⊢ (φ \land (n \subseteq X \land y \in n)) \to \exists a \in dom W y \in a$
47	5	inex2	$⊢ n \cap a \in V$
48	47	a1i	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to n \cap a \in V$
49	7	simplbda	$⊢ (φ \land a W s) \to (s We a \land \forall y \in a \underset{˙}{[} s^{-1} [\{y\}] / u \underset{˙}{]} u F (s \cap (u \times u)) = y)$
50	49	simpld	$⊢ (φ \land a W s) \to s We a$
51	50	ad2ant2r	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to s We a$
52		wefr	$⊢ s We a \to s Fr a$
53	51 52	syl	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to s Fr a$
54		inss2	$⊢ n \cap a \subseteq a$
55	54	a1i	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to n \cap a \subseteq a$
56		simplrr	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to y \in n$
57		simprr	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to y \in a$
58		inelcm	$⊢ (y \in n \land y \in a) \to n \cap a \neq \emptyset$
59	56 57 58	syl2anc	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to n \cap a \neq \emptyset$
60		fri	$⊢ ((n \cap a \in V \land s Fr a) \land (n \cap a \subseteq a \land n \cap a \neq \emptyset)) \to \exists v \in (n \cap a) \forall z \in (n \cap a) \neg z s v$
61	48 53 55 59 60	syl22anc	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to \exists v \in (n \cap a) \forall z \in (n \cap a) \neg z s v$
62		simprl	$⊢ (((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \to v \in (n \cap a)$
63	62	elin1d	$⊢ (((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \to v \in n$
64		simplrr	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land w \in n) \to \forall z \in (n \cap a) \neg z s v$
65		ralnex	$⊢ \forall z \in (n \cap a) \neg z s v \leftrightarrow \neg \exists z \in (n \cap a) z s v$
66	64 65	sylib	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land w \in n) \to \neg \exists z \in (n \cap a) z s v$
67		df-br	$⊢ w ⋃ ran W v \leftrightarrow ⟨w, v⟩ \in ⋃ ran W$
68		eluni2	$⊢ ⟨w, v⟩ \in ⋃ ran W \leftrightarrow \exists t \in ran W ⟨w, v⟩ \in t$
69	67 68	bitri	$⊢ w ⋃ ran W v \leftrightarrow \exists t \in ran W ⟨w, v⟩ \in t$
70		vex	$⊢ t \in V$
71	70	elrn	$⊢ t \in ran W \leftrightarrow \exists b b W t$
72		df-br	$⊢ w t v \leftrightarrow ⟨w, v⟩ \in t$
73		simprll	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to w \in n$
74	73	adantr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w \in n$
75		simprr	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to w t v$
76		simp-4l	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to φ$
77		simprl	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to a W s$
78	77	ad2antrr	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to a W s$
79		simprlr	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to b W t$
80		simprr	$⊢ (φ \land (a W s \land b W t)) \to b W t$
81	1 2	fpwwe2lem2	$⊢ φ \to (b W t \leftrightarrow ((b \subseteq A \land t \subseteq b \times b) \land (t We b \land \forall y \in b \underset{˙}{[} t^{-1} [\{y\}] / u \underset{˙}{]} u F (t \cap (u \times u)) = y)))$
82	81	adantr	$⊢ (φ \land (a W s \land b W t)) \to (b W t \leftrightarrow ((b \subseteq A \land t \subseteq b \times b) \land (t We b \land \forall y \in b \underset{˙}{[} t^{-1} [\{y\}] / u \underset{˙}{]} u F (t \cap (u \times u)) = y)))$
83	80 82	mpbid	$⊢ (φ \land (a W s \land b W t)) \to ((b \subseteq A \land t \subseteq b \times b) \land (t We b \land \forall y \in b \underset{˙}{[} t^{-1} [\{y\}] / u \underset{˙}{]} u F (t \cap (u \times u)) = y))$
84	83	simpld	$⊢ (φ \land (a W s \land b W t)) \to (b \subseteq A \land t \subseteq b \times b)$
85	84	simprd	$⊢ (φ \land (a W s \land b W t)) \to t \subseteq b \times b$
86	76 78 79 85	syl12anc	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to t \subseteq b \times b$
87	86	ssbrd	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to (w t v \to w (b \times b) v)$
88	75 87	mpd	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to w (b \times b) v$
89		brxp	$⊢ w (b \times b) v \leftrightarrow (w \in b \land v \in b)$
90	89	simplbi	$⊢ w (b \times b) v \to w \in b$
91	88 90	syl	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to w \in b$
92	91	adantr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w \in b$
93	62	elin2d	$⊢ (((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \to v \in a$
94	93	ad2antrr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to v \in a$
95		simplrr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w t v$
96		brinxp2	$⊢ w (t \cap (b \times a)) v \leftrightarrow ((w \in b \land v \in a) \land w t v)$
97	92 94 95 96	syl21anbrc	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w (t \cap (b \times a)) v$
98		simprr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to s = t \cap (b \times a)$
99	98	breqd	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (w s v \leftrightarrow w (t \cap (b \times a)) v)$
100	97 99	mpbird	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w s v$
101	76 78 21	syl2anc	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to s \subseteq a \times a$
102	101	adantr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to s \subseteq a \times a$
103	102	ssbrd	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (w s v \to w (a \times a) v)$
104	100 103	mpd	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w (a \times a) v$
105		brxp	$⊢ w (a \times a) v \leftrightarrow (w \in a \land v \in a)$
106	105	simplbi	$⊢ w (a \times a) v \to w \in a$
107	104 106	syl	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w \in a$
108	74 107	elind	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w \in (n \cap a)$
109		breq1	$⊢ z = w \to (z s v \leftrightarrow w s v)$
110	109	rspcev	$⊢ (w \in (n \cap a) \land w s v) \to \exists z \in (n \cap a) z s v$
111	108 100 110	syl2anc	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (a \subseteq b \land s = t \cap (b \times a))) \to \exists z \in (n \cap a) z s v$
112	73	adantr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to w \in n$
113		simprl	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to b \subseteq a$
114	91	adantr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to w \in b$
115	113 114	sseldd	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to w \in a$
116	112 115	elind	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to w \in (n \cap a)$
117		simplrr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to w t v$
118		simprr	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to t = s \cap (a \times b)$
119		inss1	$⊢ s \cap (a \times b) \subseteq s$
120	118 119	eqsstrdi	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to t \subseteq s$
121	120	ssbrd	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to (w t v \to w s v)$
122	117 121	mpd	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to w s v$
123	116 122 110	syl2anc	$⊢ (((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \land (b \subseteq a \land t = s \cap (a \times b))) \to \exists z \in (n \cap a) z s v$
124	2	adantr	$⊢ (φ \land (a W s \land b W t)) \to A \in V$
125	3	adantlr	$⊢ ((φ \land (a W s \land b W t)) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
126		simprl	$⊢ (φ \land (a W s \land b W t)) \to a W s$
127	1 124 125 126 80	fpwwe2lem10	$⊢ (φ \land (a W s \land b W t)) \to ((a \subseteq b \land s = t \cap (b \times a)) \lor (b \subseteq a \land t = s \cap (a \times b)))$
128	76 78 79 127	syl12anc	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to ((a \subseteq b \land s = t \cap (b \times a)) \lor (b \subseteq a \land t = s \cap (a \times b)))$
129	111 123 128	mpjaodan	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land ((w \in n \land b W t) \land w t v)) \to \exists z \in (n \cap a) z s v$
130	129	expr	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land (w \in n \land b W t)) \to (w t v \to \exists z \in (n \cap a) z s v)$
131	72 130	syl5bir	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land (w \in n \land b W t)) \to (⟨w, v⟩ \in t \to \exists z \in (n \cap a) z s v)$
132	131	expr	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land w \in n) \to (b W t \to (⟨w, v⟩ \in t \to \exists z \in (n \cap a) z s v))$
133	132	exlimdv	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land w \in n) \to (\exists b b W t \to (⟨w, v⟩ \in t \to \exists z \in (n \cap a) z s v))$
134	71 133	syl5bi	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land w \in n) \to (t \in ran W \to (⟨w, v⟩ \in t \to \exists z \in (n \cap a) z s v))$
135	134	rexlimdv	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land w \in n) \to (\exists t \in ran W ⟨w, v⟩ \in t \to \exists z \in (n \cap a) z s v)$
136	69 135	syl5bi	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land w \in n) \to (w ⋃ ran W v \to \exists z \in (n \cap a) z s v)$
137	66 136	mtod	$⊢ ((((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \land w \in n) \to \neg w ⋃ ran W v$
138	137	ralrimiva	$⊢ (((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \land (v \in (n \cap a) \land \forall z \in (n \cap a) \neg z s v)) \to \forall w \in n \neg w ⋃ ran W v$
139	61 63 138	reximssdv	$⊢ ((φ \land (n \subseteq X \land y \in n)) \land (a W s \land y \in a)) \to \exists v \in n \forall w \in n \neg w ⋃ ran W v$
140	139	exp32	$⊢ (φ \land (n \subseteq X \land y \in n)) \to (a W s \to (y \in a \to \exists v \in n \forall w \in n \neg w ⋃ ran W v))$
141	140	exlimdv	$⊢ (φ \land (n \subseteq X \land y \in n)) \to (\exists s a W s \to (y \in a \to \exists v \in n \forall w \in n \neg w ⋃ ran W v))$
142	6 141	syl5bi	$⊢ (φ \land (n \subseteq X \land y \in n)) \to (a \in dom W \to (y \in a \to \exists v \in n \forall w \in n \neg w ⋃ ran W v))$
143	142	rexlimdv	$⊢ (φ \land (n \subseteq X \land y \in n)) \to (\exists a \in dom W y \in a \to \exists v \in n \forall w \in n \neg w ⋃ ran W v)$
144	46 143	mpd	$⊢ (φ \land (n \subseteq X \land y \in n)) \to \exists v \in n \forall w \in n \neg w ⋃ ran W v$
145	144	expr	$⊢ (φ \land n \subseteq X) \to (y \in n \to \exists v \in n \forall w \in n \neg w ⋃ ran W v)$
146	145	exlimdv	$⊢ (φ \land n \subseteq X) \to (\exists y y \in n \to \exists v \in n \forall w \in n \neg w ⋃ ran W v)$
147	40 146	syl5bi	$⊢ (φ \land n \subseteq X) \to (n \neq \emptyset \to \exists v \in n \forall w \in n \neg w ⋃ ran W v)$
148	147	expimpd	$⊢ φ \to ((n \subseteq X \land n \neq \emptyset) \to \exists v \in n \forall w \in n \neg w ⋃ ran W v)$
149	148	alrimiv	$⊢ φ \to \forall n ((n \subseteq X \land n \neq \emptyset) \to \exists v \in n \forall w \in n \neg w ⋃ ran W v)$
150		df-fr	$⊢ ⋃ ran W Fr X \leftrightarrow \forall n ((n \subseteq X \land n \neq \emptyset) \to \exists v \in n \forall w \in n \neg w ⋃ ran W v)$
151	149 150	sylibr	$⊢ φ \to ⋃ ran W Fr X$
152	4	eleq2i	$⊢ w \in X \leftrightarrow w \in ⋃ dom W$
153		eluni2	$⊢ w \in ⋃ dom W \leftrightarrow \exists b \in dom W w \in b$
154	152 153	bitri	$⊢ w \in X \leftrightarrow \exists b \in dom W w \in b$
155	45 154	anbi12i	$⊢ (y \in X \land w \in X) \leftrightarrow (\exists a \in dom W y \in a \land \exists b \in dom W w \in b)$
156		reeanv	$⊢ \exists a \in dom W \exists b \in dom W (y \in a \land w \in b) \leftrightarrow (\exists a \in dom W y \in a \land \exists b \in dom W w \in b)$
157	155 156	bitr4i	$⊢ (y \in X \land w \in X) \leftrightarrow \exists a \in dom W \exists b \in dom W (y \in a \land w \in b)$
158		vex	$⊢ b \in V$
159	158	eldm	$⊢ b \in dom W \leftrightarrow \exists t b W t$
160	6 159	anbi12i	$⊢ (a \in dom W \land b \in dom W) \leftrightarrow (\exists s a W s \land \exists t b W t)$
161		exdistrv	$⊢ \exists s \exists t (a W s \land b W t) \leftrightarrow (\exists s a W s \land \exists t b W t)$
162	160 161	bitr4i	$⊢ (a \in dom W \land b \in dom W) \leftrightarrow \exists s \exists t (a W s \land b W t)$
163	83	simprd	$⊢ (φ \land (a W s \land b W t)) \to (t We b \land \forall y \in b \underset{˙}{[} t^{-1} [\{y\}] / u \underset{˙}{]} u F (t \cap (u \times u)) = y)$
164	163	simpld	$⊢ (φ \land (a W s \land b W t)) \to t We b$
165	164	ad2antrr	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to t We b$
166		weso	$⊢ t We b \to t Or b$
167	165 166	syl	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to t Or b$
168		simprl	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to a \subseteq b$
169		simplrl	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to y \in a$
170	168 169	sseldd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to y \in b$
171		simplrr	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w \in b$
172		solin	$⊢ (t Or b \land (y \in b \land w \in b)) \to (y t w \lor y = w \lor w t y)$
173	167 170 171 172	syl12anc	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (y t w \lor y = w \lor w t y)$
174	22	relelrni	$⊢ b W t \to t \in ran W$
175	174	ad2antll	$⊢ (φ \land (a W s \land b W t)) \to t \in ran W$
176	175	ad2antrr	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to t \in ran W$
177		elssuni	$⊢ t \in ran W \to t \subseteq ⋃ ran W$
178	176 177	syl	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to t \subseteq ⋃ ran W$
179	178	ssbrd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (y t w \to y ⋃ ran W w)$
180		idd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (y = w \to y = w)$
181	178	ssbrd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (w t y \to w ⋃ ran W y)$
182	179 180 181	3orim123d	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to ((y t w \lor y = w \lor w t y) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y))$
183	173 182	mpd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y)$
184	50	adantrr	$⊢ (φ \land (a W s \land b W t)) \to s We a$
185	184	ad2antrr	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to s We a$
186		weso	$⊢ s We a \to s Or a$
187	185 186	syl	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to s Or a$
188		simplrl	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to y \in a$
189		simprl	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to b \subseteq a$
190		simplrr	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to w \in b$
191	189 190	sseldd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to w \in a$
192		solin	$⊢ (s Or a \land (y \in a \land w \in a)) \to (y s w \lor y = w \lor w s y)$
193	187 188 191 192	syl12anc	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to (y s w \lor y = w \lor w s y)$
194	22	relelrni	$⊢ a W s \to s \in ran W$
195	194	ad2antrl	$⊢ (φ \land (a W s \land b W t)) \to s \in ran W$
196	195	ad2antrr	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to s \in ran W$
197		elssuni	$⊢ s \in ran W \to s \subseteq ⋃ ran W$
198	196 197	syl	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to s \subseteq ⋃ ran W$
199	198	ssbrd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to (y s w \to y ⋃ ran W w)$
200		idd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to (y = w \to y = w)$
201	198	ssbrd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to (w s y \to w ⋃ ran W y)$
202	199 200 201	3orim123d	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to ((y s w \lor y = w \lor w s y) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y))$
203	193 202	mpd	$⊢ (((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \land (b \subseteq a \land t = s \cap (a \times b))) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y)$
204	127	adantr	$⊢ ((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \to ((a \subseteq b \land s = t \cap (b \times a)) \lor (b \subseteq a \land t = s \cap (a \times b)))$
205	183 203 204	mpjaodan	$⊢ ((φ \land (a W s \land b W t)) \land (y \in a \land w \in b)) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y)$
206	205	exp31	$⊢ φ \to ((a W s \land b W t) \to ((y \in a \land w \in b) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y)))$
207	206	exlimdvv	$⊢ φ \to (\exists s \exists t (a W s \land b W t) \to ((y \in a \land w \in b) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y)))$
208	162 207	syl5bi	$⊢ φ \to ((a \in dom W \land b \in dom W) \to ((y \in a \land w \in b) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y)))$
209	208	rexlimdvv	$⊢ φ \to (\exists a \in dom W \exists b \in dom W (y \in a \land w \in b) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y))$
210	157 209	syl5bi	$⊢ φ \to ((y \in X \land w \in X) \to (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y))$
211	210	ralrimivv	$⊢ φ \to \forall y \in X \forall w \in X (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y)$
212		dfwe2	$⊢ ⋃ ran W We X \leftrightarrow (⋃ ran W Fr X \land \forall y \in X \forall w \in X (y ⋃ ran W w \lor y = w \lor w ⋃ ran W y))$
213	151 211 212	sylanbrc	$⊢ φ \to ⋃ ran W We X$
214	1	fpwwe2cbv	$⊢ W = \{⟨z, t⟩ \| ((z \subseteq A \land t \subseteq z \times z) \land (t We z \land \forall w \in z \underset{˙}{[} t^{-1} [\{w\}] / b \underset{˙}{]} b F (t \cap (b \times b)) = w))\}$
215	2	adantr	$⊢ (φ \land a W s) \to A \in V$
216		simpr	$⊢ (φ \land a W s) \to a W s$
217	214 215 216	fpwwe2lem3	$⊢ ((φ \land a W s) \land y \in a) \to s^{-1} [\{y\}] F (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) = y$
218	217	anasss	$⊢ (φ \land (a W s \land y \in a)) \to s^{-1} [\{y\}] F (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) = y$
219		cnvimass	$⊢ {⋃ ran W}^{-1} [\{y\}] \subseteq dom ⋃ ran W$
220	2 18	ssexd	$⊢ φ \to X \in V$
221	220 220	xpexd	$⊢ φ \to X \times X \in V$
222	221 38	ssexd	$⊢ φ \to ⋃ ran W \in V$
223	222	adantr	$⊢ (φ \land (a W s \land y \in a)) \to ⋃ ran W \in V$
224	223	dmexd	$⊢ (φ \land (a W s \land y \in a)) \to dom ⋃ ran W \in V$
225		ssexg	$⊢ ({⋃ ran W}^{-1} [\{y\}] \subseteq dom ⋃ ran W \land dom ⋃ ran W \in V) \to {⋃ ran W}^{-1} [\{y\}] \in V$
226	219 224 225	sylancr	$⊢ (φ \land (a W s \land y \in a)) \to {⋃ ran W}^{-1} [\{y\}] \in V$
227		id	$⊢ u = {⋃ ran W}^{-1} [\{y\}] \to u = {⋃ ran W}^{-1} [\{y\}]$
228		olc	$⊢ w = y \to (w s y \lor w = y)$
229		df-br	$⊢ z ⋃ ran W w \leftrightarrow ⟨z, w⟩ \in ⋃ ran W$
230		eluni2	$⊢ ⟨z, w⟩ \in ⋃ ran W \leftrightarrow \exists t \in ran W ⟨z, w⟩ \in t$
231	229 230	bitri	$⊢ z ⋃ ran W w \leftrightarrow \exists t \in ran W ⟨z, w⟩ \in t$
232		df-br	$⊢ z t w \leftrightarrow ⟨z, w⟩ \in t$
233	85	ad2antrr	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to t \subseteq b \times b$
234	233	ssbrd	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (z t w \to z (b \times b) w)$
235		brxp	$⊢ z (b \times b) w \leftrightarrow (z \in b \land w \in b)$
236	235	simplbi	$⊢ z (b \times b) w \to z \in b$
237	234 236	syl6	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (z t w \to z \in b)$
238	21	adantrr	$⊢ (φ \land (a W s \land b W t)) \to s \subseteq a \times a$
239	238	ssbrd	$⊢ (φ \land (a W s \land b W t)) \to (w s y \to w (a \times a) y)$
240	239	imp	$⊢ ((φ \land (a W s \land b W t)) \land w s y) \to w (a \times a) y$
241		brxp	$⊢ w (a \times a) y \leftrightarrow (w \in a \land y \in a)$
242	241	simplbi	$⊢ w (a \times a) y \to w \in a$
243	240 242	syl	$⊢ ((φ \land (a W s \land b W t)) \land w s y) \to w \in a$
244	243	a1d	$⊢ ((φ \land (a W s \land b W t)) \land w s y) \to (y \in a \to w \in a)$
245		elequ1	$⊢ w = y \to (w \in a \leftrightarrow y \in a)$
246	245	biimprd	$⊢ w = y \to (y \in a \to w \in a)$
247	246	adantl	$⊢ ((φ \land (a W s \land b W t)) \land w = y) \to (y \in a \to w \in a)$
248	244 247	jaodan	$⊢ ((φ \land (a W s \land b W t)) \land (w s y \lor w = y)) \to (y \in a \to w \in a)$
249	248	impr	$⊢ ((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \to w \in a$
250	249	adantr	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to w \in a$
251	237 250	jctird	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (z t w \to (z \in b \land w \in a))$
252		brxp	$⊢ z (b \times a) w \leftrightarrow (z \in b \land w \in a)$
253	251 252	syl6ibr	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (z t w \to z (b \times a) w)$
254	253	ancld	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (z t w \to (z t w \land z (b \times a) w))$
255		simprr	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to s = t \cap (b \times a)$
256	255	breqd	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (z s w \leftrightarrow z (t \cap (b \times a)) w)$
257		brin	$⊢ z (t \cap (b \times a)) w \leftrightarrow (z t w \land z (b \times a) w)$
258	256 257	syl6bb	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (z s w \leftrightarrow (z t w \land z (b \times a) w))$
259	254 258	sylibrd	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (a \subseteq b \land s = t \cap (b \times a))) \to (z t w \to z s w)$
260		simprr	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (b \subseteq a \land t = s \cap (a \times b))) \to t = s \cap (a \times b)$
261	260 119	eqsstrdi	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (b \subseteq a \land t = s \cap (a \times b))) \to t \subseteq s$
262	261	ssbrd	$⊢ (((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \land (b \subseteq a \land t = s \cap (a \times b))) \to (z t w \to z s w)$
263	127	adantr	$⊢ ((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \to ((a \subseteq b \land s = t \cap (b \times a)) \lor (b \subseteq a \land t = s \cap (a \times b)))$
264	259 262 263	mpjaodan	$⊢ ((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \to (z t w \to z s w)$
265	232 264	syl5bir	$⊢ ((φ \land (a W s \land b W t)) \land ((w s y \lor w = y) \land y \in a)) \to (⟨z, w⟩ \in t \to z s w)$
266	265	exp32	$⊢ (φ \land (a W s \land b W t)) \to ((w s y \lor w = y) \to (y \in a \to (⟨z, w⟩ \in t \to z s w)))$
267	266	expr	$⊢ (φ \land a W s) \to (b W t \to ((w s y \lor w = y) \to (y \in a \to (⟨z, w⟩ \in t \to z s w))))$
268	267	com24	$⊢ (φ \land a W s) \to (y \in a \to ((w s y \lor w = y) \to (b W t \to (⟨z, w⟩ \in t \to z s w))))$
269	268	impr	$⊢ (φ \land (a W s \land y \in a)) \to ((w s y \lor w = y) \to (b W t \to (⟨z, w⟩ \in t \to z s w)))$
270	269	imp	$⊢ ((φ \land (a W s \land y \in a)) \land (w s y \lor w = y)) \to (b W t \to (⟨z, w⟩ \in t \to z s w))$
271	270	exlimdv	$⊢ ((φ \land (a W s \land y \in a)) \land (w s y \lor w = y)) \to (\exists b b W t \to (⟨z, w⟩ \in t \to z s w))$
272	71 271	syl5bi	$⊢ ((φ \land (a W s \land y \in a)) \land (w s y \lor w = y)) \to (t \in ran W \to (⟨z, w⟩ \in t \to z s w))$
273	272	rexlimdv	$⊢ ((φ \land (a W s \land y \in a)) \land (w s y \lor w = y)) \to (\exists t \in ran W ⟨z, w⟩ \in t \to z s w)$
274	231 273	syl5bi	$⊢ ((φ \land (a W s \land y \in a)) \land (w s y \lor w = y)) \to (z ⋃ ran W w \to z s w)$
275	228 274	sylan2	$⊢ ((φ \land (a W s \land y \in a)) \land w = y) \to (z ⋃ ran W w \to z s w)$
276	275	ex	$⊢ (φ \land (a W s \land y \in a)) \to (w = y \to (z ⋃ ran W w \to z s w))$
277	276	alrimiv	$⊢ (φ \land (a W s \land y \in a)) \to \forall w (w = y \to (z ⋃ ran W w \to z s w))$
278		breq2	$⊢ w = y \to (z ⋃ ran W w \leftrightarrow z ⋃ ran W y)$
279		breq2	$⊢ w = y \to (z s w \leftrightarrow z s y)$
280	278 279	imbi12d	$⊢ w = y \to ((z ⋃ ran W w \to z s w) \leftrightarrow (z ⋃ ran W y \to z s y))$
281	280	equsalvw	$⊢ \forall w (w = y \to (z ⋃ ran W w \to z s w)) \leftrightarrow (z ⋃ ran W y \to z s y)$
282	277 281	sylib	$⊢ (φ \land (a W s \land y \in a)) \to (z ⋃ ran W y \to z s y)$
283	194	ad2antrl	$⊢ (φ \land (a W s \land y \in a)) \to s \in ran W$
284	283 197	syl	$⊢ (φ \land (a W s \land y \in a)) \to s \subseteq ⋃ ran W$
285	284	ssbrd	$⊢ (φ \land (a W s \land y \in a)) \to (z s y \to z ⋃ ran W y)$
286	282 285	impbid	$⊢ (φ \land (a W s \land y \in a)) \to (z ⋃ ran W y \leftrightarrow z s y)$
287		vex	$⊢ z \in V$
288	287	eliniseg	$⊢ y \in V \to (z \in {⋃ ran W}^{-1} [\{y\}] \leftrightarrow z ⋃ ran W y)$
289	288	elv	$⊢ z \in {⋃ ran W}^{-1} [\{y\}] \leftrightarrow z ⋃ ran W y$
290	287	eliniseg	$⊢ y \in V \to (z \in s^{-1} [\{y\}] \leftrightarrow z s y)$
291	290	elv	$⊢ z \in s^{-1} [\{y\}] \leftrightarrow z s y$
292	286 289 291	3bitr4g	$⊢ (φ \land (a W s \land y \in a)) \to (z \in {⋃ ran W}^{-1} [\{y\}] \leftrightarrow z \in s^{-1} [\{y\}])$
293	292	eqrdv	$⊢ (φ \land (a W s \land y \in a)) \to {⋃ ran W}^{-1} [\{y\}] = s^{-1} [\{y\}]$
294	227 293	sylan9eqr	$⊢ ((φ \land (a W s \land y \in a)) \land u = {⋃ ran W}^{-1} [\{y\}]) \to u = s^{-1} [\{y\}]$
295	294	sqxpeqd	$⊢ ((φ \land (a W s \land y \in a)) \land u = {⋃ ran W}^{-1} [\{y\}]) \to u \times u = s^{-1} [\{y\}] \times s^{-1} [\{y\}]$
296	295	ineq2d	$⊢ ((φ \land (a W s \land y \in a)) \land u = {⋃ ran W}^{-1} [\{y\}]) \to ⋃ ran W \cap (u \times u) = ⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])$
297		relinxp	$⊢ Rel (⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}]))$
298		relinxp	$⊢ Rel (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}]))$
299		vex	$⊢ w \in V$
300	299	eliniseg	$⊢ y \in V \to (w \in s^{-1} [\{y\}] \leftrightarrow w s y)$
301	290 300	anbi12d	$⊢ y \in V \to ((z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}]) \leftrightarrow (z s y \land w s y))$
302	301	elv	$⊢ (z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}]) \leftrightarrow (z s y \land w s y)$
303		orc	$⊢ w s y \to (w s y \lor w = y)$
304	303 274	sylan2	$⊢ ((φ \land (a W s \land y \in a)) \land w s y) \to (z ⋃ ran W w \to z s w)$
305	304	adantrl	$⊢ ((φ \land (a W s \land y \in a)) \land (z s y \land w s y)) \to (z ⋃ ran W w \to z s w)$
306	284	adantr	$⊢ ((φ \land (a W s \land y \in a)) \land (z s y \land w s y)) \to s \subseteq ⋃ ran W$
307	306	ssbrd	$⊢ ((φ \land (a W s \land y \in a)) \land (z s y \land w s y)) \to (z s w \to z ⋃ ran W w)$
308	305 307	impbid	$⊢ ((φ \land (a W s \land y \in a)) \land (z s y \land w s y)) \to (z ⋃ ran W w \leftrightarrow z s w)$
309	302 308	sylan2b	$⊢ ((φ \land (a W s \land y \in a)) \land (z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}])) \to (z ⋃ ran W w \leftrightarrow z s w)$
310	309	pm5.32da	$⊢ (φ \land (a W s \land y \in a)) \to (((z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}]) \land z ⋃ ran W w) \leftrightarrow ((z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}]) \land z s w))$
311		df-br	$⊢ z (⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) w \leftrightarrow ⟨z, w⟩ \in (⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}]))$
312		brinxp2	$⊢ z (⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) w \leftrightarrow ((z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}]) \land z ⋃ ran W w)$
313	311 312	bitr3i	$⊢ ⟨z, w⟩ \in (⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) \leftrightarrow ((z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}]) \land z ⋃ ran W w)$
314		df-br	$⊢ z (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) w \leftrightarrow ⟨z, w⟩ \in (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}]))$
315		brinxp2	$⊢ z (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) w \leftrightarrow ((z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}]) \land z s w)$
316	314 315	bitr3i	$⊢ ⟨z, w⟩ \in (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) \leftrightarrow ((z \in s^{-1} [\{y\}] \land w \in s^{-1} [\{y\}]) \land z s w)$
317	310 313 316	3bitr4g	$⊢ (φ \land (a W s \land y \in a)) \to (⟨z, w⟩ \in (⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) \leftrightarrow ⟨z, w⟩ \in (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])))$
318	297 298 317	eqrelrdv	$⊢ (φ \land (a W s \land y \in a)) \to ⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}]) = s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])$
319	318	adantr	$⊢ ((φ \land (a W s \land y \in a)) \land u = {⋃ ran W}^{-1} [\{y\}]) \to ⋃ ran W \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}]) = s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])$
320	296 319	eqtrd	$⊢ ((φ \land (a W s \land y \in a)) \land u = {⋃ ran W}^{-1} [\{y\}]) \to ⋃ ran W \cap (u \times u) = s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])$
321	294 320	oveq12d	$⊢ ((φ \land (a W s \land y \in a)) \land u = {⋃ ran W}^{-1} [\{y\}]) \to u F (⋃ ran W \cap (u \times u)) = s^{-1} [\{y\}] F (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}]))$
322	321	eqeq1d	$⊢ ((φ \land (a W s \land y \in a)) \land u = {⋃ ran W}^{-1} [\{y\}]) \to (u F (⋃ ran W \cap (u \times u)) = y \leftrightarrow s^{-1} [\{y\}] F (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) = y)$
323	226 322	sbcied	$⊢ (φ \land (a W s \land y \in a)) \to (\underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y \leftrightarrow s^{-1} [\{y\}] F (s \cap (s^{-1} [\{y\}] \times s^{-1} [\{y\}])) = y)$
324	218 323	mpbird	$⊢ (φ \land (a W s \land y \in a)) \to \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y$
325	324	exp32	$⊢ φ \to (a W s \to (y \in a \to \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y))$
326	325	exlimdv	$⊢ φ \to (\exists s a W s \to (y \in a \to \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y))$
327	6 326	syl5bi	$⊢ φ \to (a \in dom W \to (y \in a \to \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y))$
328	327	rexlimdv	$⊢ φ \to (\exists a \in dom W y \in a \to \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y)$
329	45 328	syl5bi	$⊢ φ \to (y \in X \to \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y)$
330	329	ralrimiv	$⊢ φ \to \forall y \in X \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y$
331	213 330	jca	$⊢ φ \to (⋃ ran W We X \land \forall y \in X \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y)$
332	1 2	fpwwe2lem2	$⊢ φ \to (X W ⋃ ran W \leftrightarrow ((X \subseteq A \land ⋃ ran W \subseteq X \times X) \land (⋃ ran W We X \land \forall y \in X \underset{˙}{[} {⋃ ran W}^{-1} [\{y\}] / u \underset{˙}{]} u F (⋃ ran W \cap (u \times u)) = y)))$
333	39 331 332	mpbir2and	$⊢ φ \to X W ⋃ ran W$
334	22	releldmi	$⊢ X W ⋃ ran W \to X \in dom W$
335	333 334	syl	$⊢ φ \to X \in dom W$

Metamath Proof Explorer

Theorem fpwwe2lem12

Proof