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

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ∧ Lim 𝐵 ) ) → ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) )
2 limsuc ⊢ ( Lim 𝐵 → ( ( rank ‘ 𝑥 ) ∈ 𝐵 ↔ suc ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
3 2 ralbidv ⊢ ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
4 3 biimpd ⊢ ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ 𝐵 ) )
5 fvex ⊢ ( rank ‘ 𝑥 ) ∈ V
6 5 sucex ⊢ suc ( rank ‘ 𝑥 ) ∈ V
7 6 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ V
8 uniiunlem ⊢ ( ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ V → ( ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ 𝐵 ↔ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 ) )
9 7 8 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ 𝐵 ↔ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 )
10 4 9 imbitrdi ⊢ ( Lim 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 ) )
11 10 impcom ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ∧ Lim 𝐵 ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 )
12 11 adantl ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ∧ Lim 𝐵 ) ) → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 )
13 limord ⊢ ( Lim 𝐵 → Ord 𝐵 )
14 0ellim ⊢ ( Lim 𝐵 → ∅ ∈ 𝐵 )
15 14 ne0d ⊢ ( Lim 𝐵 → 𝐵 ≠ ∅ )
16 13 15 jca ⊢ ( Lim 𝐵 → ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ) )
17 16 ad2antll ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ∧ Lim 𝐵 ) ) → ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ) )
18 rankval4b ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
19 6 dfiun2 ⊢ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) }
20 18 19 eqtrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } )
21 20 adantl ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ 𝐴 ) = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } )
22 21 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 ∧ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ) ) → ( rank ‘ 𝐴 ) = ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } )
23 abrexfi ⊢ ( 𝐴 ∈ Fin → { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ∈ Fin )
24 fissorduni ⊢ ( ( { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ∈ Fin ∧ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 ∧ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ) ) → ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ∈ 𝐵 )
25 23 24 syl3an1 ⊢ ( ( 𝐴 ∈ Fin ∧ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 ∧ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ) ) → ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ∈ 𝐵 )
26 25 3adant1r ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 ∧ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ) ) → ∪ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ∈ 𝐵 )
27 22 26 eqeltrd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 𝑧 = suc ( rank ‘ 𝑥 ) } ⊆ 𝐵 ∧ ( Ord 𝐵 ∧ 𝐵 ≠ ∅ ) ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )
28 1 12 17 27 syl3anc ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) ∧ ( ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ 𝐵 ∧ Lim 𝐵 ) ) → ( rank ‘ 𝐴 ) ∈ 𝐵 )