Metamath Proof Explorer


Theorem rankfu

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

Ref Expression
Hypotheses rankxpl.1
|- A e. _V
rankxpl.2
|- B e. _V
Assertion rankfu
|- ( F : A --> B -> ( rank ` F ) C_ suc suc ( rank ` ( A u. B ) ) )

Proof

Step Hyp Ref Expression
1 rankxpl.1
 |-  A e. _V
2 rankxpl.2
 |-  B e. _V
3 fssxp
 |-  ( F : A --> B -> F C_ ( A X. B ) )
4 1 2 xpex
 |-  ( A X. B ) e. _V
5 4 rankss
 |-  ( F C_ ( A X. B ) -> ( rank ` F ) C_ ( rank ` ( A X. B ) ) )
6 1 2 rankxpu
 |-  ( rank ` ( A X. B ) ) C_ suc suc ( rank ` ( A u. B ) )
7 5 6 sstrdi
 |-  ( F C_ ( A X. B ) -> ( rank ` F ) C_ suc suc ( rank ` ( A u. B ) ) )
8 3 7 syl
 |-  ( F : A --> B -> ( rank ` F ) C_ suc suc ( rank ` ( A u. B ) ) )