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

Proof

Step Hyp Ref Expression
1 dfopg ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B = A A B
2 1 fveq2d ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = rank ⁡ A A B
3 snwf ⊢ A ∈ ⋃ R1 On → A ∈ ⋃ R1 On
4 prwf ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B ∈ ⋃ R1 On
5 rankprb ⊢ A ∈ ⋃ R1 On ∧ A B ∈ ⋃ R1 On → rank ⁡ A A B = suc ⁡ rank ⁡ A ∪ rank ⁡ A B
6 3 4 5 syl2an2r ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A A B = suc ⁡ rank ⁡ A ∪ rank ⁡ A B
7 snsspr1 ⊢ A ⊆ A B
8 ssequn1 ⊢ A ⊆ A B ↔ A ∪ A B = A B
9 7 8 mpbi ⊢ A ∪ A B = A B
10 9 fveq2i ⊢ rank ⁡ A ∪ A B = rank ⁡ A B
11 rankunb ⊢ A ∈ ⋃ R1 On ∧ A B ∈ ⋃ R1 On → rank ⁡ A ∪ A B = rank ⁡ A ∪ rank ⁡ A B
12 3 4 11 syl2an2r ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ A B = rank ⁡ A ∪ rank ⁡ A B
13 rankprb ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B
14 10 12 13 3eqtr3a ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B
15 suceq ⊢ rank ⁡ A ∪ rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B → suc ⁡ rank ⁡ A ∪ rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
16 14 15 syl ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → suc ⁡ rank ⁡ A ∪ rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
17 2 6 16 3eqtrd ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B