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 ‘ 𝐴 ) ⊆ 𝐵 ) )