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 ) ) )