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 ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → rank ⁡ A ∈ B ↔ ∀ x ∈ A rank ⁡ x ∈ B

Proof

Step Hyp Ref Expression
1 rankelb ⊢ A ∈ ⋃ R1 On → x ∈ A → rank ⁡ x ∈ rank ⁡ A
2 1 3ad2ant2 ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → x ∈ A → rank ⁡ x ∈ rank ⁡ A
3 limord ⊢ Lim ⁡ B → Ord ⁡ B
4 ordtr1 ⊢ Ord ⁡ B → rank ⁡ x ∈ rank ⁡ A ∧ rank ⁡ A ∈ B → rank ⁡ x ∈ B
5 3 4 syl ⊢ Lim ⁡ B → rank ⁡ x ∈ rank ⁡ A ∧ rank ⁡ A ∈ B → rank ⁡ x ∈ B
6 5 3ad2ant3 ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → rank ⁡ x ∈ rank ⁡ A ∧ rank ⁡ A ∈ B → rank ⁡ x ∈ B
7 2 6 syland ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → x ∈ A ∧ rank ⁡ A ∈ B → rank ⁡ x ∈ B
8 7 expcomd ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → rank ⁡ A ∈ B → x ∈ A → rank ⁡ x ∈ B
9 8 ralrimdv ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → rank ⁡ A ∈ B → ∀ x ∈ A rank ⁡ x ∈ B
10 rankfilimbi ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ ∀ x ∈ A rank ⁡ x ∈ B ∧ Lim ⁡ B → rank ⁡ A ∈ B
11 10 3impb ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ ∀ x ∈ A rank ⁡ x ∈ B ∧ Lim ⁡ B → rank ⁡ A ∈ B
12 11 3com23 ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B ∧ ∀ x ∈ A rank ⁡ x ∈ B → rank ⁡ A ∈ B
13 12 3expia ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → ∀ x ∈ A rank ⁡ x ∈ B → rank ⁡ A ∈ B
14 13 3impa ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → ∀ x ∈ A rank ⁡ x ∈ B → rank ⁡ A ∈ B
15 9 14 impbid ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ Lim ⁡ B → rank ⁡ A ∈ B ↔ ∀ x ∈ A rank ⁡ x ∈ B