fpwwe

Description: Given any function F from the powerset of A to A , canth2 gives that the function is not injective, but we can say rather more than that. 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	fpwwe.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
	fpwwe.2	$⊢ φ \to A \in V$
	fpwwe.3	$⊢ (φ \land x \in (𝒫 A \cap dom card)) \to F (x) \in A$
	fpwwe.4	$⊢ X = ⋃ dom W$
Assertion	fpwwe	$⊢ φ \to ((Y W R \land F (Y) \in Y) \leftrightarrow (Y = X \land R = W (X)))$

Proof

Step	Hyp	Ref	Expression
1		fpwwe.1	$⊢ W = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
2		fpwwe.2	$⊢ φ \to A \in V$
3		fpwwe.3	$⊢ (φ \land x \in (𝒫 A \cap dom card)) \to F (x) \in A$
4		fpwwe.4	$⊢ X = ⋃ dom W$
5		df-ov	$⊢ Y (F \circ 1^{st}) R = (F \circ 1^{st}) (⟨Y, R⟩)$
6		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
7		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
8	6 7	ax-mp	$⊢ 1^{st} Fn V$
9		opex	$⊢ ⟨Y, R⟩ \in V$
10		fvco2	$⊢ (1^{st} Fn V \land ⟨Y, R⟩ \in V) \to (F \circ 1^{st}) (⟨Y, R⟩) = F (1^{st} (⟨Y, R⟩))$
11	8 9 10	mp2an	$⊢ (F \circ 1^{st}) (⟨Y, R⟩) = F (1^{st} (⟨Y, R⟩))$
12	5 11	eqtri	$⊢ Y (F \circ 1^{st}) R = F (1^{st} (⟨Y, R⟩))$
13	1	bropaex12	$⊢ Y W R \to (Y \in V \land R \in V)$
14		op1stg	$⊢ (Y \in V \land R \in V) \to 1^{st} (⟨Y, R⟩) = Y$
15	13 14	syl	$⊢ Y W R \to 1^{st} (⟨Y, R⟩) = Y$
16	15	fveq2d	$⊢ Y W R \to F (1^{st} (⟨Y, R⟩)) = F (Y)$
17	12 16	eqtrid	$⊢ Y W R \to Y (F \circ 1^{st}) R = F (Y)$
18	17	eleq1d	$⊢ Y W R \to (Y (F \circ 1^{st}) R \in Y \leftrightarrow F (Y) \in Y)$
19	18	pm5.32i	$⊢ (Y W R \land Y (F \circ 1^{st}) R \in Y) \leftrightarrow (Y W R \land F (Y) \in Y)$
20		vex	$⊢ r \in V$
21	20	cnvex	$⊢ r^{-1} \in V$
22	21	imaex	$⊢ r^{-1} [\{y\}] \in V$
23		vex	$⊢ u \in V$
24	20	inex1	$⊢ r \cap (u \times u) \in V$
25	23 24	opco1i	$⊢ u (F \circ 1^{st}) (r \cap (u \times u)) = F (u)$
26		fveq2	$⊢ u = r^{-1} [\{y\}] \to F (u) = F (r^{-1} [\{y\}])$
27	25 26	eqtrid	$⊢ u = r^{-1} [\{y\}] \to u (F \circ 1^{st}) (r \cap (u \times u)) = F (r^{-1} [\{y\}])$
28	27	eqeq1d	$⊢ u = r^{-1} [\{y\}] \to (u (F \circ 1^{st}) (r \cap (u \times u)) = y \leftrightarrow F (r^{-1} [\{y\}]) = y)$
29	22 28	sbcie	$⊢ \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u (F \circ 1^{st}) (r \cap (u \times u)) = y \leftrightarrow F (r^{-1} [\{y\}]) = y$
30	29	ralbii	$⊢ \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u (F \circ 1^{st}) (r \cap (u \times u)) = y \leftrightarrow \forall y \in x F (r^{-1} [\{y\}]) = y$
31	30	anbi2i	$⊢ (r We x \land \forall y \in x \underset{˙}{[} r^{-1} [\{y\}] / u \underset{˙}{]} u (F \circ 1^{st}) (r \cap (u \times u)) = y) \leftrightarrow (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y)$
32	31	anbi2i	$⊢ ((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 \circ 1^{st}) (r \cap (u \times u)) = y)) \leftrightarrow ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))$
33	32	opabbii	$⊢ \{⟨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 \circ 1^{st}) (r \cap (u \times u)) = y))\} = \{⟨x, r⟩ \| ((x \subseteq A \land r \subseteq x \times x) \land (r We x \land \forall y \in x F (r^{-1} [\{y\}]) = y))\}$
34	1 33	eqtr4i	$⊢ 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 \circ 1^{st}) (r \cap (u \times u)) = y))\}$
35		vex	$⊢ x \in V$
36	35 20	opco1i	$⊢ x (F \circ 1^{st}) r = F (x)$
37		simp1	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \subseteq A$
38		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
39	37 38	sylibr	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \in 𝒫 A$
40		19.8a	$⊢ r We x \to \exists r r We x$
41	40	3ad2ant3	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to \exists r r We x$
42		ween	$⊢ x \in dom card \leftrightarrow \exists r r We x$
43	41 42	sylibr	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \in dom card$
44	39 43	elind	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \in (𝒫 A \cap dom card)$
45	44 3	sylan2	$⊢ (φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to F (x) \in A$
46	36 45	eqeltrid	$⊢ (φ \land (x \subseteq A \land r \subseteq x \times x \land r We x)) \to x (F \circ 1^{st}) r \in A$
47	34 2 46 4	fpwwe2	$⊢ φ \to ((Y W R \land Y (F \circ 1^{st}) R \in Y) \leftrightarrow (Y = X \land R = W (X)))$
48	19 47	bitr3id	$⊢ φ \to ((Y W R \land F (Y) \in Y) \leftrightarrow (Y = X \land R = W (X)))$

Metamath Proof Explorer

Theorem fpwwe

Proof