Metamath Proof Explorer

Theorem rankmapu

Description: An upper bound on the rank of set exponentiation. (Contributed by Gérard Lang, 5-Aug-2018)

Ref Expression
Hypotheses rankxpl.1 ⊢ 𝐴 ∈ V
rankxpl.2 ⊢ 𝐵 ∈ V
Assertion rankmapu ( rank ‘ ( 𝐴 ↑m 𝐵 ) ) ⊆ suc suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 rankxpl.1 ⊢ 𝐴 ∈ V
2 rankxpl.2 ⊢ 𝐵 ∈ V
3 mapsspw ⊢ ( 𝐴 ↑m 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 )
4 2 1 xpex ⊢ ( 𝐵 × 𝐴 ) ∈ V
5 4 pwex ⊢ 𝒫 ( 𝐵 × 𝐴 ) ∈ V
6 5 rankss ⊢ ( ( 𝐴 ↑m 𝐵 ) ⊆ 𝒫 ( 𝐵 × 𝐴 ) → ( rank ‘ ( 𝐴 ↑m 𝐵 ) ) ⊆ ( rank ‘ 𝒫 ( 𝐵 × 𝐴 ) ) )
7 3 6 ax-mp ⊢ ( rank ‘ ( 𝐴 ↑m 𝐵 ) ) ⊆ ( rank ‘ 𝒫 ( 𝐵 × 𝐴 ) )
8 4 rankpw ⊢ ( rank ‘ 𝒫 ( 𝐵 × 𝐴 ) ) = suc ( rank ‘ ( 𝐵 × 𝐴 ) )
9 2 1 rankxpu ⊢ ( rank ‘ ( 𝐵 × 𝐴 ) ) ⊆ suc suc ( rank ‘ ( 𝐵 ∪ 𝐴 ) )
10 uncom ⊢ ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 )
11 10 fveq2i ⊢ ( rank ‘ ( 𝐵 ∪ 𝐴 ) ) = ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
12 suceq ⊢ ( ( rank ‘ ( 𝐵 ∪ 𝐴 ) ) = ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) → suc ( rank ‘ ( 𝐵 ∪ 𝐴 ) ) = suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
13 11 12 ax-mp ⊢ suc ( rank ‘ ( 𝐵 ∪ 𝐴 ) ) = suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
14 suceq ⊢ ( suc ( rank ‘ ( 𝐵 ∪ 𝐴 ) ) = suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) → suc suc ( rank ‘ ( 𝐵 ∪ 𝐴 ) ) = suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
15 13 14 ax-mp ⊢ suc suc ( rank ‘ ( 𝐵 ∪ 𝐴 ) ) = suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
16 9 15 sseqtri ⊢ ( rank ‘ ( 𝐵 × 𝐴 ) ) ⊆ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
17 rankon ⊢ ( rank ‘ ( 𝐵 × 𝐴 ) ) ∈ On
18 17 onordi ⊢ Ord ( rank ‘ ( 𝐵 × 𝐴 ) )
19 rankon ⊢ ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ On
20 19 onsuci ⊢ suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ On
21 20 onsuci ⊢ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ∈ On
22 21 onordi ⊢ Ord suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
23 ordsucsssuc ⊢ ( ( Ord ( rank ‘ ( 𝐵 × 𝐴 ) ) ∧ Ord suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) → ( ( rank ‘ ( 𝐵 × 𝐴 ) ) ⊆ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ suc ( rank ‘ ( 𝐵 × 𝐴 ) ) ⊆ suc suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ) )
24 18 22 23 mp2an ⊢ ( ( rank ‘ ( 𝐵 × 𝐴 ) ) ⊆ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) ↔ suc ( rank ‘ ( 𝐵 × 𝐴 ) ) ⊆ suc suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
25 16 24 mpbi ⊢ suc ( rank ‘ ( 𝐵 × 𝐴 ) ) ⊆ suc suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
26 8 25 eqsstri ⊢ ( rank ‘ 𝒫 ( 𝐵 × 𝐴 ) ) ⊆ suc suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
27 7 26 sstri ⊢ ( rank ‘ ( 𝐴 ↑m 𝐵 ) ) ⊆ suc suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )