Metamath Proof Explorer

Theorem r1filimi

Description: If all elements in a finite set appear in the cumulative hierarchy prior to a limit ordinal, then that set also appears in the cumulative hierarchy prior to the limit ordinal. (Contributed by BTernaryTau, 19-Jan-2026)

Ref Expression
Assertion r1filimi 
|- ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A e. U. ( R1 " B ) )

Proof

Step Hyp Ref Expression
1 raleq 
 |-  ( a = A -> ( A. x e. a x e. U. ( R1 " B ) <-> A. x e. A x e. U. ( R1 " B ) ) )
2 eleq1 
 |-  ( a = A -> ( a e. U. ( R1 " On ) <-> A e. U. ( R1 " On ) ) )
3 1 2 imbi12d 
 |-  ( a = A -> ( ( A. x e. a x e. U. ( R1 " B ) -> a e. U. ( R1 " On ) ) <-> ( A. x e. A x e. U. ( R1 " B ) -> A e. U. ( R1 " On ) ) ) )
4 3 imbi2d 
 |-  ( a = A -> ( ( Lim B -> ( A. x e. a x e. U. ( R1 " B ) -> a e. U. ( R1 " On ) ) ) <-> ( Lim B -> ( A. x e. A x e. U. ( R1 " B ) -> A e. U. ( R1 " On ) ) ) ) )
5 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
6 5 simpli 
 |-  Fun R1
7 eluniima 
 |-  ( Fun R1 -> ( x e. U. ( R1 " B ) <-> E. y e. B x e. ( R1 ` y ) ) )
8 6 7 ax-mp 
 |-  ( x e. U. ( R1 " B ) <-> E. y e. B x e. ( R1 ` y ) )
9 limord 
 |-  ( Lim B -> Ord B )
10 ordsson 
 |-  ( Ord B -> B C_ On )
11 9 10 syl 
 |-  ( Lim B -> B C_ On )
12 11 sseld 
 |-  ( Lim B -> ( y e. B -> y e. On ) )
13 12 anim1d 
 |-  ( Lim B -> ( ( y e. B /\ x e. ( R1 ` y ) ) -> ( y e. On /\ x e. ( R1 ` y ) ) ) )
14 13 reximdv2 
 |-  ( Lim B -> ( E. y e. B x e. ( R1 ` y ) -> E. y e. On x e. ( R1 ` y ) ) )
15 8 14 biimtrid 
 |-  ( Lim B -> ( x e. U. ( R1 " B ) -> E. y e. On x e. ( R1 ` y ) ) )
16 15 ralimdv 
 |-  ( Lim B -> ( A. x e. a x e. U. ( R1 " B ) -> A. x e. a E. y e. On x e. ( R1 ` y ) ) )
17 vex 
 |-  a e. _V
18 17 tz9.12 
 |-  ( A. x e. a E. y e. On x e. ( R1 ` y ) -> E. y e. On a e. ( R1 ` y ) )
19 eluniima 
 |-  ( Fun R1 -> ( a e. U. ( R1 " On ) <-> E. y e. On a e. ( R1 ` y ) ) )
20 6 19 ax-mp 
 |-  ( a e. U. ( R1 " On ) <-> E. y e. On a e. ( R1 ` y ) )
21 18 20 sylibr 
 |-  ( A. x e. a E. y e. On x e. ( R1 ` y ) -> a e. U. ( R1 " On ) )
22 16 21 syl6 
 |-  ( Lim B -> ( A. x e. a x e. U. ( R1 " B ) -> a e. U. ( R1 " On ) ) )
23 4 22 vtoclg 
 |-  ( A e. Fin -> ( Lim B -> ( A. x e. A x e. U. ( R1 " B ) -> A e. U. ( R1 " On ) ) ) )
24 23 impcomd 
 |-  ( A e. Fin -> ( ( A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A e. U. ( R1 " On ) ) )
25 24 3impib 
 |-  ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A e. U. ( R1 " On ) )
26 simp3 
 |-  ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> Lim B )
27 simp1 
 |-  ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A e. Fin )
28 eluniima 
 |-  ( Fun R1 -> ( x e. U. ( R1 " B ) <-> E. z e. B x e. ( R1 ` z ) ) )
29 6 28 ax-mp 
 |-  ( x e. U. ( R1 " B ) <-> E. z e. B x e. ( R1 ` z ) )
30 df-rex 
 |-  ( E. z e. B x e. ( R1 ` z ) <-> E. z ( z e. B /\ x e. ( R1 ` z ) ) )
31 rankr1ai 
 |-  ( x e. ( R1 ` z ) -> ( rank ` x ) e. z )
32 ordtr1 
 |-  ( Ord B -> ( ( ( rank ` x ) e. z /\ z e. B ) -> ( rank ` x ) e. B ) )
33 31 32 sylani 
 |-  ( Ord B -> ( ( x e. ( R1 ` z ) /\ z e. B ) -> ( rank ` x ) e. B ) )
34 33 ancomsd 
 |-  ( Ord B -> ( ( z e. B /\ x e. ( R1 ` z ) ) -> ( rank ` x ) e. B ) )
35 34 exlimdv 
 |-  ( Ord B -> ( E. z ( z e. B /\ x e. ( R1 ` z ) ) -> ( rank ` x ) e. B ) )
36 30 35 biimtrid 
 |-  ( Ord B -> ( E. z e. B x e. ( R1 ` z ) -> ( rank ` x ) e. B ) )
37 29 36 biimtrid 
 |-  ( Ord B -> ( x e. U. ( R1 " B ) -> ( rank ` x ) e. B ) )
38 37 ralimdv 
 |-  ( Ord B -> ( A. x e. A x e. U. ( R1 " B ) -> A. x e. A ( rank ` x ) e. B ) )
39 9 38 syl 
 |-  ( Lim B -> ( A. x e. A x e. U. ( R1 " B ) -> A. x e. A ( rank ` x ) e. B ) )
40 39 impcom 
 |-  ( ( A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A. x e. A ( rank ` x ) e. B )
41 40 3adant1 
 |-  ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A. x e. A ( rank ` x ) e. B )
42 rankfilimbi 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ ( A. x e. A ( rank ` x ) e. B /\ Lim B ) ) -> ( rank ` A ) e. B )
43 27 25 41 26 42 syl22anc 
 |-  ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> ( rank ` A ) e. B )
44 fveq2 
 |-  ( w = suc ( rank ` A ) -> ( R1 ` w ) = ( R1 ` suc ( rank ` A ) ) )
45 44 eleq2d 
 |-  ( w = suc ( rank ` A ) -> ( A e. ( R1 ` w ) <-> A e. ( R1 ` suc ( rank ` A ) ) ) )
46 limsuc 
 |-  ( Lim B -> ( ( rank ` A ) e. B <-> suc ( rank ` A ) e. B ) )
47 46 biimpa 
 |-  ( ( Lim B /\ ( rank ` A ) e. B ) -> suc ( rank ` A ) e. B )
48 47 3adant1 
 |-  ( ( A e. U. ( R1 " On ) /\ Lim B /\ ( rank ` A ) e. B ) -> suc ( rank ` A ) e. B )
49 rankidb 
 |-  ( A e. U. ( R1 " On ) -> A e. ( R1 ` suc ( rank ` A ) ) )
50 49 3ad2ant1 
 |-  ( ( A e. U. ( R1 " On ) /\ Lim B /\ ( rank ` A ) e. B ) -> A e. ( R1 ` suc ( rank ` A ) ) )
51 45 48 50 rspcedvdw 
 |-  ( ( A e. U. ( R1 " On ) /\ Lim B /\ ( rank ` A ) e. B ) -> E. w e. B A e. ( R1 ` w ) )
52 eluniima 
 |-  ( Fun R1 -> ( A e. U. ( R1 " B ) <-> E. w e. B A e. ( R1 ` w ) ) )
53 6 52 ax-mp 
 |-  ( A e. U. ( R1 " B ) <-> E. w e. B A e. ( R1 ` w ) )
54 51 53 sylibr 
 |-  ( ( A e. U. ( R1 " On ) /\ Lim B /\ ( rank ` A ) e. B ) -> A e. U. ( R1 " B ) )
55 25 26 43 54 syl3anc 
 |-  ( ( A e. Fin /\ A. x e. A x e. U. ( R1 " B ) /\ Lim B ) -> A e. U. ( R1 " B ) )