Metamath Proof Explorer

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 ⊢ A ∈ V
Assertion rankr1b ⊢ B ∈ On → A ⊆ R1 ⁡ B ↔ rank ⁡ A ⊆ B

Proof

Step Hyp Ref Expression
1 rankr1b.1 ⊢ A ∈ V
2 r1fnon ⊢ R1 Fn On
3 2 fndmi ⊢ dom ⁡ R1 = On
4 3 eleq2i ⊢ B ∈ dom ⁡ R1 ↔ B ∈ On
5 unir1 ⊢ ⋃ R1 On = V
6 1 5 eleqtrri ⊢ A ∈ ⋃ R1 On
7 rankr1bg ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → A ⊆ R1 ⁡ B ↔ rank ⁡ A ⊆ B
8 6 7 mpan ⊢ B ∈ dom ⁡ R1 → A ⊆ R1 ⁡ B ↔ rank ⁡ A ⊆ B
9 4 8 sylbir ⊢ B ∈ On → A ⊆ R1 ⁡ B ↔ rank ⁡ A ⊆ B