Metamath Proof Explorer

Theorem rankfilimbi

Description: If all elements in a finite well-founded set have a rank less than a limit ordinal, then the rank of that set is also less than the limit ordinal. (Contributed by BTernaryTau, 19-Jan-2026)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ ( A. x e. A ( rank ` x ) e. B /\ Lim B ) ) -> ( A e. Fin /\ A e. U. ( R1 " On ) ) )
2 limsuc 
 |-  ( Lim B -> ( ( rank ` x ) e. B <-> suc ( rank ` x ) e. B ) )
3 2 ralbidv 
 |-  ( Lim B -> ( A. x e. A ( rank ` x ) e. B <-> A. x e. A suc ( rank ` x ) e. B ) )
4 3 biimpd 
 |-  ( Lim B -> ( A. x e. A ( rank ` x ) e. B -> A. x e. A suc ( rank ` x ) e. B ) )
5 fvex 
 |-  ( rank ` x ) e. _V
6 5 sucex 
 |-  suc ( rank ` x ) e. _V
7 6 rgenw 
 |-  A. x e. A suc ( rank ` x ) e. _V
8 uniiunlem 
 |-  ( A. x e. A suc ( rank ` x ) e. _V -> ( A. x e. A suc ( rank ` x ) e. B <-> { z | E. x e. A z = suc ( rank ` x ) } C_ B ) )
9 7 8 ax-mp 
 |-  ( A. x e. A suc ( rank ` x ) e. B <-> { z | E. x e. A z = suc ( rank ` x ) } C_ B )
10 4 9 imbitrdi 
 |-  ( Lim B -> ( A. x e. A ( rank ` x ) e. B -> { z | E. x e. A z = suc ( rank ` x ) } C_ B ) )
11 10 impcom 
 |-  ( ( A. x e. A ( rank ` x ) e. B /\ Lim B ) -> { z | E. x e. A z = suc ( rank ` x ) } C_ B )
12 11 adantl 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ ( A. x e. A ( rank ` x ) e. B /\ Lim B ) ) -> { z | E. x e. A z = suc ( rank ` x ) } C_ B )
13 limord 
 |-  ( Lim B -> Ord B )
14 0ellim 
 |-  ( Lim B -> (/) e. B )
15 14 ne0d 
 |-  ( Lim B -> B =/= (/) )
16 13 15 jca 
 |-  ( Lim B -> ( Ord B /\ B =/= (/) ) )
17 16 ad2antll 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ ( A. x e. A ( rank ` x ) e. B /\ Lim B ) ) -> ( Ord B /\ B =/= (/) ) )
18 rankval4b 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = U_ x e. A suc ( rank ` x ) )
19 6 dfiun2 
 |-  U_ x e. A suc ( rank ` x ) = U. { z | E. x e. A z = suc ( rank ` x ) }
20 18 19 eqtrdi 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = U. { z | E. x e. A z = suc ( rank ` x ) } )
21 20 adantl 
 |-  ( ( A e. Fin /\ A e. U. ( R1 " On ) ) -> ( rank ` A ) = U. { z | E. x e. A z = suc ( rank ` x ) } )
22 21 3ad2ant1 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ { z | E. x e. A z = suc ( rank ` x ) } C_ B /\ ( Ord B /\ B =/= (/) ) ) -> ( rank ` A ) = U. { z | E. x e. A z = suc ( rank ` x ) } )
23 abrexfi 
 |-  ( A e. Fin -> { z | E. x e. A z = suc ( rank ` x ) } e. Fin )
24 fissorduni 
 |-  ( ( { z | E. x e. A z = suc ( rank ` x ) } e. Fin /\ { z | E. x e. A z = suc ( rank ` x ) } C_ B /\ ( Ord B /\ B =/= (/) ) ) -> U. { z | E. x e. A z = suc ( rank ` x ) } e. B )
25 23 24 syl3an1 
 |-  ( ( A e. Fin /\ { z | E. x e. A z = suc ( rank ` x ) } C_ B /\ ( Ord B /\ B =/= (/) ) ) -> U. { z | E. x e. A z = suc ( rank ` x ) } e. B )
26 25 3adant1r 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ { z | E. x e. A z = suc ( rank ` x ) } C_ B /\ ( Ord B /\ B =/= (/) ) ) -> U. { z | E. x e. A z = suc ( rank ` x ) } e. B )
27 22 26 eqeltrd 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ { z | E. x e. A z = suc ( rank ` x ) } C_ B /\ ( Ord B /\ B =/= (/) ) ) -> ( rank ` A ) e. B )
28 1 12 17 27 syl3anc 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ ( A. x e. A ( rank ` x ) e. B /\ Lim B ) ) -> ( rank ` A ) e. B )