Metamath Proof Explorer

Theorem rankelb

Description: The membership relation is inherited by the rank function. Proposition 9.16 of TakeutiZaring p. 79. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Assertion rankelb ⊢ B ∈ ⋃ R1 On → A ∈ B → rank ⁡ A ∈ rank ⁡ B

Proof

Step Hyp Ref Expression
1 r1elssi ⊢ B ∈ ⋃ R1 On → B ⊆ ⋃ R1 On
2 1 sseld ⊢ B ∈ ⋃ R1 On → A ∈ B → A ∈ ⋃ R1 On
3 rankidn ⊢ A ∈ ⋃ R1 On → ¬ A ∈ R1 ⁡ rank ⁡ A
4 2 3 syl6 ⊢ B ∈ ⋃ R1 On → A ∈ B → ¬ A ∈ R1 ⁡ rank ⁡ A
5 4 imp ⊢ B ∈ ⋃ R1 On ∧ A ∈ B → ¬ A ∈ R1 ⁡ rank ⁡ A
6 rankon ⊢ rank ⁡ B ∈ On
7 rankon ⊢ rank ⁡ A ∈ On
8 ontri1 ⊢ rank ⁡ B ∈ On ∧ rank ⁡ A ∈ On → rank ⁡ B ⊆ rank ⁡ A ↔ ¬ rank ⁡ A ∈ rank ⁡ B
9 6 7 8 mp2an ⊢ rank ⁡ B ⊆ rank ⁡ A ↔ ¬ rank ⁡ A ∈ rank ⁡ B
10 rankdmr1 ⊢ rank ⁡ B ∈ dom ⁡ R1
11 rankdmr1 ⊢ rank ⁡ A ∈ dom ⁡ R1
12 r1ord3g ⊢ rank ⁡ B ∈ dom ⁡ R1 ∧ rank ⁡ A ∈ dom ⁡ R1 → rank ⁡ B ⊆ rank ⁡ A → R1 ⁡ rank ⁡ B ⊆ R1 ⁡ rank ⁡ A
13 10 11 12 mp2an ⊢ rank ⁡ B ⊆ rank ⁡ A → R1 ⁡ rank ⁡ B ⊆ R1 ⁡ rank ⁡ A
14 r1rankidb ⊢ B ∈ ⋃ R1 On → B ⊆ R1 ⁡ rank ⁡ B
15 14 sselda ⊢ B ∈ ⋃ R1 On ∧ A ∈ B → A ∈ R1 ⁡ rank ⁡ B
16 ssel ⊢ R1 ⁡ rank ⁡ B ⊆ R1 ⁡ rank ⁡ A → A ∈ R1 ⁡ rank ⁡ B → A ∈ R1 ⁡ rank ⁡ A
17 13 15 16 syl2imc ⊢ B ∈ ⋃ R1 On ∧ A ∈ B → rank ⁡ B ⊆ rank ⁡ A → A ∈ R1 ⁡ rank ⁡ A
18 9 17 biimtrrid ⊢ B ∈ ⋃ R1 On ∧ A ∈ B → ¬ rank ⁡ A ∈ rank ⁡ B → A ∈ R1 ⁡ rank ⁡ A
19 5 18 mt3d ⊢ B ∈ ⋃ R1 On ∧ A ∈ B → rank ⁡ A ∈ rank ⁡ B
20 19 ex ⊢ B ∈ ⋃ R1 On → A ∈ B → rank ⁡ A ∈ rank ⁡ B