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 ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B

Proof

Step Hyp Ref Expression
1 snwf ⊢ A ∈ ⋃ R1 On → A ∈ ⋃ R1 On
2 snwf ⊢ B ∈ ⋃ R1 On → B ∈ ⋃ R1 On
3 rankunb ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B
4 1 2 3 syl2an ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ B = rank ⁡ A ∪ rank ⁡ B
5 ranksnb ⊢ A ∈ ⋃ R1 On → rank ⁡ A = suc ⁡ rank ⁡ A
6 ranksnb ⊢ B ∈ ⋃ R1 On → rank ⁡ B = suc ⁡ rank ⁡ B
7 uneq12 ⊢ rank ⁡ A = suc ⁡ rank ⁡ A ∧ rank ⁡ B = suc ⁡ rank ⁡ B → rank ⁡ A ∪ rank ⁡ B = suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
8 5 6 7 syl2an ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ rank ⁡ B = suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
9 4 8 eqtrd ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ B = suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
10 df-pr ⊢ A B = A ∪ B
11 10 fveq2i ⊢ rank ⁡ A B = rank ⁡ A ∪ B
12 rankon ⊢ rank ⁡ A ∈ On
13 12 onordi ⊢ Ord ⁡ rank ⁡ A
14 rankon ⊢ rank ⁡ B ∈ On
15 14 onordi ⊢ Ord ⁡ rank ⁡ B
16 ordsucun ⊢ Ord ⁡ rank ⁡ A ∧ Ord ⁡ rank ⁡ B → suc ⁡ rank ⁡ A ∪ rank ⁡ B = suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
17 13 15 16 mp2an ⊢ suc ⁡ rank ⁡ A ∪ rank ⁡ B = suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
18 9 11 17 3eqtr4g ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B