Metamath Proof Explorer

Theorem rankval4

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. (Contributed by NM, 12-Oct-2003)

Ref Expression
Hypothesis rankr1b.1 ⊢ 𝐴 ∈ V
Assertion rankval4 ( rank ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 )

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ 𝐴 ∈ V
2 nfcv ⊢ Ⅎ 𝑥 𝐴
3 nfcv ⊢ Ⅎ 𝑥 𝑅1
4 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 )
5 3 4 nffv ⊢ Ⅎ 𝑥 ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
6 2 5 dfss2f ⊢ ( 𝐴 ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
7 vex ⊢ 𝑥 ∈ V
8 7 rankid ⊢ 𝑥 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) )
9 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → suc ( rank ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
10 rankon ⊢ ( rank ‘ 𝑥 ) ∈ On
11 10 onsuci ⊢ suc ( rank ‘ 𝑥 ) ∈ On
12 11 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On
13 iunon ⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On ) → ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On )
14 1 12 13 mp2an ⊢ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On
15 r1ord3 ⊢ ( ( suc ( rank ‘ 𝑥 ) ∈ On ∧ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On ) → ( suc ( rank ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
16 11 14 15 mp2an ⊢ ( suc ( rank ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) → ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) )
17 9 16 syl ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) )
18 17 sseld ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝑥 ) ) → 𝑥 ∈ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
19 8 18 mpi ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) )
20 6 19 mpgbir ⊢ 𝐴 ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
21 fvex ⊢ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ∈ V
22 21 rankss ⊢ ( 𝐴 ⊆ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) )
23 20 22 ax-mp ⊢ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) )
24 r1ord3 ⊢ ( ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On ∧ 𝑦 ∈ On ) → ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 → ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) ) )
25 14 24 mpan ⊢ ( 𝑦 ∈ On → ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 → ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) ) )
26 25 ss2rabi ⊢ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } ⊆ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) }
27 intss ⊢ ( { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } ⊆ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } → ∩ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } ⊆ ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } )
28 26 27 ax-mp ⊢ ∩ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } ⊆ ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 }
29 rankval2 ⊢ ( ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ∈ V → ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) = ∩ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) } )
30 21 29 ax-mp ⊢ ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) = ∩ { 𝑦 ∈ On ∣ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ⊆ ( 𝑅1 ‘ 𝑦 ) }
31 intmin ⊢ ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ∈ On → ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) )
32 14 31 ax-mp ⊢ ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 } = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 )
33 32 eqcomi ⊢ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) = ∩ { 𝑦 ∈ On ∣ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ 𝑦 }
34 28 30 33 3sstr4i ⊢ ( rank ‘ ( 𝑅1 ‘ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ) ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 )
35 23 34 sstri ⊢ ( rank ‘ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 )
36 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) )
37 1 rankel ⊢ ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) )
38 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
39 10 38 onsucssi ⊢ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝐴 ) ↔ suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) )
40 37 39 sylib ⊢ ( 𝑥 ∈ 𝐴 → suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 ) )
41 36 40 mprgbir ⊢ ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝐴 )
42 35 41 eqssi ⊢ ( rank ‘ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 suc ( rank ‘ 𝑥 )