Metamath Proof Explorer

Theorem rankval3b

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, 17-Nov-2014)

Ref Expression
Assertion rankval3b ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } )

Proof

Step Hyp Ref Expression
1 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
2 simprl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → 𝑥 ∈ On )
3 ontri1 ⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ 𝑥 ∈ On ) → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ( rank ‘ 𝐴 ) ) )
4 1 2 3 sylancr ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → ( ( rank ‘ 𝐴 ) ⊆ 𝑥 ↔ ¬ 𝑥 ∈ ( rank ‘ 𝐴 ) ) )
5 4 con2bid ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → ( 𝑥 ∈ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
6 r1elssi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
8 7 sselda ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
9 rankdmr1 ⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
10 r1dmlim ⊢ Lim dom 𝑅1
11 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
12 ordtr1 ⊢ ( Ord dom 𝑅1 → ( ( 𝑥 ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 ) )
13 10 11 12 mp2b ⊢ ( ( 𝑥 ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 )
14 9 13 mpan2 ⊢ ( 𝑥 ∈ ( rank ‘ 𝐴 ) → 𝑥 ∈ dom 𝑅1 )
15 14 ad2antlr ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ dom 𝑅1 )
16 rankr1ag ⊢ ( ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ dom 𝑅1 ) → ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝑦 ) ∈ 𝑥 ) )
17 8 15 16 syl2anc ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝑦 ) ∈ 𝑥 ) )
18 17 ralbidva ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) )
19 18 biimpar ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
20 19 an32s ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
21 dfss3 ⊢ ( 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
22 20 21 sylibr ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) )
23 simpll ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
24 14 adantl ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → 𝑥 ∈ dom 𝑅1 )
25 rankr1bg ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
26 23 24 25 syl2anc ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
27 22 26 mpbid ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 )
28 27 ex ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ( 𝑥 ∈ ( rank ‘ 𝐴 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
29 28 adantrl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → ( 𝑥 ∈ ( rank ‘ 𝐴 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
30 5 29 sylbird ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → ( ¬ ( rank ‘ 𝐴 ) ⊆ 𝑥 → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
31 30 pm2.18d ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 )
32 31 ex ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
33 32 alrimiv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
34 ssintab ⊢ ( ( rank ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) } ↔ ∀ 𝑥 ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
35 33 34 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) } )
36 df-rab ⊢ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) }
37 36 inteqi ⊢ ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } = ∩ { 𝑥 ∣ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) }
38 35 37 sseqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } )
39 rankelb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑦 ∈ 𝐴 → ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) ) )
40 39 ralrimiv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) )
41 eleq2 ⊢ ( 𝑥 = ( rank ‘ 𝐴 ) → ( ( rank ‘ 𝑦 ) ∈ 𝑥 ↔ ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) ) )
42 41 ralbidv ⊢ ( 𝑥 = ( rank ‘ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) ) )
43 42 onintss ⊢ ( ( rank ‘ 𝐴 ) ∈ On → ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } ⊆ ( rank ‘ 𝐴 ) ) )
44 1 40 43 mpsyl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } ⊆ ( rank ‘ 𝐴 ) )
45 38 44 eqssd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } )