Metamath Proof Explorer

Theorem rankuni2b

Description: The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 8-Jun-2013)

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

Proof

Step Hyp Ref Expression
1 uniwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
2 rankval3b ⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) = ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } )
3 1 2 sylbi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) = ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } )
4 eleq2 ⊢ ( 𝑧 = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) → ( ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
5 4 ralbidv ⊢ ( 𝑧 = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) → ( ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
6 iuneq1 ⊢ ( 𝑦 = 𝐴 → ∪ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
7 6 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ∪ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On ↔ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ On ) )
8 vex ⊢ 𝑦 ∈ V
9 rankon ⊢ ( rank ‘ 𝑥 ) ∈ On
10 9 rgenw ⊢ ∀ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On
11 iunon ⊢ ( ( 𝑦 ∈ V ∧ ∀ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On ) → ∪ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On )
12 8 10 11 mp2an ⊢ ∪ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On
13 7 12 vtoclg ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ On )
14 eluni2 ⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 )
15 nfv ⊢ Ⅎ 𝑥 𝐴 ∈ ∪ ( 𝑅1 “ On )
16 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
17 16 nfel2 ⊢ Ⅎ 𝑥 ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
18 r1elssi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
19 18 sseld ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) )
20 rankelb ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑦 ∈ 𝑥 → ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑥 ) ) )
21 19 20 syl6 ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑥 ) ) ) )
22 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
23 22 sseld ⊢ ( 𝑥 ∈ 𝐴 → ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑥 ) → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
24 23 a1i ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑥 ) → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) ) )
25 21 24 syldd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) ) )
26 15 17 25 rexlimd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
27 14 26 syl5bi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑦 ∈ ∪ 𝐴 → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
28 27 ralrimiv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
29 5 13 28 elrabd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } )
30 intss1 ⊢ ( ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } → ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } ⊆ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
31 29 30 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } ⊆ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
32 3 31 eqsstrd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
33 1 biimpi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
34 elssuni ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴 )
35 rankssb ⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ⊆ ∪ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) ) )
36 33 34 35 syl2im ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) ) )
37 36 ralrimiv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) )
38 iunss ⊢ ( ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) )
39 37 38 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) )
40 32 39 eqssd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )