Metamath Proof Explorer

Theorem rankfilimb

Description: The rank of a finite well-founded set is less than a limit ordinal iff the ranks of all of its elements are less than that limit ordinal. (Contributed by BTernaryTau, 22-Jan-2026)

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

Proof

Step Hyp Ref Expression
1 rankelb 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) )
2 1 3ad2ant2 
 |-  ( ( A e. Fin /\ A e. U. ( R1 " On ) /\ Lim B ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) )
3 limord 
 |-  ( Lim B -> Ord B )
4 ordtr1 
 |-  ( Ord B -> ( ( ( rank ` x ) e. ( rank ` A ) /\ ( rank ` A ) e. B ) -> ( rank ` x ) e. B ) )
5 3 4 syl 
 |-  ( Lim B -> ( ( ( rank ` x ) e. ( rank ` A ) /\ ( rank ` A ) e. B ) -> ( rank ` x ) e. B ) )
6 5 3ad2ant3 
 |-  ( ( A e. Fin /\ A e. U. ( R1 " On ) /\ Lim B ) -> ( ( ( rank ` x ) e. ( rank ` A ) /\ ( rank ` A ) e. B ) -> ( rank ` x ) e. B ) )
7 2 6 syland 
 |-  ( ( A e. Fin /\ A e. U. ( R1 " On ) /\ Lim B ) -> ( ( x e. A /\ ( rank ` A ) e. B ) -> ( rank ` x ) e. B ) )
8 7 expcomd 
 |-  ( ( A e. Fin /\ A e. U. ( R1 " On ) /\ Lim B ) -> ( ( rank ` A ) e. B -> ( x e. A -> ( rank ` x ) e. B ) ) )
9 8 ralrimdv 
 |-  ( ( A e. Fin /\ A e. U. ( R1 " On ) /\ Lim B ) -> ( ( rank ` A ) e. B -> A. x e. A ( rank ` x ) e. B ) )
10 rankfilimbi 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ ( A. x e. A ( rank ` x ) e. B /\ Lim B ) ) -> ( rank ` A ) e. B )
11 10 3impb 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ A. x e. A ( rank ` x ) e. B /\ Lim B ) -> ( rank ` A ) e. B )
12 11 3com23 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ Lim B /\ A. x e. A ( rank ` x ) e. B ) -> ( rank ` A ) e. B )
13 12 3expia 
 |-  ( ( ( A e. Fin /\ A e. U. ( R1 " On ) ) /\ Lim B ) -> ( A. x e. A ( rank ` x ) e. B -> ( rank ` A ) e. B ) )
14 13 3impa 
 |-  ( ( A e. Fin /\ A e. U. ( R1 " On ) /\ Lim B ) -> ( A. x e. A ( rank ` x ) e. B -> ( rank ` A ) e. B ) )
15 9 14 impbid 
 |-  ( ( A e. Fin /\ A e. U. ( R1 " On ) /\ Lim B ) -> ( ( rank ` A ) e. B <-> A. x e. A ( rank ` x ) e. B ) )