Theorem rankc1

Description: A relationship that can be used for computation of rank. (Contributed by NM, 16-Sep-2006)

	Ref	Expression
Hypothesis	rankr1b.1	$$⊢A\in \mathrm{V}$$
Assertion	rankc1	$$⊢\forall x\in A\mathrm{rank}\left(x\right)\in \mathrm{rank}\left(\bigcup A\right)\leftrightarrow \mathrm{rank}\left(A\right)=\mathrm{rank}\left(\bigcup A\right)$$

Proof

Step	Hyp	Ref	Expression
1		rankr1b.1	$$⊢A\in \mathrm{V}$$
2	1	rankuniss	$$⊢\mathrm{rank}\left(\bigcup A\right)\subseteq \mathrm{rank}\left(A\right)$$
3	2	biantru	$$⊢\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(\bigcup A\right)\leftrightarrow \left(\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(\bigcup A\right)\wedge \mathrm{rank}\left(\bigcup A\right)\subseteq \mathrm{rank}\left(A\right)\right)$$
4		iunss	$$⊢\bigcup _{x\in A}\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(\bigcup A\right)\leftrightarrow \forall x\in A\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(\bigcup A\right)$$
5	1	rankval4	$$⊢\mathrm{rank}\left(A\right)=\bigcup _{x\in A}\mathrm{suc}\mathrm{rank}\left(x\right)$$
6	5	sseq1i	$$⊢\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(\bigcup A\right)\leftrightarrow \bigcup _{x\in A}\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(\bigcup A\right)$$
7		rankon	$$⊢\mathrm{rank}\left(x\right)\in \mathrm{On}$$
8		rankon	$$⊢\mathrm{rank}\left(\bigcup A\right)\in \mathrm{On}$$
9	7 8	onsucssi	$$⊢\mathrm{rank}\left(x\right)\in \mathrm{rank}\left(\bigcup A\right)\leftrightarrow \mathrm{suc}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(\bigcup A\right)$$
10	9	ralbii	$$⊢\forall x\in A\mathrm{rank}\left(x\right)\in \mathrm{rank}\left(\bigcup A\right)\leftrightarrow \forall x\in A\mathrm{suc}\mathrm{rank}\left(x\right)\subseteq \mathrm{rank}\left(\bigcup A\right)$$
11	4 6 10	3bitr4ri	$$⊢\forall x\in A\mathrm{rank}\left(x\right)\in \mathrm{rank}\left(\bigcup A\right)\leftrightarrow \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(\bigcup A\right)$$
12		eqss	$$⊢\mathrm{rank}\left(A\right)=\mathrm{rank}\left(\bigcup A\right)\leftrightarrow \left(\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(\bigcup A\right)\wedge \mathrm{rank}\left(\bigcup A\right)\subseteq \mathrm{rank}\left(A\right)\right)$$
13	3 11 12	3bitr4i	$$⊢\forall x\in A\mathrm{rank}\left(x\right)\in \mathrm{rank}\left(\bigcup A\right)\leftrightarrow \mathrm{rank}\left(A\right)=\mathrm{rank}\left(\bigcup A\right)$$