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

Metamath Proof Explorer

Theorem rankopb

Description: The rank of an ordered pair. Part of Exercise 4 of Kunen p. 107. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion rankopb ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dfopg ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } } )
2 1 fveq2d ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( rank ‘ { { 𝐴 } , { 𝐴 , 𝐵 } } ) )
3 snwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
4 prwf ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) )
5 rankprb ⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { { 𝐴 } , { 𝐴 , 𝐵 } } ) = suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , 𝐵 } ) ) )
6 3 4 5 syl2an2r ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { { 𝐴 } , { 𝐴 , 𝐵 } } ) = suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , 𝐵 } ) ) )
7 snsspr1 ⊢ { 𝐴 } ⊆ { 𝐴 , 𝐵 }
8 ssequn1 ⊢ ( { 𝐴 } ⊆ { 𝐴 , 𝐵 } ↔ ( { 𝐴 } ∪ { 𝐴 , 𝐵 } ) = { 𝐴 , 𝐵 } )
9 7 8 mpbi ⊢ ( { 𝐴 } ∪ { 𝐴 , 𝐵 } ) = { 𝐴 , 𝐵 }
10 9 fveq2i ⊢ ( rank ‘ ( { 𝐴 } ∪ { 𝐴 , 𝐵 } ) ) = ( rank ‘ { 𝐴 , 𝐵 } )
11 rankunb ⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐴 , 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐴 , 𝐵 } ) ) = ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , 𝐵 } ) ) )
12 3 4 11 syl2an2r ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐴 , 𝐵 } ) ) = ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , 𝐵 } ) ) )
13 rankprb ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { 𝐴 , 𝐵 } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
14 10 12 13 3eqtr3a ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , 𝐵 } ) ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
15 suceq ⊢ ( ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , 𝐵 } ) ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) → suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , 𝐵 } ) ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
16 14 15 syl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , 𝐵 } ) ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )
17 2 6 16 3eqtrd ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )