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 r1dmlim ⊢ Lim dom 𝑅1
7 limsuc ⊢ ( Lim dom 𝑅1 → ( 𝐵 ∈ dom 𝑅1 ↔ suc 𝐵 ∈ dom 𝑅1 ) )
8 6 7 ax-mp ⊢ ( 𝐵 ∈ dom 𝑅1 ↔ suc 𝐵 ∈ dom 𝑅1 )
9 5 8 sylibr ⊢ ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) → 𝐵 ∈ dom 𝑅1 )
10 9 adantl ⊢ ( ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) → 𝐵 ∈ dom 𝑅1 )
11 10 a1i ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) → 𝐵 ∈ dom 𝑅1 ) )
12 eqss ⊢ ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
13 rankr1clem ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐵 ⊆ ( rank ‘ 𝐴 ) ) )
14 rankr1ag ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ suc 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
15 8 14 sylan2b ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
16 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
17 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
18 6 17 ax-mp ⊢ Ord dom 𝑅1
19 ordelon ⊢ ( ( Ord dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
20 18 19 mpan ⊢ ( 𝐵 ∈ dom 𝑅1 → 𝐵 ∈ On )
21 20 adantl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
22 onsssuc ⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ 𝐵 ∈ On ) → ( ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
23 16 21 22 sylancr ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
24 15 23 bitr4d ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
25 13 24 anbi12d ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ↔ ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) ) )
26 12 25 bitr4id ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) )
27 26 ex ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐵 ∈ dom 𝑅1 → ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) ) )
28 4 11 27 pm5.21ndd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) ) )