Metamath Proof Explorer

Theorem weexenwe

Description: If a well-ordering of an infinite set exists, then a well-ordering equinumerous to the set exists. (Contributed by BTernaryTau, 31-Jul-2026)

Ref Expression
Assertion weexenwe 
|- ( ( E. r r We A /\ _om ~<_ A ) -> E. s ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) )

Proof

Step Hyp Ref Expression
1 ween 
 |-  ( A e. dom card <-> E. r r We A )
2 inss2 
 |-  ( r i^i ( A X. A ) ) C_ ( A X. A )
3 weinxp 
 |-  ( r We A <-> ( r i^i ( A X. A ) ) We A )
4 3 biimpi 
 |-  ( r We A -> ( r i^i ( A X. A ) ) We A )
5 4 3ad2ant3 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ r We A ) -> ( r i^i ( A X. A ) ) We A )
6 reldom 
 |-  Rel ~<_
7 6 brrelex2i 
 |-  ( _om ~<_ A -> A e. _V )
8 7 7 xpexd 
 |-  ( _om ~<_ A -> ( A X. A ) e. _V )
9 ssdomg 
 |-  ( ( A X. A ) e. _V -> ( ( r i^i ( A X. A ) ) C_ ( A X. A ) -> ( r i^i ( A X. A ) ) ~<_ ( A X. A ) ) )
10 8 2 9 mpisyl 
 |-  ( _om ~<_ A -> ( r i^i ( A X. A ) ) ~<_ ( A X. A ) )
11 infxpidm2 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( A X. A ) ~~ A )
12 domentr 
 |-  ( ( ( r i^i ( A X. A ) ) ~<_ ( A X. A ) /\ ( A X. A ) ~~ A ) -> ( r i^i ( A X. A ) ) ~<_ A )
13 10 11 12 syl2an2 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( r i^i ( A X. A ) ) ~<_ A )
14 13 3adant3 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ r We A ) -> ( r i^i ( A X. A ) ) ~<_ A )
15 weso 
 |-  ( ( r i^i ( A X. A ) ) We A -> ( r i^i ( A X. A ) ) Or A )
16 3 15 sylbi 
 |-  ( r We A -> ( r i^i ( A X. A ) ) Or A )
17 vex 
 |-  r e. _V
18 17 inex1 
 |-  ( r i^i ( A X. A ) ) e. _V
19 soinfdom 
 |-  ( ( ( r i^i ( A X. A ) ) Or A /\ ( r i^i ( A X. A ) ) e. _V /\ _om ~<_ A ) -> A ~<_ ( r i^i ( A X. A ) ) )
20 18 19 mp3an2 
 |-  ( ( ( r i^i ( A X. A ) ) Or A /\ _om ~<_ A ) -> A ~<_ ( r i^i ( A X. A ) ) )
21 16 20 sylan 
 |-  ( ( r We A /\ _om ~<_ A ) -> A ~<_ ( r i^i ( A X. A ) ) )
22 21 ancoms 
 |-  ( ( _om ~<_ A /\ r We A ) -> A ~<_ ( r i^i ( A X. A ) ) )
23 22 3adant1 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ r We A ) -> A ~<_ ( r i^i ( A X. A ) ) )
24 sbth 
 |-  ( ( ( r i^i ( A X. A ) ) ~<_ A /\ A ~<_ ( r i^i ( A X. A ) ) ) -> ( r i^i ( A X. A ) ) ~~ A )
25 14 23 24 syl2anc 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ r We A ) -> ( r i^i ( A X. A ) ) ~~ A )
26 sseq1 
 |-  ( s = ( r i^i ( A X. A ) ) -> ( s C_ ( A X. A ) <-> ( r i^i ( A X. A ) ) C_ ( A X. A ) ) )
27 weeq1 
 |-  ( s = ( r i^i ( A X. A ) ) -> ( s We A <-> ( r i^i ( A X. A ) ) We A ) )
28 breq1 
 |-  ( s = ( r i^i ( A X. A ) ) -> ( s ~~ A <-> ( r i^i ( A X. A ) ) ~~ A ) )
29 26 27 28 3anbi123d 
 |-  ( s = ( r i^i ( A X. A ) ) -> ( ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) <-> ( ( r i^i ( A X. A ) ) C_ ( A X. A ) /\ ( r i^i ( A X. A ) ) We A /\ ( r i^i ( A X. A ) ) ~~ A ) ) )
30 18 29 spcev 
 |-  ( ( ( r i^i ( A X. A ) ) C_ ( A X. A ) /\ ( r i^i ( A X. A ) ) We A /\ ( r i^i ( A X. A ) ) ~~ A ) -> E. s ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) )
31 2 5 25 30 mp3an2i 
 |-  ( ( A e. dom card /\ _om ~<_ A /\ r We A ) -> E. s ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) )
32 31 3expia 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( r We A -> E. s ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) ) )
33 32 exlimdv 
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( E. r r We A -> E. s ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) ) )
34 1 33 sylanbr 
 |-  ( ( E. r r We A /\ _om ~<_ A ) -> ( E. r r We A -> E. s ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) ) )
35 34 adantrd 
 |-  ( ( E. r r We A /\ _om ~<_ A ) -> ( ( E. r r We A /\ _om ~<_ A ) -> E. s ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) ) )
36 35 pm2.43i 
 |-  ( ( E. r r We A /\ _om ~<_ A ) -> E. s ( s C_ ( A X. A ) /\ s We A /\ s ~~ A ) )