rankval4

Description: The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of Jech p. 72. Also a special case of Theorem 7V(b) of Enderton p. 204. (Contributed by NM, 12-Oct-2003)

		Ref	Expression
	Hypothesis	rankr1b.1	$⊢ A \in V$
	Assertion	rankval4	$⊢ rank (A) = ⋃_{x \in A} suc rank (x)$

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	$⊢ A \in V$
2		nfcv	$⊢ \underline{Ⅎ} x A$
3		nfcv	$⊢ \underline{Ⅎ} x R_{1}$
4		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} suc rank (x)$
5	3 4	nffv	$⊢ \underline{Ⅎ} x R_{1} (⋃_{x \in A} suc rank (x))$
6	2 5	dfssf	$⊢ A \subseteq R_{1} (⋃_{x \in A} suc rank (x)) \leftrightarrow \forall x (x \in A \to x \in R_{1} (⋃_{x \in A} suc rank (x)))$
7		vex	$⊢ x \in V$
8	7	rankid	$⊢ x \in R_{1} (suc rank (x))$
9		ssiun2	$⊢ x \in A \to suc rank (x) \subseteq ⋃_{x \in A} suc rank (x)$
10		rankon	$⊢ rank (x) \in On$
11	10	onsuci	$⊢ suc rank (x) \in On$
12	11	rgenw	$⊢ \forall x \in A suc rank (x) \in On$
13		iunon	$⊢ (A \in V \land \forall x \in A suc rank (x) \in On) \to ⋃_{x \in A} suc rank (x) \in On$
14	1 12 13	mp2an	$⊢ ⋃_{x \in A} suc rank (x) \in On$
15		r1ord3	$⊢ (suc rank (x) \in On \land ⋃_{x \in A} suc rank (x) \in On) \to (suc rank (x) \subseteq ⋃_{x \in A} suc rank (x) \to R_{1} (suc rank (x)) \subseteq R_{1} (⋃_{x \in A} suc rank (x)))$
16	11 14 15	mp2an	$⊢ suc rank (x) \subseteq ⋃_{x \in A} suc rank (x) \to R_{1} (suc rank (x)) \subseteq R_{1} (⋃_{x \in A} suc rank (x))$
17	9 16	syl	$⊢ x \in A \to R_{1} (suc rank (x)) \subseteq R_{1} (⋃_{x \in A} suc rank (x))$
18	17	sseld	$⊢ x \in A \to (x \in R_{1} (suc rank (x)) \to x \in R_{1} (⋃_{x \in A} suc rank (x)))$
19	8 18	mpi	$⊢ x \in A \to x \in R_{1} (⋃_{x \in A} suc rank (x))$
20	6 19	mpgbir	$⊢ A \subseteq R_{1} (⋃_{x \in A} suc rank (x))$
21		fvex	$⊢ R_{1} (⋃_{x \in A} suc rank (x)) \in V$
22	21	rankss	$⊢ A \subseteq R_{1} (⋃_{x \in A} suc rank (x)) \to rank (A) \subseteq rank (R_{1} (⋃_{x \in A} suc rank (x)))$
23	20 22	ax-mp	$⊢ rank (A) \subseteq rank (R_{1} (⋃_{x \in A} suc rank (x)))$
24		r1ord3	$⊢ (⋃_{x \in A} suc rank (x) \in On \land y \in On) \to (⋃_{x \in A} suc rank (x) \subseteq y \to R_{1} (⋃_{x \in A} suc rank (x)) \subseteq R_{1} (y))$
25	14 24	mpan	$⊢ y \in On \to (⋃_{x \in A} suc rank (x) \subseteq y \to R_{1} (⋃_{x \in A} suc rank (x)) \subseteq R_{1} (y))$
26	25	ss2rabi	$⊢ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\} \subseteq \{y \in On \| R_{1} (⋃_{x \in A} suc rank (x)) \subseteq R_{1} (y)\}$
27		intss	$⊢ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\} \subseteq \{y \in On \| R_{1} (⋃_{x \in A} suc rank (x)) \subseteq R_{1} (y)\} \to ⋂ \{y \in On \| R_{1} (⋃_{x \in A} suc rank (x)) \subseteq R_{1} (y)\} \subseteq ⋂ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\}$
28	26 27	ax-mp	$⊢ ⋂ \{y \in On \| R_{1} (⋃_{x \in A} suc rank (x)) \subseteq R_{1} (y)\} \subseteq ⋂ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\}$
29		rankval2	$⊢ R_{1} (⋃_{x \in A} suc rank (x)) \in V \to rank (R_{1} (⋃_{x \in A} suc rank (x))) = ⋂ \{y \in On \| R_{1} (⋃_{x \in A} suc rank (x)) \subseteq R_{1} (y)\}$
30	21 29	ax-mp	$⊢ rank (R_{1} (⋃_{x \in A} suc rank (x))) = ⋂ \{y \in On \| R_{1} (⋃_{x \in A} suc rank (x)) \subseteq R_{1} (y)\}$
31		intmin	$⊢ ⋃_{x \in A} suc rank (x) \in On \to ⋂ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\} = ⋃_{x \in A} suc rank (x)$
32	14 31	ax-mp	$⊢ ⋂ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\} = ⋃_{x \in A} suc rank (x)$
33	32	eqcomi	$⊢ ⋃_{x \in A} suc rank (x) = ⋂ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\}$
34	28 30 33	3sstr4i	$⊢ rank (R_{1} (⋃_{x \in A} suc rank (x))) \subseteq ⋃_{x \in A} suc rank (x)$
35	23 34	sstri	$⊢ rank (A) \subseteq ⋃_{x \in A} suc rank (x)$
36		iunss	$⊢ ⋃_{x \in A} suc rank (x) \subseteq rank (A) \leftrightarrow \forall x \in A suc rank (x) \subseteq rank (A)$
37	1	rankel	$⊢ x \in A \to rank (x) \in rank (A)$
38		rankon	$⊢ rank (A) \in On$
39	10 38	onsucssi	$⊢ rank (x) \in rank (A) \leftrightarrow suc rank (x) \subseteq rank (A)$
40	37 39	sylib	$⊢ x \in A \to suc rank (x) \subseteq rank (A)$
41	36 40	mprgbir	$⊢ ⋃_{x \in A} suc rank (x) \subseteq rank (A)$
42	35 41	eqssi	$⊢ rank (A) = ⋃_{x \in A} suc rank (x)$

Metamath Proof Explorer

Theorem rankval4

Proof