Theorem 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	⊢ ( 𝐴 ∈ 𝑉 → { 𝑟 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ⊆ 𝐴 )
2		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
3	1 2	sylibr	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑥 ∈ 𝒫 𝐴 )
4		simp2	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑟 ⊆ ( 𝑥 × 𝑥 ) )
5		xpss12	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( 𝑥 × 𝑥 ) ⊆ ( 𝐴 × 𝐴 ) )
6	1 1 5	syl2anc	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ( 𝑥 × 𝑥 ) ⊆ ( 𝐴 × 𝐴 ) )
7	4 6	sstrd	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑟 ⊆ ( 𝐴 × 𝐴 ) )
8		velpw	⊢ ( 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ↔ 𝑟 ⊆ ( 𝐴 × 𝐴 ) )
9	7 8	sylibr	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
10	3 9	jca	⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) )
11	10	eximi	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) → ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) )
12	11	ss2abi	⊢ { 𝑟 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ⊆ { 𝑟 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) }
13		simpr	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
14	13	exlimiv	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) → 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) )
15	14	ss2abi	⊢ { 𝑟 ∣ ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) ) } ⊆ { 𝑟 ∣ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) }
16	12 15	sstri	⊢ { 𝑟 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ⊆ { 𝑟 ∣ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) }
17		abid2	⊢ { 𝑟 ∣ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) } = 𝒫 ( 𝐴 × 𝐴 )
18		sqxpexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 𝐴 ) ∈ V )
19	18	pwexd	⊢ ( 𝐴 ∈ 𝑉 → 𝒫 ( 𝐴 × 𝐴 ) ∈ V )
20	17 19	eqeltrid	⊢ ( 𝐴 ∈ 𝑉 → { 𝑟 ∣ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) } ∈ V )
21		ssexg	⊢ ( ( { 𝑟 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ⊆ { 𝑟 ∣ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) } ∧ { 𝑟 ∣ 𝑟 ∈ 𝒫 ( 𝐴 × 𝐴 ) } ∈ V ) → { 𝑟 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ∈ V )
22	16 20 21	sylancr	⊢ ( 𝐴 ∈ 𝑉 → { 𝑟 ∣ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ ( 𝑥 × 𝑥 ) ∧ 𝑟 We 𝑥 ) } ∈ V )