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 ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟪ 𝐴 , 𝐵 ⟫ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 snwf ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) )
2 df-altop ⊢ ⟪ 𝐴 , 𝐵 ⟫ = { { 𝐴 } , { 𝐴 , { 𝐵 } } }
3 2 fveq2i ⊢ ( rank ‘ ⟪ 𝐴 , 𝐵 ⟫ ) = ( rank ‘ { { 𝐴 } , { 𝐴 , { 𝐵 } } } )
4 snwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
5 4 adantr ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
6 prwf ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → { 𝐴 , { 𝐵 } } ∈ ∪ ( 𝑅1 “ On ) )
7 rankprb ⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐴 , { 𝐵 } } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { { 𝐴 } , { 𝐴 , { 𝐵 } } } ) = suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) )
8 5 6 7 syl2anc ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { { 𝐴 } , { 𝐴 , { 𝐵 } } } ) = suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) )
9 3 8 syl5eq ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟪ 𝐴 , 𝐵 ⟫ ) = suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) )
10 snsspr1 ⊢ { 𝐴 } ⊆ { 𝐴 , { 𝐵 } }
11 ssequn1 ⊢ ( { 𝐴 } ⊆ { 𝐴 , { 𝐵 } } ↔ ( { 𝐴 } ∪ { 𝐴 , { 𝐵 } } ) = { 𝐴 , { 𝐵 } } )
12 10 11 mpbi ⊢ ( { 𝐴 } ∪ { 𝐴 , { 𝐵 } } ) = { 𝐴 , { 𝐵 } }
13 12 fveq2i ⊢ ( rank ‘ ( { 𝐴 } ∪ { 𝐴 , { 𝐵 } } ) ) = ( rank ‘ { 𝐴 , { 𝐵 } } )
14 rankunb ⊢ ( ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐴 , { 𝐵 } } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐴 , { 𝐵 } } ) ) = ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) )
15 5 6 14 syl2anc ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ( { 𝐴 } ∪ { 𝐴 , { 𝐵 } } ) ) = ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) )
16 rankprb ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ { 𝐴 , { 𝐵 } } ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) )
17 13 15 16 3eqtr3a ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) )
18 suceq ⊢ ( ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) = suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) → suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) )
19 17 18 syl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → suc ( ( rank ‘ { 𝐴 } ) ∪ ( rank ‘ { 𝐴 , { 𝐵 } } ) ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) )
20 9 19 eqtrd ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ { 𝐵 } ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟪ 𝐴 , 𝐵 ⟫ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) )
21 1 20 sylan2 ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟪ 𝐴 , 𝐵 ⟫ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) )
22 ranksnb ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐵 } ) = suc ( rank ‘ 𝐵 ) )
23 22 uneq2d ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) = ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
24 suceq ⊢ ( ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) = ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) → suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) = suc ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
25 suceq ⊢ ( suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) = suc ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) → suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) = suc suc ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
26 23 24 25 3syl ⊢ ( 𝐵 ∈ ∪ ( 𝑅1 “ On ) → suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) = suc suc ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
27 26 adantl ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → suc suc ( ( rank ‘ 𝐴 ) ∪ ( rank ‘ { 𝐵 } ) ) = suc suc ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )
28 21 27 eqtrd ⊢ ( ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝐵 ∈ ∪ ( 𝑅1 “ On ) ) → ( rank ‘ ⟪ 𝐴 , 𝐵 ⟫ ) = suc suc ( ( rank ‘ 𝐴 ) ∪ suc ( rank ‘ 𝐵 ) ) )