Metamath Proof Explorer

Theorem rankssb

Description: The subset relation is inherited by the rank function. Exercise 1 of TakeutiZaring p. 80. (Contributed by NM, 25-Nov-2003) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	rankssb	$⊢ B \in ⋃ R_{1} [On] \to (A \subseteq B \to rank (A) \subseteq rank (B))$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (B \in ⋃ R_{1} [On] \land A \subseteq B) \to A \subseteq B$
2		r1rankidb	$⊢ B \in ⋃ R_{1} [On] \to B \subseteq R_{1} (rank (B))$
3	2	adantr	$⊢ (B \in ⋃ R_{1} [On] \land A \subseteq B) \to B \subseteq R_{1} (rank (B))$
4	1 3	sstrd	$⊢ (B \in ⋃ R_{1} [On] \land A \subseteq B) \to A \subseteq R_{1} (rank (B))$
5		sswf	$⊢ (B \in ⋃ R_{1} [On] \land A \subseteq B) \to A \in ⋃ R_{1} [On]$
6		rankdmr1	$⊢ rank (B) \in dom R_{1}$
7		rankr1bg	$⊢ (A \in ⋃ R_{1} [On] \land rank (B) \in dom R_{1}) \to (A \subseteq R_{1} (rank (B)) \leftrightarrow rank (A) \subseteq rank (B))$
8	5 6 7	sylancl	$⊢ (B \in ⋃ R_{1} [On] \land A \subseteq B) \to (A \subseteq R_{1} (rank (B)) \leftrightarrow rank (A) \subseteq rank (B))$
9	4 8	mpbid	$⊢ (B \in ⋃ R_{1} [On] \land A \subseteq B) \to rank (A) \subseteq rank (B)$
10	9	ex	$⊢ B \in ⋃ R_{1} [On] \to (A \subseteq B \to rank (A) \subseteq rank (B))$