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 rankun
Description: The rank of the union of two sets. Theorem 15.17(iii) of Monk1
p. 112. (Contributed by NM , 26-Nov-2003) (Revised by Mario Carneiro , 17-Nov-2014)
Ref
Expression
Hypotheses
ranksn.1 ⊢ 𝐴 ∈ V
rankun.2 ⊢ 𝐵 ∈ V
Assertion
rankun ⊢ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
ranksn.1 ⊢ 𝐴 ∈ V
2
rankun.2 ⊢ 𝐵 ∈ V
3
unir1 ⊢ ∪ ( 𝑅1 “ On ) = V
4
1 3
eleqtrri ⊢ 𝐴 ∈ ∪ ( 𝑅1 “ On )
5
2 3
eleqtrri ⊢ 𝐵 ∈ ∪ ( 𝑅1 “ On )
6
rankunb ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
7
4 5 6
mp2an ⊢ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )