Metamath Proof Explorer

Theorem rankr1bg

Description: A relationship between rank and R1 . See rankr1ag for the membership version. (Contributed by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankr1bg ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 r1dmlim ⊢ Lim dom 𝑅1
2 limsuc ⊢ ( Lim dom 𝑅1 → ( 𝐵 ∈ dom 𝑅1 ↔ suc 𝐵 ∈ dom 𝑅1 ) )
3 1 2 ax-mp ⊢ ( 𝐵 ∈ dom 𝑅1 ↔ suc 𝐵 ∈ dom 𝑅1 )
4 rankr1ag ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ suc 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
5 3 4 sylan2b ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
6 r1sucg ⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝑅1 ‘ suc 𝐵 ) = 𝒫 ( 𝑅1 ‘ 𝐵 ) )
7 6 adantl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝑅1 ‘ suc 𝐵 ) = 𝒫 ( 𝑅1 ‘ 𝐵 ) )
8 7 eleq2d ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝐵 ) ) )
9 fvex ⊢ ( 𝑅1 ‘ 𝐵 ) ∈ V
10 9 elpw2 ⊢ ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) )
11 8 10 bitr2di ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc 𝐵 ) ) )
12 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
13 limord ⊢ ( Lim dom 𝑅1 → Ord dom 𝑅1 )
14 1 13 ax-mp ⊢ Ord dom 𝑅1
15 ordelon ⊢ ( ( Ord dom 𝑅1 ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
16 14 15 mpan ⊢ ( 𝐵 ∈ dom 𝑅1 → 𝐵 ∈ On )
17 16 adantl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → 𝐵 ∈ On )
18 onsssuc ⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ 𝐵 ∈ On ) → ( ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
19 12 17 18 sylancr ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐴 ) ⊆ 𝐵 ↔ ( rank ‘ 𝐴 ) ∈ suc 𝐵 ) )
20 5 11 19 3bitr4d ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )