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

Metamath Proof Explorer

Theorem rankop

Description: The rank of an ordered pair. Part of Exercise 4 of Kunen p. 107. (Contributed by NM, 13-Sep-2006) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses ranksn.1 ⊢ 𝐴 ∈ V
rankun.2 ⊢ 𝐵 ∈ V
Assertion rankop ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = suc suc ( ( 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 rankopb ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
7 4 5 6 mp2an ⊢ ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) )