Metamath Proof Explorer

Theorem onprcf1acwevdlem1

Description: Lemma for onprcf1acwevd . (Contributed by BTernaryTau, 10-Sep-2026)

Ref Expression
Hypothesis onprcf1acwevdlem1.1 
|- W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
Assertion onprcf1acwevdlem1 
|- ( ( A C_ W /\ B e. On /\ A. y e. A -. y We ( R1 ` B ) ) -> A e. _V )

Proof

Step Hyp Ref Expression
1 onprcf1acwevdlem1.1 
 |-  W = { r | E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) }
2 19.28v 
 |-  ( A. y ( ( A C_ W /\ B e. On ) /\ ( y e. A -> -. y We ( R1 ` B ) ) ) <-> ( ( A C_ W /\ B e. On ) /\ A. y ( y e. A -> -. y We ( R1 ` B ) ) ) )
3 df-ral 
 |-  ( A. y e. A -. y We ( R1 ` B ) <-> A. y ( y e. A -> -. y We ( R1 ` B ) ) )
4 3 anbi2i 
 |-  ( ( ( A C_ W /\ B e. On ) /\ A. y e. A -. y We ( R1 ` B ) ) <-> ( ( A C_ W /\ B e. On ) /\ A. y ( y e. A -> -. y We ( R1 ` B ) ) ) )
5 2 4 bitr4i 
 |-  ( A. y ( ( A C_ W /\ B e. On ) /\ ( y e. A -> -. y We ( R1 ` B ) ) ) <-> ( ( A C_ W /\ B e. On ) /\ A. y e. A -. y We ( R1 ` B ) ) )
6 df-3an 
 |-  ( ( A C_ W /\ B e. On /\ ( y e. A -> -. y We ( R1 ` B ) ) ) <-> ( ( A C_ W /\ B e. On ) /\ ( y e. A -> -. y We ( R1 ` B ) ) ) )
7 6 albii 
 |-  ( A. y ( A C_ W /\ B e. On /\ ( y e. A -> -. y We ( R1 ` B ) ) ) <-> A. y ( ( A C_ W /\ B e. On ) /\ ( y e. A -> -. y We ( R1 ` B ) ) ) )
8 df-3an 
 |-  ( ( A C_ W /\ B e. On /\ A. y e. A -. y We ( R1 ` B ) ) <-> ( ( A C_ W /\ B e. On ) /\ A. y e. A -. y We ( R1 ` B ) ) )
9 5 7 8 3bitr4ri 
 |-  ( ( A C_ W /\ B e. On /\ A. y e. A -. y We ( R1 ` B ) ) <-> A. y ( A C_ W /\ B e. On /\ ( y e. A -> -. y We ( R1 ` B ) ) ) )
10 nfa1 
 |-  F/ y A. y ( A C_ W /\ B e. On /\ ( y e. A -> -. y We ( R1 ` B ) ) )
11 nfcv 
 |-  F/_ y A
12 nfcv 
 |-  F/_ y { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) }
13 idd 
 |-  ( y e. A -> ( A C_ W -> A C_ W ) )
14 idd 
 |-  ( y e. A -> ( B e. On -> B e. On ) )
15 pm2.27 
 |-  ( y e. A -> ( ( y e. A -> -. y We ( R1 ` B ) ) -> -. y We ( R1 ` B ) ) )
16 13 14 15 3anim123d 
 |-  ( y e. A -> ( ( A C_ W /\ B e. On /\ ( y e. A -> -. y We ( R1 ` B ) ) ) -> ( A C_ W /\ B e. On /\ -. y We ( R1 ` B ) ) ) )
17 simp1 
 |-  ( ( A C_ W /\ B e. On /\ -. y We ( R1 ` B ) ) -> A C_ W )
18 ssel2 
 |-  ( ( A C_ W /\ y e. A ) -> y e. W )
19 vex 
 |-  y e. _V
20 sseq1 
 |-  ( r = y -> ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) <-> y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) ) )
21 weeq1 
 |-  ( r = y -> ( r We ( R1 ` x ) <-> y We ( R1 ` x ) ) )
22 20 21 anbi12d 
 |-  ( r = y -> ( ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) <-> ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) ) )
23 22 rexbidv 
 |-  ( r = y -> ( E. x e. On ( r C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ r We ( R1 ` x ) ) <-> E. x e. On ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) ) )
24 19 23 1 elab2 
 |-  ( y e. W <-> E. x e. On ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) )
