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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rankelb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ) )
2	1	3ad2ant2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ) )
3		limord	⊢ ( Lim 𝐵 → Ord 𝐵 )
4		ordtr1	⊢ ( Ord 𝐵 → ( ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
5	3 4	syl	⊢ ( Lim 𝐵 → ( ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
6	5	3ad2ant3	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ) → ( ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
7	2 6	syland	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝐴 ) ∈ 𝐵 ) → ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
8	7	expcomd	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ 𝐵 ) ) )
9	8	ralrimdv	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
10		rankfilimbi	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ∧ Lim 𝐵 ) ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )
11	10	3impb	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ∧ Lim 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )
12	11	3com23	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ Lim 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )
13	12	3expia	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ Lim 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
14	13	3impa	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
15	9 14	impbid	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ Lim 𝐵 ) → ( ( rank ‘ 𝐴 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ) )