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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
4	3	simpri	$⊢ Lim dom R_{1}$
5		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
6	4 5	ax-mp	$⊢ Ord dom R_{1}$
7		ordelon	$⊢ (Ord dom R_{1} \land B \in dom R_{1}) \to B \in On$
8	6 7	mpan	$⊢ B \in dom R_{1} \to B \in On$
9	8	adantl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to B \in On$
10		rankon	$⊢ rank (A) \in On$
11		ontri1	$⊢ (B \in On \land rank (A) \in On) \to (B \subseteq rank (A) \leftrightarrow \neg rank (A) \in B)$
12	9 10 11	sylancl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (B \subseteq rank (A) \leftrightarrow \neg rank (A) \in B)$
13	2 12	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