Metamath Proof Explorer

Theorem onprcf1acwevdlem2

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

Ref Expression
Hypotheses onprcf1acwevdlem2.1 
|- R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y S z ) ) }
onprcf1acwevdlem2.2 
|- S = ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
onprcf1acwevdlem2.3 
|- ( ( ph /\ u e. On ) -> E. w e. On ( F ` w ) We ( R1 ` u ) )
Assertion onprcf1acwevdlem2 
|- ( ph -> R We _V )

Proof

Step Hyp Ref Expression
1 onprcf1acwevdlem2.1 
 |-  R = { <. y , z >. | ( ( rank ` y ) e. ( rank ` z ) \/ ( ( rank ` y ) = ( rank ` z ) /\ y S z ) ) }
2 onprcf1acwevdlem2.2 
 |-  S = ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
3 onprcf1acwevdlem2.3 
 |-  ( ( ph /\ u e. On ) -> E. w e. On ( F ` w ) We ( R1 ` u ) )
4 rankon 
 |-  ( rank ` y ) e. On
5 4 onsuci 
 |-  suc ( rank ` y ) e. On
6 3 ralrimiva 
 |-  ( ph -> A. u e. On E. w e. On ( F ` w ) We ( R1 ` u ) )
7 eqidd 
 |-  ( u = suc ( rank ` y ) -> ( F ` w ) = ( F ` w ) )
8 fveq2 
 |-  ( u = suc ( rank ` y ) -> ( R1 ` u ) = ( R1 ` suc ( rank ` y ) ) )
9 7 8 weeq12d 
 |-  ( u = suc ( rank ` y ) -> ( ( F ` w ) We ( R1 ` u ) <-> ( F ` w ) We ( R1 ` suc ( rank ` y ) ) ) )
10 9 rexbidv 
 |-  ( u = suc ( rank ` y ) -> ( E. w e. On ( F ` w ) We ( R1 ` u ) <-> E. w e. On ( F ` w ) We ( R1 ` suc ( rank ` y ) ) ) )
11 10 rspcv 
 |-  ( suc ( rank ` y ) e. On -> ( A. u e. On E. w e. On ( F ` w ) We ( R1 ` u ) -> E. w e. On ( F ` w ) We ( R1 ` suc ( rank ` y ) ) ) )
12 5 6 11 mpsyl 
 |-  ( ph -> E. w e. On ( F ` w ) We ( R1 ` suc ( rank ` y ) ) )
13 12 alrimiv 
 |-  ( ph -> A. y E. w e. On ( F ` w ) We ( R1 ` suc ( rank ` y ) ) )
14 vex 
 |-  v e. _V
15 14 rankr1 
 |-  ( ( rank ` y ) = ( rank ` v ) <-> ( -. v e. ( R1 ` ( rank ` y ) ) /\ v e. ( R1 ` suc ( rank ` y ) ) ) )
16 15 simprbi 
 |-  ( ( rank ` y ) = ( rank ` v ) -> v e. ( R1 ` suc ( rank ` y ) ) )
17 16 eqcoms 
 |-  ( ( rank ` v ) = ( rank ` y ) -> v e. ( R1 ` suc ( rank ` y ) ) )
18 17 rgenw 
 |-  A. v e. _V ( ( rank ` v ) = ( rank ` y ) -> v e. ( R1 ` suc ( rank ` y ) ) )
19 rabss 
 |-  ( { v e. _V | ( rank ` v ) = ( rank ` y ) } C_ ( R1 ` suc ( rank ` y ) ) <-> A. v e. _V ( ( rank ` v ) = ( rank ` y ) -> v e. ( R1 ` suc ( rank ` y ) ) ) )
20 18 19 mpbir 
 |-  { v e. _V | ( rank ` v ) = ( rank ` y ) } C_ ( R1 ` suc ( rank ` y ) )
21 nfcv 
 |-  F/_ w F
22 nfrab1 
 |-  F/_ w { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) }
23 22 nfint 
 |-  F/_ w |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) }
24 21 23 nffv 
 |-  F/_ w ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
25 2 24 nfcxfr 
 |-  F/_ w S
26 nfcv 
 |-  F/_ w ( R1 ` suc ( rank ` y ) )
27 25 26 nfwe 
 |-  F/ w S We ( R1 ` suc ( rank ` y ) )
28 fveq2 
 |-  ( w = |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } -> ( F ` w ) = ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) )
29 28 2 eqtr4di 
 |-  ( w = |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } -> ( F ` w ) = S )
30 eqidd 
 |-  ( w = |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } -> ( R1 ` suc ( rank ` y ) ) = ( R1 ` suc ( rank ` y ) ) )
31 29 30 weeq12d 
 |-  ( w = |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } -> ( ( F ` w ) We ( R1 ` suc ( rank ` y ) ) <-> S We ( R1 ` suc ( rank ` y ) ) ) )
32 27 31 onminsb 
 |-  ( E. w e. On ( F ` w ) We ( R1 ` suc ( rank ` y ) ) -> S We ( R1 ` suc ( rank ` y ) ) )
33 wess 
 |-  ( { v e. _V | ( rank ` v ) = ( rank ` y ) } C_ ( R1 ` suc ( rank ` y ) ) -> ( S We ( R1 ` suc ( rank ` y ) ) -> S We { v e. _V | ( rank ` v ) = ( rank ` y ) } ) )
34 20 32 33 mpsyl 
 |-  ( E. w e. On ( F ` w ) We ( R1 ` suc ( rank ` y ) ) -> S We { v e. _V | ( rank ` v ) = ( rank ` y ) } )
35 34 alimi 
 |-  ( A. y E. w e. On ( F ` w ) We ( R1 ` suc ( rank ` y ) ) -> A. y S We { v e. _V | ( rank ` v ) = ( rank ` y ) } )
36 ralv 
 |-  ( A. y e. _V S We { v e. _V | ( rank ` v ) = ( rank ` y ) } <-> A. y S We { v e. _V | ( rank ` v ) = ( rank ` y ) } )
37 eqidd 
 |-  ( q = ( rank ` y ) -> ( F ` w ) = ( F ` w ) )
38 suceq 
 |-  ( q = ( rank ` y ) -> suc q = suc ( rank ` y ) )
39 38 fveq2d 
 |-  ( q = ( rank ` y ) -> ( R1 ` suc q ) = ( R1 ` suc ( rank ` y ) ) )
40 37 39 weeq12d 
 |-  ( q = ( rank ` y ) -> ( ( F ` w ) We ( R1 ` suc q ) <-> ( F ` w ) We ( R1 ` suc ( rank ` y ) ) ) )
41 40 rabbidv 
 |-  ( q = ( rank ` y ) -> { w e. On | ( F ` w ) We ( R1 ` suc q ) } = { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
42 41 inteqd 
 |-  ( q = ( rank ` y ) -> |^| { w e. On | ( F ` w ) We ( R1 ` suc q ) } = |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
43 42 fveq2d 
 |-  ( q = ( rank ` y ) -> ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc q ) } ) = ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) )
44 43 2 eqtr4di 
 |-  ( q = ( rank ` y ) -> ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc q ) } ) = S )
45 eqidd 
 |-  ( t = y -> ( F ` w ) = ( F ` w ) )
46 fveq2 
 |-  ( t = y -> ( rank ` t ) = ( rank ` y ) )
47 46 suceqd 
 |-  ( t = y -> suc ( rank ` t ) = suc ( rank ` y ) )
48 47 fveq2d 
 |-  ( t = y -> ( R1 ` suc ( rank ` t ) ) = ( R1 ` suc ( rank ` y ) ) )
49 45 48 weeq12d 
 |-  ( t = y -> ( ( F ` w ) We ( R1 ` suc ( rank ` t ) ) <-> ( F ` w ) We ( R1 ` suc ( rank ` y ) ) ) )
50 49 rabbidv 
 |-  ( t = y -> { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` t ) ) } = { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
51 50 inteqd 
 |-  ( t = y -> |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` t ) ) } = |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } )
52 51 fveq2d 
 |-  ( t = y -> ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` t ) ) } ) = ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` y ) ) } ) )
53 52 2 eqtr4di 
 |-  ( t = y -> ( F ` |^| { w e. On | ( F ` w ) We ( R1 ` suc ( rank ` t ) ) } ) = S )
54 1 44 53 werankwe 
 |-  ( A. y e. _V S We { v e. _V | ( rank ` v ) = ( rank ` y ) } -> R We _V )
55 36 54 sylbir 
 |-  ( A. y S We { v e. _V | ( rank ` v ) = ( rank ` y ) } -> R We _V )
56 13 35 55 3syl 
 |-  ( ph -> R We _V )