Metamath Proof Explorer

Theorem rankval4b

Description: The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of Jech p. 72. Also a special case of Theorem 7V(b) of Enderton p. 204. This variant of rankval4 does not use Regularity, and so requires the assumption that A is in the range of R1 . (Contributed by BTernaryTau, 19-Jan-2026)

Ref Expression
Assertion rankval4b ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 r1wf ⊢ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ∈ ∪ ( 𝑅1 “ On )
2 rankon ⊢ ( rank ‘ 𝑥 ) ∈ On
3 2 onsuci ⊢ suc ( rank ‘ 𝑥 ) ∈ On
4 3 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On
5 iunon ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On ) → ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On )
6 4 5 mpan2 ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On )
7 r1ord3 ⊢ ( ( suc ( rank ‘ 𝑥 ) ∈ On ∧ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On ) → ( suc ( rank ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
8 3 6 7 sylancr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( suc ( rank ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
9 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → suc ( rank ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
10 8 9 impel ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) )
11 elwf ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
12 rankidb ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → 𝑥 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) )
13 11 12 syl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) )
14 10 13 sseldd ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) )
15 14 ex ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
16 15 alrimiv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
17 nfcv ⊢ Ⅎ 𝑥 𝐴
18 nfcv ⊢ Ⅎ 𝑥 𝑅1
19 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 )
20 18 19 nffv ⊢ Ⅎ 𝑥 ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
21 17 20 dfssf ⊢ ( 𝐴 ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
22 16 21 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) )
23 rankssb ⊢ ( ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) ) )
24 1 22 23 mpsyl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
25 r1ord3 ⊢ ( ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On ∧ 𝑦 ∈ On ) → ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 → ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) ) )
26 6 25 sylan ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑦 ∈ On ) → ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 → ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) ) )
27 26 ss2rabdv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } ⊆ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } )
28 intss ⊢ ( { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } ⊆ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } → ∩ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } ⊆ ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } )
29 27 28 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } ⊆ ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } )
30 rankval2b ⊢ ( ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) = ∩ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } )
31 1 30 mp1i ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) = ∩ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } )
32 intmin ⊢ ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On → ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
33 6 32 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
34 33 eqcomd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) = ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } )
35 29 31 34 3sstr4d ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
36 24 35 sstrd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
37 rankelb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ) )
38 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
39 2 38 onsucssi ⊢ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ↔ suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) )
40 37 39 imbitrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) ) )
41 40 ralrimiv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) )
42 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) )
43 41 42 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) )
44 36 43 eqssd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )