Theorem rankr1b

Description: A relationship between rank and R1 . See rankr1a for the membership version. (Contributed by NM, 15-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Hypothesis	rankr1b.1	⊢ 𝐴 ∈ V
Assertion	rankr1b	⊢ ( 𝐵 ∈ On → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	⊢ 𝐴 ∈ V
2		r1fnon	⊢ 𝑅1 Fn On
3	2	fndmi	⊢ dom 𝑅1 = On
4	3	eleq2i	⊢ ( 𝐵 ∈ dom 𝑅1 ↔ 𝐵 ∈ On )
5		unir1	⊢ ∪ ( 𝑅1 “ On ) = V
6	1 5	eleqtrri	⊢ 𝐴 ∈ ∪ ( 𝑅1 “ On )
7		rankr1bg	⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ dom 𝑅1 ) → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
8	6 7	mpan	⊢ ( 𝐵 ∈ dom 𝑅1 → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )
9	4 8	sylbir	⊢ ( 𝐵 ∈ On → ( 𝐴 ⊆ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ⊆ 𝐵 ) )