rankelb

Description: The membership relation is inherited by the rank function. Proposition 9.16 of TakeutiZaring p. 79. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		r1elssi	$⊢ B \in ⋃ R_{1} [On] \to B \subseteq ⋃ R_{1} [On]$
2	1	sseld	$⊢ B \in ⋃ R_{1} [On] \to (A \in B \to A \in ⋃ R_{1} [On])$
3		rankidn	$⊢ A \in ⋃ R_{1} [On] \to \neg A \in R_{1} (rank (A))$
4	2 3	syl6	$⊢ B \in ⋃ R_{1} [On] \to (A \in B \to \neg A \in R_{1} (rank (A)))$
5	4	imp	$⊢ (B \in ⋃ R_{1} [On] \land A \in B) \to \neg A \in R_{1} (rank (A))$
6		rankon	$⊢ rank (B) \in On$
7		rankon	$⊢ rank (A) \in On$
8		ontri1	$⊢ (rank (B) \in On \land rank (A) \in On) \to (rank (B) \subseteq rank (A) \leftrightarrow \neg rank (A) \in rank (B))$
9	6 7 8	mp2an	$⊢ rank (B) \subseteq rank (A) \leftrightarrow \neg rank (A) \in rank (B)$
10		rankdmr1	$⊢ rank (B) \in dom R_{1}$
11		rankdmr1	$⊢ rank (A) \in dom R_{1}$
12		r1ord3g	$⊢ (rank (B) \in dom R_{1} \land rank (A) \in dom R_{1}) \to (rank (B) \subseteq rank (A) \to R_{1} (rank (B)) \subseteq R_{1} (rank (A)))$
13	10 11 12	mp2an	$⊢ rank (B) \subseteq rank (A) \to R_{1} (rank (B)) \subseteq R_{1} (rank (A))$
14		r1rankidb	$⊢ B \in ⋃ R_{1} [On] \to B \subseteq R_{1} (rank (B))$
15	14	sselda	$⊢ (B \in ⋃ R_{1} [On] \land A \in B) \to A \in R_{1} (rank (B))$
16		ssel	$⊢ R_{1} (rank (B)) \subseteq R_{1} (rank (A)) \to (A \in R_{1} (rank (B)) \to A \in R_{1} (rank (A)))$
17	13 15 16	syl2imc	$⊢ (B \in ⋃ R_{1} [On] \land A \in B) \to (rank (B) \subseteq rank (A) \to A \in R_{1} (rank (A)))$
18	9 17	biimtrrid	$⊢ (B \in ⋃ R_{1} [On] \land A \in B) \to (\neg rank (A) \in rank (B) \to A \in R_{1} (rank (A)))$
19	5 18	mt3d	$⊢ (B \in ⋃ R_{1} [On] \land A \in B) \to rank (A) \in rank (B)$
20	19	ex	$⊢ B \in ⋃ R_{1} [On] \to (A \in B \to rank (A) \in rank (B))$

Metamath Proof Explorer

Theorem rankelb

Proof