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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
11	10	simpri	$⊢ Lim dom R_{1}$
12		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
13		ordtr1	$⊢ Ord dom R_{1} \to ((x \in rank (A) \land rank (A) \in dom R_{1}) \to x \in dom R_{1})$
14	11 12 13	mp2b	$⊢ (x \in rank (A) \land rank (A) \in dom R_{1}) \to x \in dom R_{1}$
15	9 14	mpan2	$⊢ x \in rank (A) \to x \in dom R_{1}$
16	15	ad2antlr	$⊢ ((A \in ⋃ R_{1} [On] \land x \in rank (A)) \land y \in A) \to x \in dom R_{1}$
17		rankr1ag	$⊢ (y \in ⋃ R_{1} [On] \land x \in dom R_{1}) \to (y \in R_{1} (x) \leftrightarrow rank (y) \in x)$
18	8 16 17	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)$
19	18	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)$
20	19	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)$
21	20	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)$
22		dfss3	$⊢ A \subseteq R_{1} (x) \leftrightarrow \forall y \in A y \in R_{1} (x)$
23	21 22	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)$
24		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]$
25	15	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}$
26		rankr1bg	$⊢ (A \in ⋃ R_{1} [On] \land x \in dom R_{1}) \to (A \subseteq R_{1} (x) \leftrightarrow rank (A) \subseteq x)$
27	24 25 26	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)$
28	23 27	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$
29	28	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)$
30	29	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)$
31	5 30	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)$
32	31	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$
33	32	ex	$⊢ A \in ⋃ R_{1} [On] \to ((x \in On \land \forall y \in A rank (y) \in x) \to rank (A) \subseteq x)$
34	33	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)$
35		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)$
36	34 35	sylibr	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \subseteq ⋂ \{x \| (x \in On \land \forall y \in A rank (y) \in x)\}$
37		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)\}$
38	37	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)\}$
39	36 38	sseqtrrdi	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \subseteq ⋂ \{x \in On \| \forall y \in A rank (y) \in x\}$
40		rankelb	$⊢ A \in ⋃ R_{1} [On] \to (y \in A \to rank (y) \in rank (A))$
41	40	ralrimiv	$⊢ A \in ⋃ R_{1} [On] \to \forall y \in A rank (y) \in rank (A)$
42		eleq2	$⊢ x = rank (A) \to (rank (y) \in x \leftrightarrow rank (y) \in rank (A))$
43	42	ralbidv	$⊢ x = rank (A) \to (\forall y \in A rank (y) \in x \leftrightarrow \forall y \in A rank (y) \in rank (A))$
44	43	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))$
45	1 41 44	mpsyl	$⊢ A \in ⋃ R_{1} [On] \to ⋂ \{x \in On \| \forall y \in A rank (y) \in x\} \subseteq rank (A)$
46	39 45	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