fpwwe2lem10

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

	Ref	Expression
Hypotheses	fpwwe2.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u F (r \cap (u \times u)) = y))\}$
	fpwwe2.2	$⊢ φ \to A \in V$
	fpwwe2.3	$⊢ (φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
	fpwwe2.4	$⊢ X = ⋃ dom W$
Assertion	fpwwe2lem10	$⊢ φ \to W : dom W ⟶ 𝒫 (X \times 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	1	relopabiv	$⊢ Rel W$
6	5	a1i	$⊢ φ \to Rel W$
7		simprr	$⊢ ((φ \land (w W s \land w W t)) \land (w \subseteq w \land s = t \cap (w \times w))) \to s = t \cap (w \times w)$
8	1 2	fpwwe2lem2	$⊢ φ \to (w W t \leftrightarrow ((w \subseteq A \land t \subseteq w \times w) \land (t We w \land \forall y \in w \underset{˙}{[} t^{-1} [\{y\}] / u \underset{˙}{]} u F (t \cap (u \times u)) = y)))$
9	8	simprbda	$⊢ (φ \land w W t) \to (w \subseteq A \land t \subseteq w \times w)$
10	9	simprd	$⊢ (φ \land w W t) \to t \subseteq w \times w$
11	10	adantrl	$⊢ (φ \land (w W s \land w W t)) \to t \subseteq w \times w$
12	11	adantr	$⊢ ((φ \land (w W s \land w W t)) \land (w \subseteq w \land s = t \cap (w \times w))) \to t \subseteq w \times w$
13		dfss2	$⊢ t \subseteq w \times w \leftrightarrow t \cap (w \times w) = t$
14	12 13	sylib	$⊢ ((φ \land (w W s \land w W t)) \land (w \subseteq w \land s = t \cap (w \times w))) \to t \cap (w \times w) = t$
15	7 14	eqtrd	$⊢ ((φ \land (w W s \land w W t)) \land (w \subseteq w \land s = t \cap (w \times w))) \to s = t$
16		simprr	$⊢ ((φ \land (w W s \land w W t)) \land (w \subseteq w \land t = s \cap (w \times w))) \to t = s \cap (w \times w)$
17	1 2	fpwwe2lem2	$⊢ φ \to (w W s \leftrightarrow ((w \subseteq A \land s \subseteq w \times w) \land (s We w \land \forall y \in w \underset{˙}{[} s^{-1} [\{y\}] / u \underset{˙}{]} u F (s \cap (u \times u)) = y)))$
18	17	simprbda	$⊢ (φ \land w W s) \to (w \subseteq A \land s \subseteq w \times w)$
19	18	simprd	$⊢ (φ \land w W s) \to s \subseteq w \times w$
20	19	adantrr	$⊢ (φ \land (w W s \land w W t)) \to s \subseteq w \times w$
21	20	adantr	$⊢ ((φ \land (w W s \land w W t)) \land (w \subseteq w \land t = s \cap (w \times w))) \to s \subseteq w \times w$
22		dfss2	$⊢ s \subseteq w \times w \leftrightarrow s \cap (w \times w) = s$
23	21 22	sylib	$⊢ ((φ \land (w W s \land w W t)) \land (w \subseteq w \land t = s \cap (w \times w))) \to s \cap (w \times w) = s$
24	16 23	eqtr2d	$⊢ ((φ \land (w W s \land w W t)) \land (w \subseteq w \land t = s \cap (w \times w))) \to s = t$
25	2	adantr	$⊢ (φ \land (w W s \land w W t)) \to A \in V$
26	3	adantlr	$⊢ ((φ \land (w W s \land w W t)) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
27		simprl	$⊢ (φ \land (w W s \land w W t)) \to w W s$
28		simprr	$⊢ (φ \land (w W s \land w W t)) \to w W t$
29	1 25 26 27 28	fpwwe2lem9	$⊢ (φ \land (w W s \land w W t)) \to ((w \subseteq w \land s = t \cap (w \times w)) \lor (w \subseteq w \land t = s \cap (w \times w)))$
30	15 24 29	mpjaodan	$⊢ (φ \land (w W s \land w W t)) \to s = t$
31	30	ex	$⊢ φ \to ((w W s \land w W t) \to s = t)$
32	31	alrimiv	$⊢ φ \to \forall t ((w W s \land w W t) \to s = t)$
33	32	alrimivv	$⊢ φ \to \forall w \forall s \forall t ((w W s \land w W t) \to s = t)$
34		dffun2	$⊢ Fun W \leftrightarrow (Rel W \land \forall w \forall s \forall t ((w W s \land w W t) \to s = t))$
35	6 33 34	sylanbrc	$⊢ φ \to Fun W$
36	35	funfnd	$⊢ φ \to W Fn dom W$
37		vex	$⊢ s \in V$
38	37	elrn	$⊢ s \in ran W \leftrightarrow \exists w w W s$
39	5	releldmi	$⊢ w W s \to w \in dom W$
40	39	adantl	$⊢ (φ \land w W s) \to w \in dom W$
41		elssuni	$⊢ w \in dom W \to w \subseteq ⋃ dom W$
42	40 41	syl	$⊢ (φ \land w W s) \to w \subseteq ⋃ dom W$
43	42 4	sseqtrrdi	$⊢ (φ \land w W s) \to w \subseteq X$
44		xpss12	$⊢ (w \subseteq X \land w \subseteq X) \to w \times w \subseteq X \times X$
45	43 43 44	syl2anc	$⊢ (φ \land w W s) \to w \times w \subseteq X \times X$
46	19 45	sstrd	$⊢ (φ \land w W s) \to s \subseteq X \times X$
47	46	ex	$⊢ φ \to (w W s \to s \subseteq X \times X)$
48		velpw	$⊢ s \in 𝒫 (X \times X) \leftrightarrow s \subseteq X \times X$
49	47 48	imbitrrdi	$⊢ φ \to (w W s \to s \in 𝒫 (X \times X))$
50	49	exlimdv	$⊢ φ \to (\exists w w W s \to s \in 𝒫 (X \times X))$
51	38 50	biimtrid	$⊢ φ \to (s \in ran W \to s \in 𝒫 (X \times X))$
52	51	ssrdv	$⊢ φ \to ran W \subseteq 𝒫 (X \times X)$
53		df-f	$⊢ W : dom W ⟶ 𝒫 (X \times X) \leftrightarrow (W Fn dom W \land ran W \subseteq 𝒫 (X \times X))$
54	36 52 53	sylanbrc	$⊢ φ \to W : dom W ⟶ 𝒫 (X \times X)$

Metamath Proof Explorer

Theorem fpwwe2lem10

Proof