fpwwe2

Description: Given any function F from well-orderings of subsets of A to A , there is a unique well-ordered subset <. X , ( WX ) >. which "agrees" with F in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a . Theorem 1.1 of KanamoriPincus p. 415. (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	fpwwe2	$⊢ φ \to ((Y W R \land Y F R \in Y) \leftrightarrow (Y = X \land R = W (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 2 3 4	fpwwe2lem10	$⊢ φ \to W : dom W ⟶ 𝒫 (X \times X)$
6	5	ffund	$⊢ φ \to Fun W$
7		funbrfv2b	$⊢ Fun W \to (Y W R \leftrightarrow (Y \in dom W \land W (Y) = R))$
8	6 7	syl	$⊢ φ \to (Y W R \leftrightarrow (Y \in dom W \land W (Y) = R))$
9	8	simprbda	$⊢ (φ \land Y W R) \to Y \in dom W$
10	9	adantrr	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to Y \in dom W$
11		elssuni	$⊢ Y \in dom W \to Y \subseteq ⋃ dom W$
12	11 4	sseqtrrdi	$⊢ Y \in dom W \to Y \subseteq X$
13	10 12	syl	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to Y \subseteq X$
14		simpl	$⊢ (X \subseteq Y \land W (X) = R \cap (Y \times X)) \to X \subseteq Y$
15	14	a1i	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to ((X \subseteq Y \land W (X) = R \cap (Y \times X)) \to X \subseteq Y)$
16		simplrr	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to Y F R \in Y$
17	2	adantr	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to A \in V$
18	17	adantr	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to A \in V$
19	1 2 3 4	fpwwe2lem11	$⊢ φ \to X \in dom W$
20		funfvbrb	$⊢ Fun W \to (X \in dom W \leftrightarrow X W W (X))$
21	6 20	syl	$⊢ φ \to (X \in dom W \leftrightarrow X W W (X))$
22	19 21	mpbid	$⊢ φ \to X W W (X)$
23	1 2	fpwwe2lem2	$⊢ φ \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)))$
24	22 23	mpbid	$⊢ φ \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))$
25	24	ad2antrr	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \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))$
26	25	simpld	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (X \subseteq A \land W (X) \subseteq X \times X)$
27	26	simpld	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to X \subseteq A$
28	18 27	ssexd	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to X \in V$
29		difexg	$⊢ X \in V \to X ∖ Y \in V$
30	28 29	syl	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to X ∖ Y \in V$
31	25	simprd	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \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)$
32	31	simpld	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to W (X) We X$
33		wefr	$⊢ W (X) We X \to W (X) Fr X$
34	32 33	syl	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to W (X) Fr X$
35		difssd	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to X ∖ Y \subseteq X$
36		fri	$⊢ ((X ∖ Y \in V \land W (X) Fr X) \land (X ∖ Y \subseteq X \land X ∖ Y \neq \emptyset)) \to \exists z \in (X ∖ Y) \forall w \in (X ∖ Y) \neg w W (X) z$
37	36	expr	$⊢ ((X ∖ Y \in V \land W (X) Fr X) \land X ∖ Y \subseteq X) \to (X ∖ Y \neq \emptyset \to \exists z \in (X ∖ Y) \forall w \in (X ∖ Y) \neg w W (X) z)$
38	30 34 35 37	syl21anc	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (X ∖ Y \neq \emptyset \to \exists z \in (X ∖ Y) \forall w \in (X ∖ Y) \neg w W (X) z)$
39		ssdif0	$⊢ X \cap {W (X)}^{-1} [\{z\}] \subseteq Y \leftrightarrow (X \cap {W (X)}^{-1} [\{z\}]) ∖ Y = \emptyset$
40		indif1	$⊢ (X ∖ Y) \cap {W (X)}^{-1} [\{z\}] = (X \cap {W (X)}^{-1} [\{z\}]) ∖ Y$
41	40	eqeq1i	$⊢ (X ∖ Y) \cap {W (X)}^{-1} [\{z\}] = \emptyset \leftrightarrow (X \cap {W (X)}^{-1} [\{z\}]) ∖ Y = \emptyset$
42		disj	$⊢ (X ∖ Y) \cap {W (X)}^{-1} [\{z\}] = \emptyset \leftrightarrow \forall w \in (X ∖ Y) \neg w \in {W (X)}^{-1} [\{z\}]$
43		vex	$⊢ w \in V$
44	43	eliniseg	$⊢ z \in V \to (w \in {W (X)}^{-1} [\{z\}] \leftrightarrow w W (X) z)$
45	44	elv	$⊢ w \in {W (X)}^{-1} [\{z\}] \leftrightarrow w W (X) z$
46	45	notbii	$⊢ \neg w \in {W (X)}^{-1} [\{z\}] \leftrightarrow \neg w W (X) z$
47	46	ralbii	$⊢ \forall w \in (X ∖ Y) \neg w \in {W (X)}^{-1} [\{z\}] \leftrightarrow \forall w \in (X ∖ Y) \neg w W (X) z$
48	42 47	bitri	$⊢ (X ∖ Y) \cap {W (X)}^{-1} [\{z\}] = \emptyset \leftrightarrow \forall w \in (X ∖ Y) \neg w W (X) z$
49	39 41 48	3bitr2i	$⊢ X \cap {W (X)}^{-1} [\{z\}] \subseteq Y \leftrightarrow \forall w \in (X ∖ Y) \neg w W (X) z$
50		cnvimass	$⊢ {W (X)}^{-1} [\{z\}] \subseteq dom W (X)$
51	26	simprd	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to W (X) \subseteq X \times X$
52		dmss	$⊢ W (X) \subseteq X \times X \to dom W (X) \subseteq dom (X \times X)$
53	51 52	syl	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to dom W (X) \subseteq dom (X \times X)$
54		dmxpid	$⊢ dom (X \times X) = X$
55	53 54	sseqtrdi	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to dom W (X) \subseteq X$
56	50 55	sstrid	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to {W (X)}^{-1} [\{z\}] \subseteq X$
57		sseqin2	$⊢ {W (X)}^{-1} [\{z\}] \subseteq X \leftrightarrow X \cap {W (X)}^{-1} [\{z\}] = {W (X)}^{-1} [\{z\}]$
58	56 57	sylib	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to X \cap {W (X)}^{-1} [\{z\}] = {W (X)}^{-1} [\{z\}]$
59	58	sseq1d	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (X \cap {W (X)}^{-1} [\{z\}] \subseteq Y \leftrightarrow {W (X)}^{-1} [\{z\}] \subseteq Y)$
60	49 59	bitr3id	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (\forall w \in (X ∖ Y) \neg w W (X) z \leftrightarrow {W (X)}^{-1} [\{z\}] \subseteq Y)$
61	60	rexbidv	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (\exists z \in (X ∖ Y) \forall w \in (X ∖ Y) \neg w W (X) z \leftrightarrow \exists z \in (X ∖ Y) {W (X)}^{-1} [\{z\}] \subseteq Y)$
62		eldifn	$⊢ z \in (X ∖ Y) \to \neg z \in Y$
63	62	ad2antrl	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to \neg z \in Y$
64		eleq1w	$⊢ w = z \to (w \in Y \leftrightarrow z \in Y)$
65	64	notbid	$⊢ w = z \to (\neg w \in Y \leftrightarrow \neg z \in Y)$
66	63 65	syl5ibrcom	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to (w = z \to \neg w \in Y)$
67	66	con2d	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to (w \in Y \to \neg w = z)$
68	67	imp	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to \neg w = z$
69	63	adantr	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to \neg z \in Y$
70		simprr	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to R = W (X) \cap (X \times Y)$
71	70	ad2antrr	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to R = W (X) \cap (X \times Y)$
72	71	breqd	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to (z R w \leftrightarrow z (W (X) \cap (X \times Y)) w)$
73		eldifi	$⊢ z \in (X ∖ Y) \to z \in X$
74	73	ad2antrl	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to z \in X$
75	74	adantr	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to z \in X$
76		simpr	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to w \in Y$
77		brxp	$⊢ z (X \times Y) w \leftrightarrow (z \in X \land w \in Y)$
78	75 76 77	sylanbrc	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to z (X \times Y) w$
79		brin	$⊢ z (W (X) \cap (X \times Y)) w \leftrightarrow (z W (X) w \land z (X \times Y) w)$
80	79	rbaib	$⊢ z (X \times Y) w \to (z (W (X) \cap (X \times Y)) w \leftrightarrow z W (X) w)$
81	78 80	syl	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to (z (W (X) \cap (X \times Y)) w \leftrightarrow z W (X) w)$
82	72 81	bitrd	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to (z R w \leftrightarrow z W (X) w)$
83	1 2	fpwwe2lem2	$⊢ φ \to (Y W R \leftrightarrow ((Y \subseteq A \land R \subseteq Y \times Y) \land (R We Y \land \forall y \in Y \underset{˙}{[} R^{-1} [\{y\}] / u \underset{˙}{]} u F (R \cap (u \times u)) = y)))$
84	83	biimpa	$⊢ (φ \land Y W R) \to ((Y \subseteq A \land R \subseteq Y \times Y) \land (R We Y \land \forall y \in Y \underset{˙}{[} R^{-1} [\{y\}] / u \underset{˙}{]} u F (R \cap (u \times u)) = y))$
85	84	adantrr	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to ((Y \subseteq A \land R \subseteq Y \times Y) \land (R We Y \land \forall y \in Y \underset{˙}{[} R^{-1} [\{y\}] / u \underset{˙}{]} u F (R \cap (u \times u)) = y))$
86	85	simpld	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to (Y \subseteq A \land R \subseteq Y \times Y)$
87	86	simprd	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to R \subseteq Y \times Y$
88	87	ad5ant12	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to R \subseteq Y \times Y$
89	88	ssbrd	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to (z R w \to z (Y \times Y) w)$
90		brxp	$⊢ z (Y \times Y) w \leftrightarrow (z \in Y \land w \in Y)$
91	90	simplbi	$⊢ z (Y \times Y) w \to z \in Y$
92	89 91	syl6	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to (z R w \to z \in Y)$
93	82 92	sylbird	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to (z W (X) w \to z \in Y)$
94	69 93	mtod	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to \neg z W (X) w$
95	32	ad2antrr	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to W (X) We X$
96		weso	$⊢ W (X) We X \to W (X) Or X$
97	95 96	syl	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to W (X) Or X$
98	13	ad2antrr	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to Y \subseteq X$
99	98	sselda	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to w \in X$
100		sotric	$⊢ (W (X) Or X \land (w \in X \land z \in X)) \to (w W (X) z \leftrightarrow \neg (w = z \lor z W (X) w))$
101		ioran	$⊢ \neg (w = z \lor z W (X) w) \leftrightarrow (\neg w = z \land \neg z W (X) w)$
102	100 101	bitrdi	$⊢ (W (X) Or X \land (w \in X \land z \in X)) \to (w W (X) z \leftrightarrow (\neg w = z \land \neg z W (X) w))$
103	97 99 75 102	syl12anc	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to (w W (X) z \leftrightarrow (\neg w = z \land \neg z W (X) w))$
104	68 94 103	mpbir2and	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to w W (X) z$
105	104 45	sylibr	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land w \in Y) \to w \in {W (X)}^{-1} [\{z\}]$
106	105	ex	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to (w \in Y \to w \in {W (X)}^{-1} [\{z\}])$
107	106	ssrdv	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to Y \subseteq {W (X)}^{-1} [\{z\}]$
108		simprr	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to {W (X)}^{-1} [\{z\}] \subseteq Y$
109	107 108	eqssd	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to Y = {W (X)}^{-1} [\{z\}]$
110		in32	$⊢ (W (X) \cap (X \times Y)) \cap (Y \times Y) = (W (X) \cap (Y \times Y)) \cap (X \times Y)$
111		simplrr	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to R = W (X) \cap (X \times Y)$
112	111	ineq1d	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to R \cap (Y \times Y) = (W (X) \cap (X \times Y)) \cap (Y \times Y)$
113	87	ad2antrr	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to R \subseteq Y \times Y$
114		df-ss	$⊢ R \subseteq Y \times Y \leftrightarrow R \cap (Y \times Y) = R$
115	113 114	sylib	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to R \cap (Y \times Y) = R$
116	112 115	eqtr3d	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to (W (X) \cap (X \times Y)) \cap (Y \times Y) = R$
117		inss2	$⊢ W (X) \cap (Y \times Y) \subseteq Y \times Y$
118		xpss1	$⊢ Y \subseteq X \to Y \times Y \subseteq X \times Y$
119	98 118	syl	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to Y \times Y \subseteq X \times Y$
120	117 119	sstrid	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to W (X) \cap (Y \times Y) \subseteq X \times Y$
121		df-ss	$⊢ W (X) \cap (Y \times Y) \subseteq X \times Y \leftrightarrow (W (X) \cap (Y \times Y)) \cap (X \times Y) = W (X) \cap (Y \times Y)$
122	120 121	sylib	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to (W (X) \cap (Y \times Y)) \cap (X \times Y) = W (X) \cap (Y \times Y)$
123	110 116 122	3eqtr3a	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to R = W (X) \cap (Y \times Y)$
124	109	sqxpeqd	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to Y \times Y = {W (X)}^{-1} [\{z\}] \times {W (X)}^{-1} [\{z\}]$
125	124	ineq2d	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to W (X) \cap (Y \times Y) = W (X) \cap ({W (X)}^{-1} [\{z\}] \times {W (X)}^{-1} [\{z\}])$
126	123 125	eqtrd	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to R = W (X) \cap ({W (X)}^{-1} [\{z\}] \times {W (X)}^{-1} [\{z\}])$
127	109 126	oveq12d	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to Y F R = {W (X)}^{-1} [\{z\}] F (W (X) \cap ({W (X)}^{-1} [\{z\}] \times {W (X)}^{-1} [\{z\}]))$
128	18	adantr	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to A \in V$
129	22	adantr	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to X W W (X)$
130	129	ad2antrr	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to X W W (X)$
131	1 128 130	fpwwe2lem3	$⊢ ((((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \land z \in X) \to {W (X)}^{-1} [\{z\}] F (W (X) \cap ({W (X)}^{-1} [\{z\}] \times {W (X)}^{-1} [\{z\}])) = z$
132	74 131	mpdan	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to {W (X)}^{-1} [\{z\}] F (W (X) \cap ({W (X)}^{-1} [\{z\}] \times {W (X)}^{-1} [\{z\}])) = z$
133	127 132	eqtrd	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to Y F R = z$
134	133 63	eqneltrd	$⊢ (((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \land (z \in (X ∖ Y) \land {W (X)}^{-1} [\{z\}] \subseteq Y)) \to \neg Y F R \in Y$
135	134	rexlimdvaa	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (\exists z \in (X ∖ Y) {W (X)}^{-1} [\{z\}] \subseteq Y \to \neg Y F R \in Y)$
136	61 135	sylbid	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (\exists z \in (X ∖ Y) \forall w \in (X ∖ Y) \neg w W (X) z \to \neg Y F R \in Y)$
137	38 136	syld	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (X ∖ Y \neq \emptyset \to \neg Y F R \in Y)$
138	137	necon4ad	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to (Y F R \in Y \to X ∖ Y = \emptyset)$
139	16 138	mpd	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to X ∖ Y = \emptyset$
140		ssdif0	$⊢ X \subseteq Y \leftrightarrow X ∖ Y = \emptyset$
141	139 140	sylibr	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (Y \subseteq X \land R = W (X) \cap (X \times Y))) \to X \subseteq Y$
142	141	ex	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to ((Y \subseteq X \land R = W (X) \cap (X \times Y)) \to X \subseteq Y)$
143	3	adantlr	$⊢ ((φ \land (Y W R \land Y F R \in Y)) \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x F r \in A$
144		simprl	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to Y W R$
145	1 17 143 129 144	fpwwe2lem9	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to ((X \subseteq Y \land W (X) = R \cap (Y \times X)) \lor (Y \subseteq X \land R = W (X) \cap (X \times Y)))$
146	15 142 145	mpjaod	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to X \subseteq Y$
147	13 146	eqssd	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to Y = X$
148	6	adantr	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to Fun W$
149	147 144	eqbrtrrd	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to X W R$
150		funbrfv	$⊢ Fun W \to (X W R \to W (X) = R)$
151	148 149 150	sylc	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to W (X) = R$
152	151	eqcomd	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to R = W (X)$
153	147 152	jca	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to (Y = X \land R = W (X))$
154	153	ex	$⊢ φ \to ((Y W R \land Y F R \in Y) \to (Y = X \land R = W (X)))$
155	1 2 3 4	fpwwe2lem12	$⊢ φ \to X F W (X) \in X$
156	22 155	jca	$⊢ φ \to (X W W (X) \land X F W (X) \in X)$
157		breq12	$⊢ (Y = X \land R = W (X)) \to (Y W R \leftrightarrow X W W (X))$
158		oveq12	$⊢ (Y = X \land R = W (X)) \to Y F R = X F W (X)$
159		simpl	$⊢ (Y = X \land R = W (X)) \to Y = X$
160	158 159	eleq12d	$⊢ (Y = X \land R = W (X)) \to (Y F R \in Y \leftrightarrow X F W (X) \in X)$
161	157 160	anbi12d	$⊢ (Y = X \land R = W (X)) \to ((Y W R \land Y F R \in Y) \leftrightarrow (X W W (X) \land X F W (X) \in X))$
162	156 161	syl5ibrcom	$⊢ φ \to ((Y = X \land R = W (X)) \to (Y W R \land Y F R \in Y))$
163	154 162	impbid	$⊢ φ \to ((Y W R \land Y F R \in Y) \leftrightarrow (Y = X \land R = W (X)))$

Metamath Proof Explorer

Theorem fpwwe2

Proof