Theorem abweex 35775

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

Assertion

Ref	Expression
abweex	⊢ (𝐴 ∈ 𝑉 → {𝑟 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ∈ V)

Distinct variable group:   𝐴,𝑟,𝑥

Allowed substitution hints:   𝑉(𝑥, 𝑟)

Proof of Theorem abweex

Step	Hyp	Ref	Expression
1		simp1 1154	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ⊆ 𝐴)
2		velpw 4561	. . . . . . 7 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
3	1, 2	sylibr 237	. . . . . 6 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑥 ∈ 𝒫 𝐴)
4		simp2 1155	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝑥 × 𝑥))
5		xpss12 5666	. . . . . . . . 9 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
6	1, 1, 5	syl2anc 596	. . . . . . . 8 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 × 𝑥) ⊆ (𝐴 × 𝐴))
7	4, 6	sstrd 3919	. . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ⊆ (𝐴 × 𝐴))
8		velpw 4561	. . . . . . 7 ⊢ (𝑟 ∈ 𝒫 (𝐴 × 𝐴) ↔ 𝑟 ⊆ (𝐴 × 𝐴))
9	7, 8	sylibr 237	. . . . . 6 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
10	3, 9	jca 521	. . . . 5 ⊢ ((𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → (𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)))
11	10	eximi 1867	. . . 4 ⊢ (∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥) → ∃𝑥(𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)))
12	11	ss2abi 3990	. . 3 ⊢ {𝑟 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⊆ {𝑟 ∣ ∃𝑥(𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴))}
13		simpr 490	. . . . 5 ⊢ ((𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
14	13	exlimiv 1962	. . . 4 ⊢ (∃𝑥(𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)) → 𝑟 ∈ 𝒫 (𝐴 × 𝐴))
15	14	ss2abi 3990	. . 3 ⊢ {𝑟 ∣ ∃𝑥(𝑥 ∈ 𝒫 𝐴 ∧ 𝑟 ∈ 𝒫 (𝐴 × 𝐴))} ⊆ {𝑟 ∣ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)}
16	12, 15	sstri 3918	. 2 ⊢ {𝑟 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⊆ {𝑟 ∣ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)}
17		abid2 2897	. . 3 ⊢ {𝑟 ∣ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)} = 𝒫 (𝐴 × 𝐴)
18		sqxpexg 7773	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝐴 × 𝐴) ∈ V)
19	18	pwexd 5341	. . 3 ⊢ (𝐴 ∈ 𝑉 → 𝒫 (𝐴 × 𝐴) ∈ V)
20	17, 19	eqeltrid 2864	. 2 ⊢ (𝐴 ∈ 𝑉 → {𝑟 ∣ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)} ∈ V)
21		ssexg 5281	. 2 ⊢ (({𝑟 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ⊆ {𝑟 ∣ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)} ∧ {𝑟 ∣ 𝑟 ∈ 𝒫 (𝐴 × 𝐴)} ∈ V) → {𝑟 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ∈ V)
22	16, 20, 21	sylancr 599	1 ⊢ (𝐴 ∈ 𝑉 → {𝑟 ∣ ∃𝑥(𝑥 ⊆ 𝐴 ∧ 𝑟 ⊆ (𝑥 × 𝑥) ∧ 𝑟 We 𝑥)} ∈ V)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103  ∃wex 1811   ∈ wcel 2144  {cab 2738  Vcvv 3450   ⊆ wss 3896  𝒫 cpw 4556   We wwe 5603   × cxp 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5327  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-opab 5167  df-xp 5657  df-rel 5658

This theorem is used by:  onprcf1acwevdlem1  35996