rankr1c

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1 . Proposition 9.15(2) of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 17-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ B = rank (A) \to B = rank (A)$
2		rankdmr1	$⊢ rank (A) \in dom R_{1}$
3	1 2	eqeltrdi	$⊢ B = rank (A) \to B \in dom R_{1}$
4	3	a1i	$⊢ A \in ⋃ R_{1} [On] \to (B = rank (A) \to B \in dom R_{1})$
5		elfvdm	$⊢ A \in R_{1} (suc B) \to suc B \in dom R_{1}$
6		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
7	6	simpri	$⊢ Lim dom R_{1}$
8		limsuc	$⊢ Lim dom R_{1} \to (B \in dom R_{1} \leftrightarrow suc B \in dom R_{1})$
9	7 8	ax-mp	$⊢ B \in dom R_{1} \leftrightarrow suc B \in dom R_{1}$
10	5 9	sylibr	$⊢ A \in R_{1} (suc B) \to B \in dom R_{1}$
11	10	adantl	$⊢ (\neg A \in R_{1} (B) \land A \in R_{1} (suc B)) \to B \in dom R_{1}$
12	11	a1i	$⊢ A \in ⋃ R_{1} [On] \to ((\neg A \in R_{1} (B) \land A \in R_{1} (suc B)) \to B \in dom R_{1})$
13		eqss	$⊢ B = rank (A) \leftrightarrow (B \subseteq rank (A) \land rank (A) \subseteq B)$
14		rankr1clem	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (\neg A \in R_{1} (B) \leftrightarrow B \subseteq rank (A))$
15		rankr1ag	$⊢ (A \in ⋃ R_{1} [On] \land suc B \in dom R_{1}) \to (A \in R_{1} (suc B) \leftrightarrow rank (A) \in suc B)$
16	9 15	sylan2b	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (suc B) \leftrightarrow rank (A) \in suc B)$
17		rankon	$⊢ rank (A) \in On$
18		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
19	7 18	ax-mp	$⊢ Ord dom R_{1}$
20		ordelon	$⊢ (Ord dom R_{1} \land B \in dom R_{1}) \to B \in On$
21	19 20	mpan	$⊢ B \in dom R_{1} \to B \in On$
22	21	adantl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to B \in On$
23		onsssuc	$⊢ (rank (A) \in On \land B \in On) \to (rank (A) \subseteq B \leftrightarrow rank (A) \in suc B)$
24	17 22 23	sylancr	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (rank (A) \subseteq B \leftrightarrow rank (A) \in suc B)$
25	16 24	bitr4d	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (suc B) \leftrightarrow rank (A) \subseteq B)$
26	14 25	anbi12d	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to ((\neg A \in R_{1} (B) \land A \in R_{1} (suc B)) \leftrightarrow (B \subseteq rank (A) \land rank (A) \subseteq B))$
27	13 26	bitr4id	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (B = rank (A) \leftrightarrow (\neg A \in R_{1} (B) \land A \in R_{1} (suc B)))$
28	27	ex	$⊢ A \in ⋃ R_{1} [On] \to (B \in dom R_{1} \to (B = rank (A) \leftrightarrow (\neg A \in R_{1} (B) \land A \in R_{1} (suc B))))$
29	4 12 28	pm5.21ndd	$⊢ A \in ⋃ R_{1} [On] \to (B = rank (A) \leftrightarrow (\neg A \in R_{1} (B) \land A \in R_{1} (suc B)))$

Metamath Proof Explorer

Theorem rankr1c

Proof