This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 r1elssi ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → 𝐵 ⊆ ∪ ( 𝑅1 “ On ) )
2 1 sseld ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ ∪ ( 𝑅1 “ On ) ) )
3 rankidn ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ¬ 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
4 2 3 syl6 ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
5 4 imp ⊢ ( ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ 𝐵 ) → ¬ 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
6 rankon ⊢ ( rank ‘ 𝐵 ) ∈ On
7 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
8 ontri1 ⊢ ( ( ( rank ‘ 𝐵 ) ∈ On ∧ ( rank ‘ 𝐴 ) ∈ On ) → ( ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) )
9 6 7 8 mp2an ⊢ ( ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) )
10 rankdmr1 ⊢ ( rank ‘ 𝐵 ) ∈ dom 𝑅1
11 rankdmr1 ⊢ ( rank ‘ 𝐴 ) ∈ dom 𝑅1
12 r1ord3g ⊢ ( ( ( rank ‘ 𝐵 ) ∈ dom 𝑅1 ∧ ( rank ‘ 𝐴 ) ∈ dom 𝑅1 ) → ( ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) → ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
13 10 11 12 mp2an ⊢ ( ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) → ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
14 r1rankidb ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → 𝐵 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) )
15 14 sselda ⊢ ( ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) )
16 ssel ⊢ ( ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) → ( 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐵 ) ) → 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
17 13 15 16 syl2imc ⊢ ( ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ 𝐵 ) → ( ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) → 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
18 9 17 biimtrrid ⊢ ( ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ 𝐵 ) → ( ¬ ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) → 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) )
19 5 18 mt3d ⊢ ( ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐴 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) )
20 19 ex ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) )