Metamath Proof Explorer

Theorem acwer1prclem

Description: Lemma for acwer1prc . (Contributed by BTernaryTau, 31-Jul-2026)

Ref Expression
Hypothesis acwer1prclem.1 
|- W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
Assertion acwer1prclem 
|- ( ( CHOICE /\ _om ~<_ A /\ ( card ` ( R1 ` B ) ) = A ) -> E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = A ) )

Proof

Step Hyp Ref Expression
1 acwer1prclem.1 
 |-  W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
2 simp1 
 |-  ( ( CHOICE /\ _om ~<_ A /\ ( card ` ( R1 ` B ) ) = A ) -> CHOICE )
3 breq2 
 |-  ( ( card ` ( R1 ` B ) ) = A -> ( _om ~<_ ( card ` ( R1 ` B ) ) <-> _om ~<_ A ) )
4 3 biimpar 
 |-  ( ( ( card ` ( R1 ` B ) ) = A /\ _om ~<_ A ) -> _om ~<_ ( card ` ( R1 ` B ) ) )
5 fvex 
 |-  ( R1 ` B ) e. _V
6 acnum 
 |-  ( CHOICE -> ( ( R1 ` B ) e. _V -> ( R1 ` B ) e. dom card ) )
7 5 6 mpi 
 |-  ( CHOICE -> ( R1 ` B ) e. dom card )
8 cardid2 
 |-  ( ( R1 ` B ) e. dom card -> ( card ` ( R1 ` B ) ) ~~ ( R1 ` B ) )
9 domentr 
 |-  ( ( _om ~<_ ( card ` ( R1 ` B ) ) /\ ( card ` ( R1 ` B ) ) ~~ ( R1 ` B ) ) -> _om ~<_ ( R1 ` B ) )
10 8 9 sylan2 
 |-  ( ( _om ~<_ ( card ` ( R1 ` B ) ) /\ ( R1 ` B ) e. dom card ) -> _om ~<_ ( R1 ` B ) )
11 7 10 sylan2 
 |-  ( ( _om ~<_ ( card ` ( R1 ` B ) ) /\ CHOICE ) -> _om ~<_ ( R1 ` B ) )
12 11 expcom 
 |-  ( CHOICE -> ( _om ~<_ ( card ` ( R1 ` B ) ) -> _om ~<_ ( R1 ` B ) ) )
13 4 12 syl5 
 |-  ( CHOICE -> ( ( ( card ` ( R1 ` B ) ) = A /\ _om ~<_ A ) -> _om ~<_ ( R1 ` B ) ) )
14 13 ancomsd 
 |-  ( CHOICE -> ( ( _om ~<_ A /\ ( card ` ( R1 ` B ) ) = A ) -> _om ~<_ ( R1 ` B ) ) )
15 14 3impib 
 |-  ( ( CHOICE /\ _om ~<_ A /\ ( card ` ( R1 ` B ) ) = A ) -> _om ~<_ ( R1 ` B ) )
16 dfac8 
 |-  ( CHOICE <-> A. z E. y y We z )
17 weeq2 
 |-  ( z = ( R1 ` B ) -> ( y We z <-> y We ( R1 ` B ) ) )
18 17 exbidv 
 |-  ( z = ( R1 ` B ) -> ( E. y y We z <-> E. y y We ( R1 ` B ) ) )
19 5 18 spcv 
 |-  ( A. z E. y y We z -> E. y y We ( R1 ` B ) )
20 16 19 sylbi 
 |-  ( CHOICE -> E. y y We ( R1 ` B ) )
21 weexenwe 
 |-  ( ( E. y y We ( R1 ` B ) /\ _om ~<_ ( R1 ` B ) ) -> E. s ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ s ~~ ( R1 ` B ) ) )
22 20 21 sylan 
 |-  ( ( CHOICE /\ _om ~<_ ( R1 ` B ) ) -> E. s ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ s ~~ ( R1 ` B ) ) )
23 carden2b 
 |-  ( s ~~ ( R1 ` B ) -> ( card ` s ) = ( card ` ( R1 ` B ) ) )
24 23 3anim3i 
 |-  ( ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ s ~~ ( R1 ` B ) ) -> ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) )
25 24 eximi 
 |-  ( E. s ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ s ~~ ( R1 ` B ) ) -> E. s ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) )
26 22 25 syl 
 |-  ( ( CHOICE /\ _om ~<_ ( R1 ` B ) ) -> E. s ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) )
27 2 15 26 syl2anc 
 |-  ( ( CHOICE /\ _om ~<_ A /\ ( card ` ( R1 ` B ) ) = A ) -> E. s ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) )
28 df-3an 
 |-  ( ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) <-> ( ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) )
29 fveq2 
 |-  ( x = B -> ( R1 ` x ) = ( R1 ` B ) )
30 29 sqxpeqd 
 |-  ( x = B -> ( ( R1 ` x ) X. ( R1 ` x ) ) = ( ( R1 ` B ) X. ( R1 ` B ) ) )
31 30 sseq2d 
 |-  ( x = B -> ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) <-> s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) ) )
32 eqidd 
 |-  ( x = B -> s = s )
33 32 29 weeq12d 
 |-  ( x = B -> ( s We ( R1 ` x ) <-> s We ( R1 ` B ) ) )
34 31 33 anbi12d 
 |-  ( x = B -> ( ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) <-> ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) ) )
35 34 rspcev 
 |-  ( ( B e. On /\ ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) ) -> E. x e. On ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) )
36 0elon 
 |-  (/) e. On
37 r1fnon 
 |-  R1 Fn On
38 37 fndmi 
 |-  dom R1 = On
39 38 eleq2i 
 |-  ( B e. dom R1 <-> B e. On )
40 ndmfv 
 |-  ( -. B e. dom R1 -> ( R1 ` B ) = (/) )
41 39 40 sylnbir 
 |-  ( -. B e. On -> ( R1 ` B ) = (/) )
42 r10 
 |-  ( R1 ` (/) ) = (/)
43 41 42 eqtr4di 
 |-  ( -. B e. On -> ( R1 ` B ) = ( R1 ` (/) ) )
44 43 sqxpeqd 
 |-  ( -. B e. On -> ( ( R1 ` B ) X. ( R1 ` B ) ) = ( ( R1 ` (/) ) X. ( R1 ` (/) ) ) )
45 44 sseq2d 
 |-  ( -. B e. On -> ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) <-> s C_ ( ( R1 ` (/) ) X. ( R1 ` (/) ) ) ) )
46 eqidd 
 |-  ( -. B e. On -> s = s )
47 46 43 weeq12d 
 |-  ( -. B e. On -> ( s We ( R1 ` B ) <-> s We ( R1 ` (/) ) ) )
48 45 47 anbi12d 
 |-  ( -. B e. On -> ( ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) <-> ( s C_ ( ( R1 ` (/) ) X. ( R1 ` (/) ) ) /\ s We ( R1 ` (/) ) ) ) )
49 48 biimpa 
 |-  ( ( -. B e. On /\ ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) ) -> ( s C_ ( ( R1 ` (/) ) X. ( R1 ` (/) ) ) /\ s We ( R1 ` (/) ) ) )
50 fveq2 
 |-  ( x = (/) -> ( R1 ` x ) = ( R1 ` (/) ) )
51 50 sqxpeqd 
 |-  ( x = (/) -> ( ( R1 ` x ) X. ( R1 ` x ) ) = ( ( R1 ` (/) ) X. ( R1 ` (/) ) ) )
52 51 sseq2d 
 |-  ( x = (/) -> ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) <-> s C_ ( ( R1 ` (/) ) X. ( R1 ` (/) ) ) ) )
53 eqidd 
 |-  ( x = (/) -> s = s )
54 53 50 weeq12d 
 |-  ( x = (/) -> ( s We ( R1 ` x ) <-> s We ( R1 ` (/) ) ) )
55 52 54 anbi12d 
 |-  ( x = (/) -> ( ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) <-> ( s C_ ( ( R1 ` (/) ) X. ( R1 ` (/) ) ) /\ s We ( R1 ` (/) ) ) ) )
56 55 rspcev 
 |-  ( ( (/) e. On /\ ( s C_ ( ( R1 ` (/) ) X. ( R1 ` (/) ) ) /\ s We ( R1 ` (/) ) ) ) -> E. x e. On ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) )
57 36 49 56 sylancr 
 |-  ( ( -. B e. On /\ ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) ) -> E. x e. On ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) )
58 35 57 pm2.61ian 
 |-  ( ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) -> E. x e. On ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) )
59 vex 
 |-  s e. _V
60 sseq1 
 |-  ( r = s -> ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) <-> s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) ) )
61 weeq1 
 |-  ( r = s -> ( r We ( R1 ` x ) <-> s We ( R1 ` x ) ) )
62 60 61 anbi12d 
 |-  ( r = s -> ( ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) <-> ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) ) )
63 62 rexbidv 
 |-  ( r = s -> ( E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) <-> E. x e. On ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) ) )
64 59 63 1 elab2 
 |-  ( s e. W <-> E. x e. On ( s C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ s We ( R1 ` x ) ) )
65 58 64 sylibr 
 |-  ( ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) -> s e. W )
66 acnum 
 |-  ( CHOICE -> ( s e. W -> s e. dom card ) )
67 cardf2 
 |-  card : { v | E. w e. On w ~~ v } --> On
68 ffun 
 |-  ( card : { v | E. w e. On w ~~ v } --> On -> Fun card )
69 67 68 ax-mp 
 |-  Fun card
70 funfvima 
 |-  ( ( Fun card /\ s e. dom card ) -> ( s e. W -> ( card ` s ) e. ( card " W ) ) )
71 69 70 mpan 
 |-  ( s e. dom card -> ( s e. W -> ( card ` s ) e. ( card " W ) ) )
72 66 71 syli 
 |-  ( CHOICE -> ( s e. W -> ( card ` s ) e. ( card " W ) ) )
73 eqtr 
 |-  ( ( ( card ` s ) = ( card ` ( R1 ` B ) ) /\ ( card ` ( R1 ` B ) ) = A ) -> ( card ` s ) = A )
74 73 expcom 
 |-  ( ( card ` ( R1 ` B ) ) = A -> ( ( card ` s ) = ( card ` ( R1 ` B ) ) -> ( card ` s ) = A ) )
75 72 74 im2anan9 
 |-  ( ( CHOICE /\ ( card ` ( R1 ` B ) ) = A ) -> ( ( s e. W /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) -> ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = A ) ) )
76 65 75 sylani 
 |-  ( ( CHOICE /\ ( card ` ( R1 ` B ) ) = A ) -> ( ( ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) -> ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = A ) ) )
77 28 76 biimtrid 
 |-  ( ( CHOICE /\ ( card ` ( R1 ` B ) ) = A ) -> ( ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) -> ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = A ) ) )
78 77 eximdv 
 |-  ( ( CHOICE /\ ( card ` ( R1 ` B ) ) = A ) -> ( E. s ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) -> E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = A ) ) )
79 78 3adant2 
 |-  ( ( CHOICE /\ _om ~<_ A /\ ( card ` ( R1 ` B ) ) = A ) -> ( E. s ( s C_ ( ( R1 ` B ) X. ( R1 ` B ) ) /\ s We ( R1 ` B ) /\ ( card ` s ) = ( card ` ( R1 ` B ) ) ) -> E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = A ) ) )
80 27 79 mpd 
 |-  ( ( CHOICE /\ _om ~<_ A /\ ( card ` ( R1 ` B ) ) = A ) -> E. s ( ( card ` s ) e. ( card " W ) /\ ( card ` s ) = A ) )