rankval3b

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, 17-Nov-2014)

		Ref	Expression
	Assertion	rankval3b	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = ⋂ \{x \in On \| \forall y \in A rank (y) \in x\}$

Proof

Step	Hyp	Ref	Expression
1		rankon	$⊢ rank (A) \in On$
2		simprl	$⊢ (A \in ⋃ R_{1} [On] \land (x \in On \land \forall y \in A rank (y) \in x)) \to x \in On$
3		ontri1	$⊢ (rank (A) \in On \land x \in On) \to (rank (A) \subseteq x \leftrightarrow \neg x \in rank (A))$
4	1 2 3	sylancr	$⊢ (A \in ⋃ R_{1} [On] \land (x \in On \land \forall y \in A rank (y) \in x)) \to (rank (A) \subseteq x \leftrightarrow \neg x \in rank (A))$
5	4	con2bid	$⊢ (A \in ⋃ R_{1} [On] \land (x \in On \land \forall y \in A rank (y) \in x)) \to (x \in rank (A) \leftrightarrow \neg rank (A) \subseteq x)$
6		r1elssi	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq ⋃ R_{1} [On]$
7	6	adantr	$⊢ (A \in ⋃ R_{1} [On] \land x \in rank (A)) \to A \subseteq ⋃ R_{1} [On]$
8	7	sselda	$⊢ ((A \in ⋃ R_{1} [On] \land x \in rank (A)) \land y \in A) \to y \in ⋃ R_{1} [On]$
9		rankdmr1	$⊢ rank (A) \in dom R_{1}$
10		r1dmlim	$⊢ Lim dom R_{1}$
11		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
12		ordtr1	$⊢ Ord dom R_{1} \to ((x \in rank (A) \land rank (A) \in dom R_{1}) \to x \in dom R_{1})$
13	10 11 12	mp2b	$⊢ (x \in rank (A) \land rank (A) \in dom R_{1}) \to x \in dom R_{1}$
14	9 13	mpan2	$⊢ x \in rank (A) \to x \in dom R_{1}$
15	14	ad2antlr	$⊢ ((A \in ⋃ R_{1} [On] \land x \in rank (A)) \land y \in A) \to x \in dom R_{1}$
16		rankr1ag	$⊢ (y \in ⋃ R_{1} [On] \land x \in dom R_{1}) \to (y \in R_{1} (x) \leftrightarrow rank (y) \in x)$
17	8 15 16	syl2anc	$⊢ ((A \in ⋃ R_{1} [On] \land x \in rank (A)) \land y \in A) \to (y \in R_{1} (x) \leftrightarrow rank (y) \in x)$
18	17	ralbidva	$⊢ (A \in ⋃ R_{1} [On] \land x \in rank (A)) \to (\forall y \in A y \in R_{1} (x) \leftrightarrow \forall y \in A rank (y) \in x)$
19	18	biimpar	$⊢ ((A \in ⋃ R_{1} [On] \land x \in rank (A)) \land \forall y \in A rank (y) \in x) \to \forall y \in A y \in R_{1} (x)$
20	19	an32s	$⊢ ((A \in ⋃ R_{1} [On] \land \forall y \in A rank (y) \in x) \land x \in rank (A)) \to \forall y \in A y \in R_{1} (x)$
21		dfss3	$⊢ A \subseteq R_{1} (x) \leftrightarrow \forall y \in A y \in R_{1} (x)$
22	20 21	sylibr	$⊢ ((A \in ⋃ R_{1} [On] \land \forall y \in A rank (y) \in x) \land x \in rank (A)) \to A \subseteq R_{1} (x)$
23		simpll	$⊢ ((A \in ⋃ R_{1} [On] \land \forall y \in A rank (y) \in x) \land x \in rank (A)) \to A \in ⋃ R_{1} [On]$
24	14	adantl	$⊢ ((A \in ⋃ R_{1} [On] \land \forall y \in A rank (y) \in x) \land x \in rank (A)) \to x \in dom R_{1}$
25		rankr1bg	$⊢ (A \in ⋃ R_{1} [On] \land x \in dom R_{1}) \to (A \subseteq R_{1} (x) \leftrightarrow rank (A) \subseteq x)$
26	23 24 25	syl2anc	$⊢ ((A \in ⋃ R_{1} [On] \land \forall y \in A rank (y) \in x) \land x \in rank (A)) \to (A \subseteq R_{1} (x) \leftrightarrow rank (A) \subseteq x)$
27	22 26	mpbid	$⊢ ((A \in ⋃ R_{1} [On] \land \forall y \in A rank (y) \in x) \land x \in rank (A)) \to rank (A) \subseteq x$
28	27	ex	$⊢ (A \in ⋃ R_{1} [On] \land \forall y \in A rank (y) \in x) \to (x \in rank (A) \to rank (A) \subseteq x)$
29	28	adantrl	$⊢ (A \in ⋃ R_{1} [On] \land (x \in On \land \forall y \in A rank (y) \in x)) \to (x \in rank (A) \to rank (A) \subseteq x)$
30	5 29	sylbird	$⊢ (A \in ⋃ R_{1} [On] \land (x \in On \land \forall y \in A rank (y) \in x)) \to (\neg rank (A) \subseteq x \to rank (A) \subseteq x)$
31	30	pm2.18d	$⊢ (A \in ⋃ R_{1} [On] \land (x \in On \land \forall y \in A rank (y) \in x)) \to rank (A) \subseteq x$
32	31	ex	$⊢ A \in ⋃ R_{1} [On] \to ((x \in On \land \forall y \in A rank (y) \in x) \to rank (A) \subseteq x)$
33	32	alrimiv	$⊢ A \in ⋃ R_{1} [On] \to \forall x ((x \in On \land \forall y \in A rank (y) \in x) \to rank (A) \subseteq x)$
34		ssintab	$⊢ rank (A) \subseteq ⋂ \{x \| (x \in On \land \forall y \in A rank (y) \in x)\} \leftrightarrow \forall x ((x \in On \land \forall y \in A rank (y) \in x) \to rank (A) \subseteq x)$
35	33 34	sylibr	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \subseteq ⋂ \{x \| (x \in On \land \forall y \in A rank (y) \in x)\}$
36		df-rab	$⊢ \{x \in On \| \forall y \in A rank (y) \in x\} = \{x \| (x \in On \land \forall y \in A rank (y) \in x)\}$
37	36	inteqi	$⊢ ⋂ \{x \in On \| \forall y \in A rank (y) \in x\} = ⋂ \{x \| (x \in On \land \forall y \in A rank (y) \in x)\}$
38	35 37	sseqtrrdi	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \subseteq ⋂ \{x \in On \| \forall y \in A rank (y) \in x\}$
39		rankelb	$⊢ A \in ⋃ R_{1} [On] \to (y \in A \to rank (y) \in rank (A))$
40	39	ralrimiv	$⊢ A \in ⋃ R_{1} [On] \to \forall y \in A rank (y) \in rank (A)$
41		eleq2	$⊢ x = rank (A) \to (rank (y) \in x \leftrightarrow rank (y) \in rank (A))$
42	41	ralbidv	$⊢ x = rank (A) \to (\forall y \in A rank (y) \in x \leftrightarrow \forall y \in A rank (y) \in rank (A))$
43	42	onintss	$⊢ rank (A) \in On \to (\forall y \in A rank (y) \in rank (A) \to ⋂ \{x \in On \| \forall y \in A rank (y) \in x\} \subseteq rank (A))$
44	1 40 43	mpsyl	$⊢ A \in ⋃ R_{1} [On] \to ⋂ \{x \in On \| \forall y \in A rank (y) \in x\} \subseteq rank (A)$
45	38 44	eqssd	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = ⋂ \{x \in On \| \forall y \in A rank (y) \in x\}$

Metamath Proof Explorer

Theorem rankval3b

Proof