Metamath Proof Explorer

Theorem r1filimi

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