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	28	difexd	$⊢ ((φ \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$
30	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)$
31	30	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$
32		wefr	$⊢ W (X) We X \to W (X) Fr X$
33	31 32	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$
34		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$
35		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$
36	35	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)$
37	29 33 34 36	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)$
38		ssdif0	$⊢ X \cap {W (X)}^{-1} [\{z\}] \subseteq Y \leftrightarrow (X \cap {W (X)}^{-1} [\{z\}]) ∖ Y = \emptyset$
39		indif1	$⊢ (X ∖ Y) \cap {W (X)}^{-1} [\{z\}] = (X \cap {W (X)}^{-1} [\{z\}]) ∖ Y$
40	39	eqeq1i	$⊢ (X ∖ Y) \cap {W (X)}^{-1} [\{z\}] = \emptyset \leftrightarrow (X \cap {W (X)}^{-1} [\{z\}]) ∖ Y = \emptyset$
41		disj	$⊢ (X ∖ Y) \cap {W (X)}^{-1} [\{z\}] = \emptyset \leftrightarrow \forall w \in (X ∖ Y) \neg w \in {W (X)}^{-1} [\{z\}]$
42		vex	$⊢ w \in V$
43	42	eliniseg	$⊢ z \in V \to (w \in {W (X)}^{-1} [\{z\}] \leftrightarrow w W (X) z)$
44	43	elv	$⊢ w \in {W (X)}^{-1} [\{z\}] \leftrightarrow w W (X) z$
45	44	notbii	$⊢ \neg w \in {W (X)}^{-1} [\{z\}] \leftrightarrow \neg w W (X) z$
46	45	ralbii	$⊢ \forall w \in (X ∖ Y) \neg w \in {W (X)}^{-1} [\{z\}] \leftrightarrow \forall w \in (X ∖ Y) \neg w W (X) z$
47	41 46	bitri	$⊢ (X ∖ Y) \cap {W (X)}^{-1} [\{z\}] = \emptyset \leftrightarrow \forall w \in (X ∖ Y) \neg w W (X) z$
48	38 40 47	3bitr2i	$⊢ X \cap {W (X)}^{-1} [\{z\}] \subseteq Y \leftrightarrow \forall w \in (X ∖ Y) \neg w W (X) z$
49		cnvimass	$⊢ {W (X)}^{-1} [\{z\}] \subseteq dom W (X)$
50	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$
51		dmss	$⊢ W (X) \subseteq X \times X \to dom W (X) \subseteq dom (X \times X)$
52	50 51	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)$
53		dmxpid	$⊢ dom (X \times X) = X$
54	52 53	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$
55	49 54	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$
56		sseqin2	$⊢ {W (X)}^{-1} [\{z\}] \subseteq X \leftrightarrow X \cap {W (X)}^{-1} [\{z\}] = {W (X)}^{-1} [\{z\}]$
57	55 56	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\}]$
58	57	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)$
59	48 58	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)$
60	59	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)$
61		eldifn	$⊢ z \in (X ∖ Y) \to \neg z \in Y$
62	61	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$
63		eleq1w	$⊢ w = z \to (w \in Y \leftrightarrow z \in Y)$
64	63	notbid	$⊢ w = z \to (\neg w \in Y \leftrightarrow \neg z \in Y)$
65	62 64	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)$
66	65	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)$
67	66	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$
68	62	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$
69		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)$
70	69	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)$
71	70	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)$
72		eldifi	$⊢ z \in (X ∖ Y) \to z \in X$
73	72	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$
74	73	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$
75		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$
76		brxp	$⊢ z (X \times Y) w \leftrightarrow (z \in X \land w \in Y)$
77	74 75 76	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$
78		brin	$⊢ z (W (X) \cap (X \times Y)) w \leftrightarrow (z W (X) w \land z (X \times Y) w)$
79	78	rbaib	$⊢ z (X \times Y) w \to (z (W (X) \cap (X \times Y)) w \leftrightarrow z W (X) w)$
80	77 79	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)$
81	71 80	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)$
82	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)))$
83	82	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))$
84	83	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))$
85	84	simpld	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to (Y \subseteq A \land R \subseteq Y \times Y)$
86	85	simprd	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to R \subseteq Y \times Y$
87	86	ad3antrrr	$⊢ ((((φ \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$
88	87	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)$
89		brxp	$⊢ z (Y \times Y) w \leftrightarrow (z \in Y \land w \in Y)$
90	89	simplbi	$⊢ z (Y \times Y) w \to z \in Y$
91	88 90	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)$
92	81 91	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)$
93	68 92	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$
94	31	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$
95		weso	$⊢ W (X) We X \to W (X) Or X$
96	94 95	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$
97	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$
98	97	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$
99		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))$
100		ioran	$⊢ \neg (w = z \lor z W (X) w) \leftrightarrow (\neg w = z \land \neg z W (X) w)$
101	99 100	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))$
102	96 98 74 101	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))$
103	67 93 102	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$
104	103 44	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\}]$
105	104	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\}])$
106	105	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\}]$
107		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$
108	106 107	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\}]$
109		in32	$⊢ (W (X) \cap (X \times Y)) \cap (Y \times Y) = (W (X) \cap (Y \times Y)) \cap (X \times Y)$
110		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)$
111	110	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)$
112	86	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$
113		dfss2	$⊢ R \subseteq Y \times Y \leftrightarrow R \cap (Y \times Y) = R$
114	112 113	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$
115	111 114	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$
116		inss2	$⊢ W (X) \cap (Y \times Y) \subseteq Y \times Y$
117		xpss1	$⊢ Y \subseteq X \to Y \times Y \subseteq X \times Y$
118	97 117	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$
119	116 118	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$
120		dfss2	$⊢ 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)$
121	119 120	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)$
122	109 115 121	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)$
123	108	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\}]$
124	123	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\}])$
125	122 124	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\}])$
126	108 125	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\}]))$
127	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$
128	22	adantr	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to X W W (X)$
129	128	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)$
130	1 127 129	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$
131	73 130	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$
132	126 131	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$
133	132 62	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$
134	133	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)$
135	60 134	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)$
136	37 135	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)$
137	136	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)$
138	16 137	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$
139		ssdif0	$⊢ X \subseteq Y \leftrightarrow X ∖ Y = \emptyset$
140	138 139	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$
141	140	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)$
142	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$
143		simprl	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to Y W R$
144	1 17 142 128 143	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)))$
145	15 141 144	mpjaod	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to X \subseteq Y$
146	13 145	eqssd	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to Y = X$
147	6	adantr	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to Fun W$
148	146 143	eqbrtrrd	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to X W R$
149		funbrfv	$⊢ Fun W \to (X W R \to W (X) = R)$
150	147 148 149	sylc	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to W (X) = R$
151	150	eqcomd	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to R = W (X)$
152	146 151	jca	$⊢ (φ \land (Y W R \land Y F R \in Y)) \to (Y = X \land R = W (X))$
153	152	ex	$⊢ φ \to ((Y W R \land Y F R \in Y) \to (Y = X \land R = W (X)))$
154	1 2 3 4	fpwwe2lem12	$⊢ φ \to X F W (X) \in X$
155	22 154	jca	$⊢ φ \to (X W W (X) \land X F W (X) \in X)$
156		breq12	$⊢ (Y = X \land R = W (X)) \to (Y W R \leftrightarrow X W W (X))$
157		oveq12	$⊢ (Y = X \land R = W (X)) \to Y F R = X F W (X)$
158		simpl	$⊢ (Y = X \land R = W (X)) \to Y = X$
159	157 158	eleq12d	$⊢ (Y = X \land R = W (X)) \to (Y F R \in Y \leftrightarrow X F W (X) \in X)$
160	156 159	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))$
161	155 160	syl5ibrcom	$⊢ φ \to ((Y = X \land R = W (X)) \to (Y W R \land Y F R \in Y))$
162	153 161	impbid	$⊢ φ \to ((Y W R \land Y F R \in Y) \leftrightarrow (Y = X \land R = W (X)))$

Metamath Proof Explorer

Theorem fpwwe2

Proof