Metamath Proof Explorer

Theorem rankaltopb

Description: Compute the rank of an alternate ordered pair. (Contributed by Scott Fenton, 18-Dec-2013) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion rankaltopb ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B

Proof

Step Hyp Ref Expression
1 snwf ⊢ B ∈ ⋃ R1 On → B ∈ ⋃ R1 On
2 df-altop ⊢ A B = A A B
3 2 fveq2i ⊢ rank ⁡ A B = rank ⁡ A A B
4 snwf ⊢ A ∈ ⋃ R1 On → A ∈ ⋃ R1 On
5 4 adantr ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A ∈ ⋃ R1 On
6 prwf ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → A B ∈ ⋃ R1 On
7 rankprb ⊢ A ∈ ⋃ R1 On ∧ A B ∈ ⋃ R1 On → rank ⁡ A A B = suc ⁡ rank ⁡ A ∪ rank ⁡ A B
8 5 6 7 syl2anc ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A A B = suc ⁡ rank ⁡ A ∪ rank ⁡ A B
9 3 8 eqtrid ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ A B
10 snsspr1 ⊢ A ⊆ A B
11 ssequn1 ⊢ A ⊆ A B ↔ A ∪ A B = A B
12 10 11 mpbi ⊢ A ∪ A B = A B
13 12 fveq2i ⊢ rank ⁡ A ∪ A B = rank ⁡ A B
14 rankunb ⊢ A ∈ ⋃ R1 On ∧ A B ∈ ⋃ R1 On → rank ⁡ A ∪ A B = rank ⁡ A ∪ rank ⁡ A B
15 5 6 14 syl2anc ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ A B = rank ⁡ A ∪ rank ⁡ A B
16 rankprb ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B
17 13 15 16 3eqtr3a ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A ∪ rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B
18 suceq ⊢ rank ⁡ A ∪ rank ⁡ A B = suc ⁡ rank ⁡ A ∪ rank ⁡ B → suc ⁡ rank ⁡ A ∪ rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
19 17 18 syl ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → suc ⁡ rank ⁡ A ∪ rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
20 9 19 eqtrd ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
21 1 20 sylan2 ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B
22 ranksnb ⊢ B ∈ ⋃ R1 On → rank ⁡ B = suc ⁡ rank ⁡ B
23 22 uneq2d ⊢ B ∈ ⋃ R1 On → rank ⁡ A ∪ rank ⁡ B = rank ⁡ A ∪ suc ⁡ rank ⁡ B
24 suceq ⊢ rank ⁡ A ∪ rank ⁡ B = rank ⁡ A ∪ suc ⁡ rank ⁡ B → suc ⁡ rank ⁡ A ∪ rank ⁡ B = suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
25 suceq ⊢ suc ⁡ rank ⁡ A ∪ rank ⁡ B = suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B → suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B = suc ⁡ suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
26 23 24 25 3syl ⊢ B ∈ ⋃ R1 On → suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B = suc ⁡ suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
27 26 adantl ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → suc ⁡ suc ⁡ rank ⁡ A ∪ rank ⁡ B = suc ⁡ suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B
28 21 27 eqtrd ⊢ A ∈ ⋃ R1 On ∧ B ∈ ⋃ R1 On → rank ⁡ A B = suc ⁡ suc ⁡ rank ⁡ A ∪ suc ⁡ rank ⁡ B