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

Metamath Proof Explorer

Theorem rankprb

Description: The rank of an unordered pair. Part of Exercise 30 of Enderton p. 207. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion rankprb ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { 𝐴 , 𝐵 } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 snwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
2 snwf ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) )
3 rankunb ⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐵 } ) ) )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐵 } ) ) )
5 ranksnb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )
6 ranksnb ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐵 } ) = suc ( rank ‘ 𝐵 ) )
7 uneq12 ⊢ ( ( ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) ∧ ( rank ‘ { 𝐵 } ) = suc ( rank ‘ 𝐵 ) ) → ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐵 } ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
8 5 6 7 syl2an ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐵 } ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
9 4 8 eqtrd ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐵 } ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
10 df-pr ⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
11 10 fveq2i ⊢ ( rank ‘ { 𝐴 , 𝐵 } ) = ( rank ‘ ( { 𝐴 } ∪ { 𝐵 } ) )
12 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
13 12 onordi ⊢ Ord ( rank ‘ 𝐴 )
14 rankon ⊢ ( rank ‘ 𝐵 ) ∈ On
15 14 onordi ⊢ Ord ( rank ‘ 𝐵 )
16 ordsucun ⊢ ( ( Ord ( rank ‘ 𝐴 ) ∧ Ord ( rank ‘ 𝐵 ) ) → suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
17 13 15 16 mp2an ⊢ suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) = ( suc ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) )
18 9 11 17 3eqtr4g ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { 𝐴 , 𝐵 } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ 𝐵 ) ) )