This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Infinity Rank rankel
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
Hypothesis
rankel.1 ⊢ 𝐵 ∈ V
Assertion
rankel ⊢ ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
rankel.1 ⊢ 𝐵 ∈ V
2
unir1 ⊢ ∪ ( 𝑅1 “ On ) = V
3
1 2
eleqtrri ⊢ 𝐵 ∈ ∪ ( 𝑅1 “ On )
4
rankelb ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) ) )
5
3 4
ax-mp ⊢ ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐵 ) )