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 ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → A ⊆ R1 ⁡ B ↔ rank ⁡ A ⊆ B

Proof

Step Hyp Ref Expression
1 r1dmlim ⊢ Lim ⁡ dom ⁡ R1
2 limsuc ⊢ Lim ⁡ dom ⁡ R1 → B ∈ dom ⁡ R1 ↔ suc ⁡ B ∈ dom ⁡ R1
3 1 2 ax-mp ⊢ B ∈ dom ⁡ R1 ↔ suc ⁡ B ∈ dom ⁡ R1
4 rankr1ag ⊢ A ∈ ⋃ R1 On ∧ suc ⁡ B ∈ dom ⁡ R1 → A ∈ R1 ⁡ suc ⁡ B ↔ rank ⁡ A ∈ suc ⁡ B
5 3 4 sylan2b ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → A ∈ R1 ⁡ suc ⁡ B ↔ rank ⁡ A ∈ suc ⁡ B
6 r1sucg ⊢ B ∈ dom ⁡ R1 → R1 ⁡ suc ⁡ B = 𝒫 R1 ⁡ B
7 6 adantl ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → R1 ⁡ suc ⁡ B = 𝒫 R1 ⁡ B
8 7 eleq2d ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → A ∈ R1 ⁡ suc ⁡ B ↔ A ∈ 𝒫 R1 ⁡ B
9 fvex ⊢ R1 ⁡ B ∈ V
10 9 elpw2 ⊢ A ∈ 𝒫 R1 ⁡ B ↔ A ⊆ R1 ⁡ B
11 8 10 bitr2di ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → A ⊆ R1 ⁡ B ↔ A ∈ R1 ⁡ suc ⁡ B
12 rankon ⊢ rank ⁡ A ∈ On
13 limord ⊢ Lim ⁡ dom ⁡ R1 → Ord ⁡ dom ⁡ R1
14 1 13 ax-mp ⊢ Ord ⁡ dom ⁡ R1
15 ordelon ⊢ Ord ⁡ dom ⁡ R1 ∧ B ∈ dom ⁡ R1 → B ∈ On
16 14 15 mpan ⊢ B ∈ dom ⁡ R1 → B ∈ On
17 16 adantl ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → B ∈ On
18 onsssuc ⊢ rank ⁡ A ∈ On ∧ B ∈ On → rank ⁡ A ⊆ B ↔ rank ⁡ A ∈ suc ⁡ B
19 12 17 18 sylancr ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → rank ⁡ A ⊆ B ↔ rank ⁡ A ∈ suc ⁡ B
20 5 11 19 3bitr4d ⊢ A ∈ ⋃ R1 On ∧ B ∈ dom ⁡ R1 → A ⊆ R1 ⁡ B ↔ rank ⁡ A ⊆ B