Metamath Proof Explorer


Theorem rankr1c

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1 . Proposition 9.15(2) of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankr1c ( 𝐴 ( 𝑅1 “ On ) → ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅1𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 id ( 𝐵 = ( rank ‘ 𝐴 ) → 𝐵 = ( rank ‘ 𝐴 ) )
2 rankdmr1 ( rank ‘ 𝐴 ) ∈ dom 𝑅1
3 1 2 eqeltrdi ( 𝐵 = ( rank ‘ 𝐴 ) → 𝐵 ∈ dom 𝑅1 )
4 3 a1i ( 𝐴 ( 𝑅1 “ On ) → ( 𝐵 = ( rank ‘ 𝐴 ) → 𝐵 ∈ dom 𝑅1 ) )
5 elfvdm ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → suc 𝐵 ∈ dom 𝑅1 )
6 r1funlim ( Fun 𝑅1 ∧ Lim dom 𝑅1 )
7 6 simpri Lim dom 𝑅1
8 limsuc ( Lim dom 𝑅1 → ( 𝐵 ∈ dom 𝑅1 ↔ suc 𝐵 ∈ dom 𝑅1 ) )
9 7 8 ax-mp ( 𝐵 ∈ dom 𝑅1 ↔ suc 𝐵 ∈ dom 𝑅1 )
10 5 9 sylibr ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → 𝐵 ∈ dom 𝑅1 )
11 10 adantl ( ( ¬ 𝐴 ∈ ( 𝑅1𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) → 𝐵 ∈ dom 𝑅1 )
12 11 a1i ( 𝐴 ( 𝑅1 “ On ) → ( ( ¬ 𝐴 ∈ ( 𝑅1𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) → 𝐵 ∈ dom 𝑅1 ) )
13 eqss ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
14 rankr1clem ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ¬ 𝐴 ∈ ( 𝑅1𝐵 ) ↔ 𝐵 ⊆ ( rank ‘ 𝐴 ) ) )
15 rankr1ag ( ( 𝐴 ( 𝑅1 “ On ) ∧ suc 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
16 9 15 sylan2b ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
17 rankon ( rank ‘ 𝐴 ) ∈ On
18 limord ( Lim dom 𝑅1 → Ord dom 𝑅1 )
19 7 18 ax-mp Ord dom 𝑅1
20 ordelon ( ( Ord dom 𝑅1𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
21 19 20 mpan ( 𝐵 ∈ dom 𝑅1𝐵 ∈ On )
22 21 adantl ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
23 onsssuc ( ( ( rank ‘ 𝐴 ) ∈ On ∧ 𝐵 ∈ On ) → ( ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
24 17 22 23 sylancr ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
25 16 24 bitr4d ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
26 14 25 anbi12d ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( ¬ 𝐴 ∈ ( 𝑅1𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ↔ ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) ) )
27 13 26 bitr4id ( ( 𝐴 ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅1𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) )
28 27 ex ( 𝐴 ( 𝑅1 “ On ) → ( 𝐵 ∈ dom 𝑅1 → ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅1𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) ) )
29 4 12 28 pm5.21ndd ( 𝐴 ( 𝑅1 “ On ) → ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅1𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) )