25 18 24 sylib 
 |-  ( ( A C_ W /\ y e. A ) -> E. x e. On ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) )
26 25 expcom 
 |-  ( y e. A -> ( A C_ W -> E. x e. On ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) ) )
27 17 26 syl5 
 |-  ( y e. A -> ( ( A C_ W /\ B e. On /\ -. y We ( R1 ` B ) ) -> E. x e. On ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) ) )
28 ontri1 
 |-  ( ( B e. On /\ x e. On ) -> ( B C_ x <-> -. x e. B ) )
29 28 biimprd 
 |-  ( ( B e. On /\ x e. On ) -> ( -. x e. B -> B C_ x ) )
30 r1ord3 
 |-  ( ( B e. On /\ x e. On ) -> ( B C_ x -> ( R1 ` B ) C_ ( R1 ` x ) ) )
31 30 3impia 
 |-  ( ( B e. On /\ x e. On /\ B C_ x ) -> ( R1 ` B ) C_ ( R1 ` x ) )
32 wess 
 |-  ( ( R1 ` B ) C_ ( R1 ` x ) -> ( y We ( R1 ` x ) -> y We ( R1 ` B ) ) )
33 31 32 syl 
 |-  ( ( B e. On /\ x e. On /\ B C_ x ) -> ( y We ( R1 ` x ) -> y We ( R1 ` B ) ) )
34 33 con3d 
 |-  ( ( B e. On /\ x e. On /\ B C_ x ) -> ( -. y We ( R1 ` B ) -> -. y We ( R1 ` x ) ) )
35 34 3expia 
 |-  ( ( B e. On /\ x e. On ) -> ( B C_ x -> ( -. y We ( R1 ` B ) -> -. y We ( R1 ` x ) ) ) )
36 35 com23 
 |-  ( ( B e. On /\ x e. On ) -> ( -. y We ( R1 ` B ) -> ( B C_ x -> -. y We ( R1 ` x ) ) ) )
37 29 36 syl5d 
 |-  ( ( B e. On /\ x e. On ) -> ( -. y We ( R1 ` B ) -> ( -. x e. B -> -. y We ( R1 ` x ) ) ) )
38 37 3impia 
 |-  ( ( B e. On /\ x e. On /\ -. y We ( R1 ` B ) ) -> ( -. x e. B -> -. y We ( R1 ` x ) ) )
39 38 con4d 
 |-  ( ( B e. On /\ x e. On /\ -. y We ( R1 ` B ) ) -> ( y We ( R1 ` x ) -> x e. B ) )
40 simp1 
 |-  ( ( B e. On /\ x e. On /\ -. y We ( R1 ` B ) ) -> B e. On )
41 39 40 jctild 
 |-  ( ( B e. On /\ x e. On /\ -. y We ( R1 ` B ) ) -> ( y We ( R1 ` x ) -> ( B e. On /\ x e. B ) ) )
42 41 3expia 
 |-  ( ( B e. On /\ x e. On ) -> ( -. y We ( R1 ` B ) -> ( y We ( R1 ` x ) -> ( B e. On /\ x e. B ) ) ) )
43 42 impancom 
 |-  ( ( B e. On /\ -. y We ( R1 ` B ) ) -> ( x e. On -> ( y We ( R1 ` x ) -> ( B e. On /\ x e. B ) ) ) )
44 43 imp 
 |-  ( ( ( B e. On /\ -. y We ( R1 ` B ) ) /\ x e. On ) -> ( y We ( R1 ` x ) -> ( B e. On /\ x e. B ) ) )
45 44 adantld 
 |-  ( ( ( B e. On /\ -. y We ( R1 ` B ) ) /\ x e. On ) -> ( ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) -> ( B e. On /\ x e. B ) ) )
46 r1ord2 
 |-  ( B e. On -> ( x e. B -> ( R1 ` x ) C_ ( R1 ` B ) ) )
47 46 imp 
 |-  ( ( B e. On /\ x e. B ) -> ( R1 ` x ) C_ ( R1 ` B ) )
48 fvex 
 |-  ( R1 ` x ) e. _V
49 sseq1 
 |-  ( w = ( R1 ` x ) -> ( w C_ ( R1 ` B ) <-> ( R1 ` x ) C_ ( R1 ` B ) ) )
50 id 
 |-  ( w = ( R1 ` x ) -> w = ( R1 ` x ) )
51 50 sqxpeqd 
 |-  ( w = ( R1 ` x ) -> ( w X. w ) = ( ( R1 ` x ) X. ( R1 ` x ) ) )
52 51 sseq2d 
 |-  ( w = ( R1 ` x ) -> ( y C_ ( w X. w ) <-> y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) ) )
53 weeq2 
 |-  ( w = ( R1 ` x ) -> ( y We w <-> y We ( R1 ` x ) ) )
54 49 52 53 3anbi123d 
 |-  ( w = ( R1 ` x ) -> ( ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) <-> ( ( R1 ` x ) C_ ( R1 ` B ) /\ y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) ) )
55 48 54 spcev 
 |-  ( ( ( R1 ` x ) C_ ( R1 ` B ) /\ y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) -> E. w ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) )
56 55 3expib 
 |-  ( ( R1 ` x ) C_ ( R1 ` B ) -> ( ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) -> E. w ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) ) )
57 47 56 syl 
 |-  ( ( B e. On /\ x e. B ) -> ( ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) -> E. w ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) ) )
58 45 57 syli 
 |-  ( ( ( B e. On /\ -. y We ( R1 ` B ) ) /\ x e. On ) -> ( ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) -> E. w ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) ) )
59 58 rexlimdva 
 |-  ( ( B e. On /\ -. y We ( R1 ` B ) ) -> ( E. x e. On ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) -> E. w ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) ) )
60 sseq1 
 |-  ( v = y -> ( v C_ ( w X. w ) <-> y C_ ( w X. w ) ) )
61 weeq1 
 |-  ( v = y -> ( v We w <-> y We w ) )
62 60 61 3anbi23d 
 |-  ( v = y -> ( ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) <-> ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) ) )
63 62 exbidv 
 |-  ( v = y -> ( E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) <-> E. w ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) ) )
64 19 63 elab 
 |-  ( y e. { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } <-> E. w ( w C_ ( R1 ` B ) /\ y C_ ( w X. w ) /\ y We w ) )
65 59 64 imbitrrdi 
 |-  ( ( B e. On /\ -. y We ( R1 ` B ) ) -> ( E. x e. On ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) -> y e. { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } ) )
66 65 3adant1 
 |-  ( ( A C_ W /\ B e. On /\ -. y We ( R1 ` B ) ) -> ( E. x e. On ( y C_ ( ( R1 ` x ) X. ( R1 ` x ) ) /\ y We ( R1 ` x ) ) -> y e. { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } ) )
67 27 66 sylcom 
 |-  ( y e. A -> ( ( A C_ W /\ B e. On /\ -. y We ( R1 ` B ) ) -> y e. { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } ) )
68 16 67 syldc 
 |-  ( ( A C_ W /\ B e. On /\ ( y e. A -> -. y We ( R1 ` B ) ) ) -> ( y e. A -> y e. { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } ) )
69 68 sps 
 |-  ( A. y ( A C_ W /\ B e. On /\ ( y e. A -> -. y We ( R1 ` B ) ) ) -> ( y e. A -> y e. { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } ) )
70 10 11 12 69 ssrd 
 |-  ( A. y ( A C_ W /\ B e. On /\ ( y e. A -> -. y We ( R1 ` B ) ) ) -> A C_ { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } )
71 9 70 sylbi 
 |-  ( ( A C_ W /\ B e. On /\ A. y e. A -. y We ( R1 ` B ) ) -> A C_ { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } )
72 fvex 
 |-  ( R1 ` B ) e. _V
73 abweex 
 |-  ( ( R1 ` B ) e. _V -> { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } e. _V )
74 72 73 ax-mp 
 |-  { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } e. _V
75 74 ssex 
 |-  ( A C_ { v | E. w ( w C_ ( R1 ` B ) /\ v C_ ( w X. w ) /\ v We w ) } -> A e. _V )
76 71 75 syl 
 |-  ( ( A C_ W /\ B e. On /\ A. y e. A -. y We ( R1 ` B ) ) -> A e. _V )