rankr1clem

Description: Lemma for rankr1c . (Contributed by NM, 6-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	rankr1clem	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (\neg A \in R_{1} (B) \leftrightarrow B \subseteq rank (A))$

Step	Hyp	Ref	Expression
1		rankr1ag	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (B) \leftrightarrow rank (A) \in B)$
2	1	notbid	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (\neg A \in R_{1} (B) \leftrightarrow \neg rank (A) \in B)$
3		r1dmlim	$⊢ Lim dom R_{1}$
4		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
5	3 4	ax-mp	$⊢ Ord dom R_{1}$
6		ordelon	$⊢ (Ord dom R_{1} \land B \in dom R_{1}) \to B \in On$
7	5 6	mpan	$⊢ B \in dom R_{1} \to B \in On$
8	7	adantl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to B \in On$
9		rankon	$⊢ rank (A) \in On$
10		ontri1	$⊢ (B \in On \land rank (A) \in On) \to (B \subseteq rank (A) \leftrightarrow \neg rank (A) \in B)$
11	8 9 10	sylancl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (B \subseteq rank (A) \leftrightarrow \neg rank (A) \in B)$
12	2 11	bitr4d	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (\neg A \in R_{1} (B) \leftrightarrow B \subseteq rank (A))$

Metamath Proof Explorer