This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in V$
	rankxpl.2	$⊢ B \in V$
Assertion	rankfu	$⊢ F : A ⟶ B \to rank (F) \subseteq suc suc rank (A \cup B)$

Step	Hyp	Ref	Expression
1		rankxpl.1	$⊢ A \in V$
2		rankxpl.2	$⊢ B \in V$
3		fssxp	$⊢ F : A ⟶ B \to F \subseteq A \times B$
4	1 2	xpex	$⊢ A \times B \in V$
5	4	rankss	$⊢ F \subseteq A \times B \to rank (F) \subseteq rank (A \times B)$
6	1 2	rankxpu	$⊢ rank (A \times B) \subseteq suc suc rank (A \cup B)$
7	5 6	sstrdi	$⊢ F \subseteq A \times B \to rank (F) \subseteq suc suc rank (A \cup B)$
8	3 7	syl	$⊢ F : A ⟶ B \to rank (F) \subseteq suc suc rank (A \cup B)$