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

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