rankval4b

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. This variant of rankval4 does not use Regularity, and so requires the assumption that A is in the range of R1 . (Contributed by BTernaryTau, 19-Jan-2026)

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

Proof

Step	Hyp	Ref	Expression
1		r1wf	$⊢ R_{1} (⋃_{x \in A} suc rank (x)) \in ⋃ R_{1} [On]$
2		rankon	$⊢ rank (x) \in On$
3	2	onsuci	$⊢ suc rank (x) \in On$
4	3	rgenw	$⊢ \forall x \in A suc rank (x) \in On$
5		iunon	$⊢ (A \in ⋃ R_{1} [On] \land \forall x \in A suc rank (x) \in On) \to ⋃_{x \in A} suc rank (x) \in On$
6	4 5	mpan2	$⊢ A \in ⋃ R_{1} [On] \to ⋃_{x \in A} suc rank (x) \in On$
7		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)))$
8	3 6 7	sylancr	$⊢ A \in ⋃ R_{1} [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)))$
9		ssiun2	$⊢ x \in A \to suc rank (x) \subseteq ⋃_{x \in A} suc rank (x)$
10	8 9	impel	$⊢ (A \in ⋃ R_{1} [On] \land x \in A) \to R_{1} (suc rank (x)) \subseteq R_{1} (⋃_{x \in A} suc rank (x))$
11		elwf	$⊢ (A \in ⋃ R_{1} [On] \land x \in A) \to x \in ⋃ R_{1} [On]$
12		rankidb	$⊢ x \in ⋃ R_{1} [On] \to x \in R_{1} (suc rank (x))$
13	11 12	syl	$⊢ (A \in ⋃ R_{1} [On] \land x \in A) \to x \in R_{1} (suc rank (x))$
14	10 13	sseldd	$⊢ (A \in ⋃ R_{1} [On] \land x \in A) \to x \in R_{1} (⋃_{x \in A} suc rank (x))$
15	14	ex	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to x \in R_{1} (⋃_{x \in A} suc rank (x)))$
16	15	alrimiv	$⊢ A \in ⋃ R_{1} [On] \to \forall x (x \in A \to x \in R_{1} (⋃_{x \in A} suc rank (x)))$
17		nfcv	$⊢ \underline{Ⅎ} x A$
18		nfcv	$⊢ \underline{Ⅎ} x R_{1}$
19		nfiu1	$⊢ \underline{Ⅎ} x ⋃_{x \in A} suc rank (x)$
20	18 19	nffv	$⊢ \underline{Ⅎ} x R_{1} (⋃_{x \in A} suc rank (x))$
21	17 20	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)))$
22	16 21	sylibr	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq R_{1} (⋃_{x \in A} suc rank (x))$
23		rankssb	$⊢ R_{1} (⋃_{x \in A} suc rank (x)) \in ⋃ R_{1} [On] \to (A \subseteq R_{1} (⋃_{x \in A} suc rank (x)) \to rank (A) \subseteq rank (R_{1} (⋃_{x \in A} suc rank (x))))$
24	1 22 23	mpsyl	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \subseteq rank (R_{1} (⋃_{x \in A} suc rank (x)))$
25		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))$
26	6 25	sylan	$⊢ (A \in ⋃ R_{1} [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))$
27	26	ss2rabdv	$⊢ A \in ⋃ R_{1} [On] \to \{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)\}$
28		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\}$
29	27 28	syl	$⊢ A \in ⋃ R_{1} [On] \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\}$
30		rankval2b	$⊢ R_{1} (⋃_{x \in A} suc rank (x)) \in ⋃ R_{1} [On] \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)\}$
31	1 30	mp1i	$⊢ A \in ⋃ R_{1} [On] \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)\}$
32		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)$
33	6 32	syl	$⊢ A \in ⋃ R_{1} [On] \to ⋂ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\} = ⋃_{x \in A} suc rank (x)$
34	33	eqcomd	$⊢ A \in ⋃ R_{1} [On] \to ⋃_{x \in A} suc rank (x) = ⋂ \{y \in On \| ⋃_{x \in A} suc rank (x) \subseteq y\}$
35	29 31 34	3sstr4d	$⊢ A \in ⋃ R_{1} [On] \to rank (R_{1} (⋃_{x \in A} suc rank (x))) \subseteq ⋃_{x \in A} suc rank (x)$
36	24 35	sstrd	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \subseteq ⋃_{x \in A} suc rank (x)$
37		rankelb	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to rank (x) \in rank (A))$
38		rankon	$⊢ rank (A) \in On$
39	2 38	onsucssi	$⊢ rank (x) \in rank (A) \leftrightarrow suc rank (x) \subseteq rank (A)$
40	37 39	imbitrdi	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to suc rank (x) \subseteq rank (A))$
41	40	ralrimiv	$⊢ A \in ⋃ R_{1} [On] \to \forall x \in A suc rank (x) \subseteq rank (A)$
42		iunss	$⊢ ⋃_{x \in A} suc rank (x) \subseteq rank (A) \leftrightarrow \forall x \in A suc rank (x) \subseteq rank (A)$
43	41 42	sylibr	$⊢ A \in ⋃ R_{1} [On] \to ⋃_{x \in A} suc rank (x) \subseteq rank (A)$
44	36 43	eqssd	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = ⋃_{x \in A} suc rank (x)$

Metamath Proof Explorer

Theorem rankval4b

Proof