This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 r1funlim ⊢ ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
11 10 simpri ⊢ Lim dom 𝑅1
12 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
13 ordtr1 ⊢ ( Ord dom 𝑅1 → ( ( 𝑥 ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 ) )
14 11 12 13 mp2b ⊢ ( ( 𝑥 ∈ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) → 𝑥 ∈ dom 𝑅1 )
15 9 14 mpan2 ⊢ ( 𝑥 ∈ ( rank ‘ 𝐴 ) → 𝑥 ∈ dom 𝑅1 )
16 15 ad2antlr ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ dom 𝑅1 )
17 rankr1ag ⊢ ( ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ dom 𝑅1 ) → ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝑦 ) ∈ 𝑥 ) )
18 8 16 17 syl2anc ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝑦 ) ∈ 𝑥 ) )
19 18 ralbidva ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) )
20 19 biimpar ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
21 20 an32s ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
22 dfss3 ⊢ ( 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) )
23 21 22 sylibr ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) )
24 simpll ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
25 15 adantl ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → 𝑥 ∈ dom 𝑅1 )
26 rankr1bg ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑥 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
27 24 25 26 syl2anc ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
28 23 27 mpbid ⊢ ( ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ∧ 𝑥 ∈ ( rank ‘ 𝐴 ) ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 )
29 28 ex ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ( 𝑥 ∈ ( rank ‘ 𝐴 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
30 29 adantrl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → ( 𝑥 ∈ ( rank ‘ 𝐴 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
31 5 30 sylbird ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → ( ¬ ( rank ‘ 𝐴 ) ⊆ 𝑥 → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
32 31 pm2.18d ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 )
33 32 ex ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
34 33 alrimiv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
35 ssintab ⊢ ( ( rank ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) } ↔ ∀ 𝑥 ( ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) → ( rank ‘ 𝐴 ) ⊆ 𝑥 ) )
36 34 35 sylibr ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) } )
37 df-rab ⊢ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } = { 𝑥 ∣ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) }
38 37 inteqi ⊢ ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } = ∩ { 𝑥 ∣ ( 𝑥 ∈ On ∧ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ) }
39 36 38 sseqtrrdi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } )
40 rankelb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑦 ∈ 𝐴 → ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) ) )
41 40 ralrimiv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) )
42 eleq2 ⊢ ( 𝑥 = ( rank ‘ 𝐴 ) → ( ( rank ‘ 𝑦 ) ∈ 𝑥 ↔ ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) ) )
43 42 ralbidv ⊢ ( 𝑥 = ( rank ‘ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) ) )
44 43 onintss ⊢ ( ( rank ‘ 𝐴 ) ∈ On → ( ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝐴 ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } ⊆ ( rank ‘ 𝐴 ) ) )
45 1 41 44 mpsyl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } ⊆ ( rank ‘ 𝐴 ) )
46 39 45 eqssd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑥 } )