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 𝐵 ) ) ) )