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	⊢ 𝐴 ∈ V
	rankxpl.2	⊢ 𝐵 ∈ V
Assertion	rankfu	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( rank ‘ 𝐹 ) ⊆ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rankxpl.1	⊢ 𝐴 ∈ V
2		rankxpl.2	⊢ 𝐵 ∈ V
3		fssxp	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
4	1 2	xpex	⊢ ( 𝐴 × 𝐵 ) ∈ V
5	4	rankss	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( rank ‘ 𝐹 ) ⊆ ( rank ‘ ( 𝐴 × 𝐵 ) ) )
6	1 2	rankxpu	⊢ ( rank ‘ ( 𝐴 × 𝐵 ) ) ⊆ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) )
7	5 6	sstrdi	⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ( rank ‘ 𝐹 ) ⊆ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )
8	3 7	syl	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( rank ‘ 𝐹 ) ⊆ suc suc ( rank ‘ ( 𝐴 ∪ 𝐵 ) ) )