Metamath Proof Explorer

Theorem rankfilimbi

Description: If all elements of 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 ∈ Fin ∧ A ∈ ⋃ R1 On ∧ ∀ x ∈ A rank ⁡ x ∈ B ∧ Lim ⁡ B → rank ⁡ A ∈ B

Proof

Step Hyp Ref Expression
1 simpl ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ ∀ x ∈ A rank ⁡ x ∈ B ∧ Lim ⁡ B → A ∈ Fin ∧ A ∈ ⋃ R1 On
2 limsuc ⊢ Lim ⁡ B → rank ⁡ x ∈ B ↔ suc ⁡ rank ⁡ x ∈ B
3 2 ralbidv ⊢ Lim ⁡ B → ∀ x ∈ A rank ⁡ x ∈ B ↔ ∀ x ∈ A suc ⁡ rank ⁡ x ∈ B
4 3 biimpd ⊢ Lim ⁡ B → ∀ x ∈ A rank ⁡ x ∈ B → ∀ x ∈ A suc ⁡ rank ⁡ x ∈ B
5 fvex ⊢ rank ⁡ x ∈ V
6 5 sucex ⊢ suc ⁡ rank ⁡ x ∈ V
7 6 rgenw ⊢ ∀ x ∈ A suc ⁡ rank ⁡ x ∈ V
8 uniiunlem ⊢ ∀ x ∈ A suc ⁡ rank ⁡ x ∈ V → ∀ x ∈ A suc ⁡ rank ⁡ x ∈ B ↔ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B
9 7 8 ax-mp ⊢ ∀ x ∈ A suc ⁡ rank ⁡ x ∈ B ↔ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B
10 4 9 imbitrdi ⊢ Lim ⁡ B → ∀ x ∈ A rank ⁡ x ∈ B → z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B
11 10 impcom ⊢ ∀ x ∈ A rank ⁡ x ∈ B ∧ Lim ⁡ B → z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B
12 11 adantl ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ ∀ x ∈ A rank ⁡ x ∈ B ∧ Lim ⁡ B → z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B
13 limord ⊢ Lim ⁡ B → Ord ⁡ B
14 0ellim ⊢ Lim ⁡ B → ∅ ∈ B
15 14 ne0d ⊢ Lim ⁡ B → B ≠ ∅
16 13 15 jca ⊢ Lim ⁡ B → Ord ⁡ B ∧ B ≠ ∅
17 16 ad2antll ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ ∀ x ∈ A rank ⁡ x ∈ B ∧ Lim ⁡ B → Ord ⁡ B ∧ B ≠ ∅
18 rankval4b ⊢ A ∈ ⋃ R1 On → rank ⁡ A = ⋃ x ∈ A suc ⁡ rank ⁡ x
19 6 dfiun2 ⊢ ⋃ x ∈ A suc ⁡ rank ⁡ x = ⋃ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x
20 18 19 eqtrdi ⊢ A ∈ ⋃ R1 On → rank ⁡ A = ⋃ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x
21 20 adantl ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On → rank ⁡ A = ⋃ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x
22 21 3ad2ant1 ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → rank ⁡ A = ⋃ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x
23 abrexfi ⊢ A ∈ Fin → z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ∈ Fin
24 fissorduni ⊢ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ∈ Fin ∧ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → ⋃ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ∈ B
25 23 24 syl3an1 ⊢ A ∈ Fin ∧ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → ⋃ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ∈ B
26 25 3adant1r ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → ⋃ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ∈ B
27 22 26 eqeltrd ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ z | ∃ x ∈ A z = suc ⁡ rank ⁡ x ⊆ B ∧ Ord ⁡ B ∧ B ≠ ∅ → rank ⁡ A ∈ B
28 1 12 17 27 syl3anc ⊢ A ∈ Fin ∧ A ∈ ⋃ R1 On ∧ ∀ x ∈ A rank ⁡ x ∈ B ∧ Lim ⁡ B → rank ⁡ A ∈ B