abweex

Description: The class of well-orders of a set A and its subsets is a set. (Contributed by BTernaryTau, 2-Aug-2026)

		Ref	Expression
	Assertion	abweex	$⊢ A \in V \to \{r \| \exists x (x \subseteq A \land r \subseteq x \times x \land r We x)\} \in V$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \subseteq A$
2		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
3	1 2	sylibr	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \in 𝒫 A$
4		simp2	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to r \subseteq x \times x$
5		xpss12	$⊢ (x \subseteq A \land x \subseteq A) \to x \times x \subseteq A \times A$
6	1 1 5	syl2anc	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to x \times x \subseteq A \times A$
7	4 6	sstrd	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to r \subseteq A \times A$
8		velpw	$⊢ r \in 𝒫 (A \times A) \leftrightarrow r \subseteq A \times A$
9	7 8	sylibr	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to r \in 𝒫 (A \times A)$
10	3 9	jca	$⊢ (x \subseteq A \land r \subseteq x \times x \land r We x) \to (x \in 𝒫 A \land r \in 𝒫 (A \times A))$
11	10	eximi	$⊢ \exists x (x \subseteq A \land r \subseteq x \times x \land r We x) \to \exists x (x \in 𝒫 A \land r \in 𝒫 (A \times A))$
12	11	ss2abi	$⊢ \{r \| \exists x (x \subseteq A \land r \subseteq x \times x \land r We x)\} \subseteq \{r \| \exists x (x \in 𝒫 A \land r \in 𝒫 (A \times A))\}$
13		simpr	$⊢ (x \in 𝒫 A \land r \in 𝒫 (A \times A)) \to r \in 𝒫 (A \times A)$
14	13	exlimiv	$⊢ \exists x (x \in 𝒫 A \land r \in 𝒫 (A \times A)) \to r \in 𝒫 (A \times A)$
15	14	ss2abi	$⊢ \{r \| \exists x (x \in 𝒫 A \land r \in 𝒫 (A \times A))\} \subseteq \{r \| r \in 𝒫 (A \times A)\}$
16	12 15	sstri	$⊢ \{r \| \exists x (x \subseteq A \land r \subseteq x \times x \land r We x)\} \subseteq \{r \| r \in 𝒫 (A \times A)\}$
17		abid2	$⊢ \{r \| r \in 𝒫 (A \times A)\} = 𝒫 (A \times A)$
18		sqxpexg	$⊢ A \in V \to A \times A \in V$
19	18	pwexd	$⊢ A \in V \to 𝒫 (A \times A) \in V$
20	17 19	eqeltrid	$⊢ A \in V \to \{r \| r \in 𝒫 (A \times A)\} \in V$
21		ssexg	$⊢ (\{r \| \exists x (x \subseteq A \land r \subseteq x \times x \land r We x)\} \subseteq \{r \| r \in 𝒫 (A \times A)\} \land \{r \| r \in 𝒫 (A \times A)\} \in V) \to \{r \| \exists x (x \subseteq A \land r \subseteq x \times x \land r We x)\} \in V$
22	16 20 21	sylancr	$⊢ A \in V \to \{r \| \exists x (x \subseteq A \land r \subseteq x \times x \land r We x)\} \in V$

Metamath Proof Explorer

Theorem abweex

Proof