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 ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to \left({A}\subseteq {R}_{1}\left({B}\right)↔\mathrm{rank}\left({A}\right)\subseteq {B}\right)$

Proof

Step Hyp Ref Expression
1 r1funlim ${⊢}\left(\mathrm{Fun}{R}_{1}\wedge \mathrm{Lim}\mathrm{dom}{R}_{1}\right)$
2 1 simpri ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}$
3 limsuc ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \left({B}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{B}\in \mathrm{dom}{R}_{1}\right)$
4 2 3 ax-mp ${⊢}{B}\in \mathrm{dom}{R}_{1}↔\mathrm{suc}{B}\in \mathrm{dom}{R}_{1}$
5 rankr1ag ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge \mathrm{suc}{B}\in \mathrm{dom}{R}_{1}\right)\to \left({A}\in {R}_{1}\left(\mathrm{suc}{B}\right)↔\mathrm{rank}\left({A}\right)\in \mathrm{suc}{B}\right)$
6 4 5 sylan2b ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to \left({A}\in {R}_{1}\left(\mathrm{suc}{B}\right)↔\mathrm{rank}\left({A}\right)\in \mathrm{suc}{B}\right)$
7 r1sucg ${⊢}{B}\in \mathrm{dom}{R}_{1}\to {R}_{1}\left(\mathrm{suc}{B}\right)=𝒫{R}_{1}\left({B}\right)$
8 7 adantl ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to {R}_{1}\left(\mathrm{suc}{B}\right)=𝒫{R}_{1}\left({B}\right)$
9 8 eleq2d ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to \left({A}\in {R}_{1}\left(\mathrm{suc}{B}\right)↔{A}\in 𝒫{R}_{1}\left({B}\right)\right)$
10 fvex ${⊢}{R}_{1}\left({B}\right)\in \mathrm{V}$
11 10 elpw2 ${⊢}{A}\in 𝒫{R}_{1}\left({B}\right)↔{A}\subseteq {R}_{1}\left({B}\right)$
12 9 11 syl6rbb ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to \left({A}\subseteq {R}_{1}\left({B}\right)↔{A}\in {R}_{1}\left(\mathrm{suc}{B}\right)\right)$
13 rankon ${⊢}\mathrm{rank}\left({A}\right)\in \mathrm{On}$
14 limord ${⊢}\mathrm{Lim}\mathrm{dom}{R}_{1}\to \mathrm{Ord}\mathrm{dom}{R}_{1}$
15 2 14 ax-mp ${⊢}\mathrm{Ord}\mathrm{dom}{R}_{1}$
16 ordelon ${⊢}\left(\mathrm{Ord}\mathrm{dom}{R}_{1}\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to {B}\in \mathrm{On}$
17 15 16 mpan ${⊢}{B}\in \mathrm{dom}{R}_{1}\to {B}\in \mathrm{On}$
18 17 adantl ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to {B}\in \mathrm{On}$
19 onsssuc ${⊢}\left(\mathrm{rank}\left({A}\right)\in \mathrm{On}\wedge {B}\in \mathrm{On}\right)\to \left(\mathrm{rank}\left({A}\right)\subseteq {B}↔\mathrm{rank}\left({A}\right)\in \mathrm{suc}{B}\right)$
20 13 18 19 sylancr ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to \left(\mathrm{rank}\left({A}\right)\subseteq {B}↔\mathrm{rank}\left({A}\right)\in \mathrm{suc}{B}\right)$
21 6 12 20 3bitr4d ${⊢}\left({A}\in \bigcup {R}_{1}\left[\mathrm{On}\right]\wedge {B}\in \mathrm{dom}{R}_{1}\right)\to \left({A}\subseteq {R}_{1}\left({B}\right)↔\mathrm{rank}\left({A}\right)\subseteq {B}\right)$