rankuni2b

Description: The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 8-Jun-2013)

		Ref	Expression
	Assertion	rankuni2b	$⊢ A \in ⋃ R_{1} [On] \to rank (⋃ A) = ⋃_{x \in A} rank (x)$

Proof

Step	Hyp	Ref	Expression
1		uniwf	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow ⋃ A \in ⋃ R_{1} [On]$
2		rankval3b	$⊢ ⋃ A \in ⋃ R_{1} [On] \to rank (⋃ A) = ⋂ \{z \in On \| \forall y \in ⋃ A rank (y) \in z\}$
3	1 2	sylbi	$⊢ A \in ⋃ R_{1} [On] \to rank (⋃ A) = ⋂ \{z \in On \| \forall y \in ⋃ A rank (y) \in z\}$
4		eleq2	$⊢ z = ⋃_{x \in A} rank (x) \to (rank (y) \in z \leftrightarrow rank (y) \in ⋃_{x \in A} rank (x))$
5	4	ralbidv	$⊢ z = ⋃_{x \in A} rank (x) \to (\forall y \in ⋃ A rank (y) \in z \leftrightarrow \forall y \in ⋃ A rank (y) \in ⋃_{x \in A} rank (x))$
6		iuneq1	$⊢ y = A \to ⋃_{x \in y} rank (x) = ⋃_{x \in A} rank (x)$
7	6	eleq1d	$⊢ y = A \to (⋃_{x \in y} rank (x) \in On \leftrightarrow ⋃_{x \in A} rank (x) \in On)$
8		vex	$⊢ y \in V$
9		rankon	$⊢ rank (x) \in On$
10	9	rgenw	$⊢ \forall x \in y rank (x) \in On$
11		iunon	$⊢ (y \in V \land \forall x \in y rank (x) \in On) \to ⋃_{x \in y} rank (x) \in On$
12	8 10 11	mp2an	$⊢ ⋃_{x \in y} rank (x) \in On$
13	7 12	vtoclg	$⊢ A \in ⋃ R_{1} [On] \to ⋃_{x \in A} rank (x) \in On$
14		eluni2	$⊢ y \in ⋃ A \leftrightarrow \exists x \in A y \in x$
15		nfv	$⊢ Ⅎ x A \in ⋃ R_{1} [On]$
16		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} rank (x)$
17	16	nfel2	$⊢ Ⅎ x rank (y) \in ⋃_{x \in A} rank (x)$
18		r1elssi	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq ⋃ R_{1} [On]$
19	18	sseld	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to x \in ⋃ R_{1} [On])$
20		rankelb	$⊢ x \in ⋃ R_{1} [On] \to (y \in x \to rank (y) \in rank (x))$
21	19 20	syl6	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to (y \in x \to rank (y) \in rank (x)))$
22		ssiun2	$⊢ x \in A \to rank (x) \subseteq ⋃_{x \in A} rank (x)$
23	22	sseld	$⊢ x \in A \to (rank (y) \in rank (x) \to rank (y) \in ⋃_{x \in A} rank (x))$
24	23	a1i	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to (rank (y) \in rank (x) \to rank (y) \in ⋃_{x \in A} rank (x)))$
25	21 24	syldd	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to (y \in x \to rank (y) \in ⋃_{x \in A} rank (x)))$
26	15 17 25	rexlimd	$⊢ A \in ⋃ R_{1} [On] \to (\exists x \in A y \in x \to rank (y) \in ⋃_{x \in A} rank (x))$
27	14 26	syl5bi	$⊢ A \in ⋃ R_{1} [On] \to (y \in ⋃ A \to rank (y) \in ⋃_{x \in A} rank (x))$
28	27	ralrimiv	$⊢ A \in ⋃ R_{1} [On] \to \forall y \in ⋃ A rank (y) \in ⋃_{x \in A} rank (x)$
29	5 13 28	elrabd	$⊢ A \in ⋃ R_{1} [On] \to ⋃_{x \in A} rank (x) \in \{z \in On \| \forall y \in ⋃ A rank (y) \in z\}$
30		intss1	$⊢ ⋃_{x \in A} rank (x) \in \{z \in On \| \forall y \in ⋃ A rank (y) \in z\} \to ⋂ \{z \in On \| \forall y \in ⋃ A rank (y) \in z\} \subseteq ⋃_{x \in A} rank (x)$
31	29 30	syl	$⊢ A \in ⋃ R_{1} [On] \to ⋂ \{z \in On \| \forall y \in ⋃ A rank (y) \in z\} \subseteq ⋃_{x \in A} rank (x)$
32	3 31	eqsstrd	$⊢ A \in ⋃ R_{1} [On] \to rank (⋃ A) \subseteq ⋃_{x \in A} rank (x)$
33	1	biimpi	$⊢ A \in ⋃ R_{1} [On] \to ⋃ A \in ⋃ R_{1} [On]$
34		elssuni	$⊢ x \in A \to x \subseteq ⋃ A$
35		rankssb	$⊢ ⋃ A \in ⋃ R_{1} [On] \to (x \subseteq ⋃ A \to rank (x) \subseteq rank (⋃ A))$
36	33 34 35	syl2im	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to rank (x) \subseteq rank (⋃ A))$
37	36	ralrimiv	$⊢ A \in ⋃ R_{1} [On] \to \forall x \in A rank (x) \subseteq rank (⋃ A)$
38		iunss	$⊢ ⋃_{x \in A} rank (x) \subseteq rank (⋃ A) \leftrightarrow \forall x \in A rank (x) \subseteq rank (⋃ A)$
39	37 38	sylibr	$⊢ A \in ⋃ R_{1} [On] \to ⋃_{x \in A} rank (x) \subseteq rank (⋃ A)$
40	32 39	eqssd	$⊢ A \in ⋃ R_{1} [On] \to rank (⋃ A) = ⋃_{x \in A} rank (x)$

Metamath Proof Explorer

Theorem rankuni2b

Proof