Metamath Proof Explorer

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 
|- ( A e. V -> { r | E. x ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } e. _V )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x C_ A )
2 velpw 
 |-  ( x e. ~P A <-> x C_ A )
3 1 2 sylibr 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> x e. ~P A )
4 simp2 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r C_ ( x X. x ) )
5 xpss12 
 |-  ( ( x C_ A /\ x C_ A ) -> ( x X. x ) C_ ( A X. A ) )
6 1 1 5 syl2anc 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x X. x ) C_ ( A X. A ) )
7 4 6 sstrd 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r C_ ( A X. A ) )
8 velpw 
 |-  ( r e. ~P ( A X. A ) <-> r C_ ( A X. A ) )
9 7 8 sylibr 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> r e. ~P ( A X. A ) )
10 3 9 jca 
 |-  ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> ( x e. ~P A /\ r e. ~P ( A X. A ) ) )
11 10 eximi 
 |-  ( E. x ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) -> E. x ( x e. ~P A /\ r e. ~P ( A X. A ) ) )
12 11 ss2abi 
 |-  { r | E. x ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } C_ { r | E. x ( x e. ~P A /\ r e. ~P ( A X. A ) ) }
13 simpr 
 |-  ( ( x e. ~P A /\ r e. ~P ( A X. A ) ) -> r e. ~P ( A X. A ) )
14 13 exlimiv 
 |-  ( E. x ( x e. ~P A /\ r e. ~P ( A X. A ) ) -> r e. ~P ( A X. A ) )
15 14 ss2abi 
 |-  { r | E. x ( x e. ~P A /\ r e. ~P ( A X. A ) ) } C_ { r | r e. ~P ( A X. A ) }
16 12 15 sstri 
 |-  { r | E. x ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } C_ { r | r e. ~P ( A X. A ) }
17 abid2 
 |-  { r | r e. ~P ( A X. A ) } = ~P ( A X. A )
18 sqxpexg 
 |-  ( A e. V -> ( A X. A ) e. _V )
19 18 pwexd 
 |-  ( A e. V -> ~P ( A X. A ) e. _V )
20 17 19 eqeltrid 
 |-  ( A e. V -> { r | r e. ~P ( A X. A ) } e. _V )
21 ssexg 
 |-  ( ( { r | E. x ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } C_ { r | r e. ~P ( A X. A ) } /\ { r | r e. ~P ( A X. A ) } e. _V ) -> { r | E. x ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } e. _V )
22 16 20 21 sylancr 
 |-  ( A e. V -> { r | E. x ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } e. _V )