tcrank

Description: This theorem expresses two different facts from the two subset implications in this equality. In the forward direction, it says that the transitive closure has members of every rank below A . Stated another way, to construct a set at a given rank, you have to climb the entire hierarchy of ordinals below ( rankA ) , constructing at least one set at each level in order to move up the ranks. In the reverse direction, it says that every member of ( TCA ) has a rank below the rank of A , since intuitively it contains only the members of A and the members of those and so on, but nothing "bigger" than A . (Contributed by Mario Carneiro, 23-Jun-2013)

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

Proof

Step	Hyp	Ref	Expression
1		rankwflemb	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists y \in On A \in R_{1} (suc y)$
2		onsuc	$⊢ y \in On \to suc y \in On$
3		fveq2	$⊢ x = y \to R_{1} (x) = R_{1} (y)$
4	3	raleqdv	$⊢ x = y \to (\forall z \in R_{1} (x) rank (z) \subseteq rank [TC (z)] \leftrightarrow \forall z \in R_{1} (y) rank (z) \subseteq rank [TC (z)])$
5		fveq2	$⊢ z = u \to rank (z) = rank (u)$
6		fveq2	$⊢ z = u \to TC (z) = TC (u)$
7	6	imaeq2d	$⊢ z = u \to rank [TC (z)] = rank [TC (u)]$
8	5 7	sseq12d	$⊢ z = u \to (rank (z) \subseteq rank [TC (z)] \leftrightarrow rank (u) \subseteq rank [TC (u)])$
9	8	cbvralvw	$⊢ \forall z \in R_{1} (y) rank (z) \subseteq rank [TC (z)] \leftrightarrow \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]$
10	4 9	bitrdi	$⊢ x = y \to (\forall z \in R_{1} (x) rank (z) \subseteq rank [TC (z)] \leftrightarrow \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)])$
11		fveq2	$⊢ x = suc y \to R_{1} (x) = R_{1} (suc y)$
12	11	raleqdv	$⊢ x = suc y \to (\forall z \in R_{1} (x) rank (z) \subseteq rank [TC (z)] \leftrightarrow \forall z \in R_{1} (suc y) rank (z) \subseteq rank [TC (z)])$
13		simpr	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land (z \in R_{1} (x) \land w \in rank (z))) \to (z \in R_{1} (x) \land w \in rank (z))$
14		simprl	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land (z \in R_{1} (x) \land w \in rank (z))) \to z \in R_{1} (x)$
15		simplr	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land (z \in R_{1} (x) \land w \in rank (z))) \to \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]$
16		rankr1ai	$⊢ z \in R_{1} (x) \to rank (z) \in x$
17		fveq2	$⊢ y = rank (z) \to R_{1} (y) = R_{1} (rank (z))$
18	17	raleqdv	$⊢ y = rank (z) \to (\forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)] \leftrightarrow \forall u \in R_{1} (rank (z)) rank (u) \subseteq rank [TC (u)])$
19	18	rspcv	$⊢ rank (z) \in x \to (\forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)] \to \forall u \in R_{1} (rank (z)) rank (u) \subseteq rank [TC (u)])$
20	16 19	syl	$⊢ z \in R_{1} (x) \to (\forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)] \to \forall u \in R_{1} (rank (z)) rank (u) \subseteq rank [TC (u)])$
21		r1elwf	$⊢ z \in R_{1} (x) \to z \in ⋃ R_{1} [On]$
22		r1rankidb	$⊢ z \in ⋃ R_{1} [On] \to z \subseteq R_{1} (rank (z))$
23		ssralv	$⊢ z \subseteq R_{1} (rank (z)) \to (\forall u \in R_{1} (rank (z)) rank (u) \subseteq rank [TC (u)] \to \forall u \in z rank (u) \subseteq rank [TC (u)])$
24	21 22 23	3syl	$⊢ z \in R_{1} (x) \to (\forall u \in R_{1} (rank (z)) rank (u) \subseteq rank [TC (u)] \to \forall u \in z rank (u) \subseteq rank [TC (u)])$
25	20 24	syld	$⊢ z \in R_{1} (x) \to (\forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)] \to \forall u \in z rank (u) \subseteq rank [TC (u)])$
26	14 15 25	sylc	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land (z \in R_{1} (x) \land w \in rank (z))) \to \forall u \in z rank (u) \subseteq rank [TC (u)]$
27		rankval3b	$⊢ z \in ⋃ R_{1} [On] \to rank (z) = ⋂ \{x \in On \| \forall u \in z rank (u) \in x\}$
28	27	eleq2d	$⊢ z \in ⋃ R_{1} [On] \to (w \in rank (z) \leftrightarrow w \in ⋂ \{x \in On \| \forall u \in z rank (u) \in x\})$
29	28	biimpd	$⊢ z \in ⋃ R_{1} [On] \to (w \in rank (z) \to w \in ⋂ \{x \in On \| \forall u \in z rank (u) \in x\})$
30		rankon	$⊢ rank (z) \in On$
31	30	oneli	$⊢ w \in rank (z) \to w \in On$
32		eleq2w	$⊢ x = w \to (rank (u) \in x \leftrightarrow rank (u) \in w)$
33	32	ralbidv	$⊢ x = w \to (\forall u \in z rank (u) \in x \leftrightarrow \forall u \in z rank (u) \in w)$
34	33	onnminsb	$⊢ w \in On \to (w \in ⋂ \{x \in On \| \forall u \in z rank (u) \in x\} \to \neg \forall u \in z rank (u) \in w)$
35	31 34	syl	$⊢ w \in rank (z) \to (w \in ⋂ \{x \in On \| \forall u \in z rank (u) \in x\} \to \neg \forall u \in z rank (u) \in w)$
36	29 35	sylcom	$⊢ z \in ⋃ R_{1} [On] \to (w \in rank (z) \to \neg \forall u \in z rank (u) \in w)$
37	21 36	syl	$⊢ z \in R_{1} (x) \to (w \in rank (z) \to \neg \forall u \in z rank (u) \in w)$
38	37	imp	$⊢ (z \in R_{1} (x) \land w \in rank (z)) \to \neg \forall u \in z rank (u) \in w$
39		rexnal	$⊢ \exists u \in z \neg rank (u) \in w \leftrightarrow \neg \forall u \in z rank (u) \in w$
40	38 39	sylibr	$⊢ (z \in R_{1} (x) \land w \in rank (z)) \to \exists u \in z \neg rank (u) \in w$
41	40	adantl	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land (z \in R_{1} (x) \land w \in rank (z))) \to \exists u \in z \neg rank (u) \in w$
42		r19.29	$⊢ (\forall u \in z rank (u) \subseteq rank [TC (u)] \land \exists u \in z \neg rank (u) \in w) \to \exists u \in z (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)$
43	26 41 42	syl2anc	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land (z \in R_{1} (x) \land w \in rank (z))) \to \exists u \in z (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)$
44		simp2	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to u \in z$
45		tcid	$⊢ z \in V \to z \subseteq TC (z)$
46	45	elv	$⊢ z \subseteq TC (z)$
47	46	sseli	$⊢ u \in z \to u \in TC (z)$
48		fveqeq2	$⊢ x = u \to (rank (x) = w \leftrightarrow rank (u) = w)$
49	48	rspcev	$⊢ (u \in TC (z) \land rank (u) = w) \to \exists x \in TC (z) rank (x) = w$
50	49	ex	$⊢ u \in TC (z) \to (rank (u) = w \to \exists x \in TC (z) rank (x) = w)$
51	44 47 50	3syl	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to (rank (u) = w \to \exists x \in TC (z) rank (x) = w)$
52		simp3l	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to rank (u) \subseteq rank [TC (u)]$
53	52	sseld	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to (w \in rank (u) \to w \in rank [TC (u)])$
54		simp1l	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to z \in R_{1} (x)$
55		rankf	$⊢ rank : ⋃ R_{1} [On] ⟶ On$
56		ffn	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to rank Fn ⋃ R_{1} [On]$
57	55 56	ax-mp	$⊢ rank Fn ⋃ R_{1} [On]$
58		r1tr	$⊢ Tr R_{1} (x)$
59		trel	$⊢ Tr R_{1} (x) \to ((u \in z \land z \in R_{1} (x)) \to u \in R_{1} (x))$
60	58 59	ax-mp	$⊢ (u \in z \land z \in R_{1} (x)) \to u \in R_{1} (x)$
61		r1elwf	$⊢ u \in R_{1} (x) \to u \in ⋃ R_{1} [On]$
62		tcwf	$⊢ u \in ⋃ R_{1} [On] \to TC (u) \in ⋃ R_{1} [On]$
63		fvex	$⊢ TC (u) \in V$
64	63	r1elss	$⊢ TC (u) \in ⋃ R_{1} [On] \leftrightarrow TC (u) \subseteq ⋃ R_{1} [On]$
65	62 64	sylib	$⊢ u \in ⋃ R_{1} [On] \to TC (u) \subseteq ⋃ R_{1} [On]$
66	60 61 65	3syl	$⊢ (u \in z \land z \in R_{1} (x)) \to TC (u) \subseteq ⋃ R_{1} [On]$
67		fvelimab	$⊢ (rank Fn ⋃ R_{1} [On] \land TC (u) \subseteq ⋃ R_{1} [On]) \to (w \in rank [TC (u)] \leftrightarrow \exists x \in TC (u) rank (x) = w)$
68	57 66 67	sylancr	$⊢ (u \in z \land z \in R_{1} (x)) \to (w \in rank [TC (u)] \leftrightarrow \exists x \in TC (u) rank (x) = w)$
69		vex	$⊢ z \in V$
70	69	tcel	$⊢ u \in z \to TC (u) \subseteq TC (z)$
71		ssrexv	$⊢ TC (u) \subseteq TC (z) \to (\exists x \in TC (u) rank (x) = w \to \exists x \in TC (z) rank (x) = w)$
72	70 71	syl	$⊢ u \in z \to (\exists x \in TC (u) rank (x) = w \to \exists x \in TC (z) rank (x) = w)$
73	72	adantr	$⊢ (u \in z \land z \in R_{1} (x)) \to (\exists x \in TC (u) rank (x) = w \to \exists x \in TC (z) rank (x) = w)$
74	68 73	sylbid	$⊢ (u \in z \land z \in R_{1} (x)) \to (w \in rank [TC (u)] \to \exists x \in TC (z) rank (x) = w)$
75	44 54 74	syl2anc	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to (w \in rank [TC (u)] \to \exists x \in TC (z) rank (x) = w)$
76	53 75	syld	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to (w \in rank (u) \to \exists x \in TC (z) rank (x) = w)$
77		rankon	$⊢ rank (u) \in On$
78		eloni	$⊢ rank (u) \in On \to Ord rank (u)$
79		eloni	$⊢ w \in On \to Ord w$
80		ordtri3or	$⊢ (Ord rank (u) \land Ord w) \to (rank (u) \in w \lor rank (u) = w \lor w \in rank (u))$
81	78 79 80	syl2an	$⊢ (rank (u) \in On \land w \in On) \to (rank (u) \in w \lor rank (u) = w \lor w \in rank (u))$
82	77 31 81	sylancr	$⊢ w \in rank (z) \to (rank (u) \in w \lor rank (u) = w \lor w \in rank (u))$
83		3orass	$⊢ (rank (u) \in w \lor rank (u) = w \lor w \in rank (u)) \leftrightarrow (rank (u) \in w \lor (rank (u) = w \lor w \in rank (u)))$
84	82 83	sylib	$⊢ w \in rank (z) \to (rank (u) \in w \lor (rank (u) = w \lor w \in rank (u)))$
85	84	orcanai	$⊢ (w \in rank (z) \land \neg rank (u) \in w) \to (rank (u) = w \lor w \in rank (u))$
86	85	ad2ant2l	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to (rank (u) = w \lor w \in rank (u))$
87	86	3adant2	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to (rank (u) = w \lor w \in rank (u))$
88	51 76 87	mpjaod	$⊢ ((z \in R_{1} (x) \land w \in rank (z)) \land u \in z \land (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w)) \to \exists x \in TC (z) rank (x) = w$
89	88	rexlimdv3a	$⊢ (z \in R_{1} (x) \land w \in rank (z)) \to (\exists u \in z (rank (u) \subseteq rank [TC (u)] \land \neg rank (u) \in w) \to \exists x \in TC (z) rank (x) = w)$
90	13 43 89	sylc	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land (z \in R_{1} (x) \land w \in rank (z))) \to \exists x \in TC (z) rank (x) = w$
91	90	expr	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land z \in R_{1} (x)) \to (w \in rank (z) \to \exists x \in TC (z) rank (x) = w)$
92		tcwf	$⊢ z \in ⋃ R_{1} [On] \to TC (z) \in ⋃ R_{1} [On]$
93		r1elssi	$⊢ TC (z) \in ⋃ R_{1} [On] \to TC (z) \subseteq ⋃ R_{1} [On]$
94		fvelimab	$⊢ (rank Fn ⋃ R_{1} [On] \land TC (z) \subseteq ⋃ R_{1} [On]) \to (w \in rank [TC (z)] \leftrightarrow \exists x \in TC (z) rank (x) = w)$
95	93 94	sylan2	$⊢ (rank Fn ⋃ R_{1} [On] \land TC (z) \in ⋃ R_{1} [On]) \to (w \in rank [TC (z)] \leftrightarrow \exists x \in TC (z) rank (x) = w)$
96	57 92 95	sylancr	$⊢ z \in ⋃ R_{1} [On] \to (w \in rank [TC (z)] \leftrightarrow \exists x \in TC (z) rank (x) = w)$
97	21 96	syl	$⊢ z \in R_{1} (x) \to (w \in rank [TC (z)] \leftrightarrow \exists x \in TC (z) rank (x) = w)$
98	97	adantl	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land z \in R_{1} (x)) \to (w \in rank [TC (z)] \leftrightarrow \exists x \in TC (z) rank (x) = w)$
99	91 98	sylibrd	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land z \in R_{1} (x)) \to (w \in rank (z) \to w \in rank [TC (z)])$
100	99	ssrdv	$⊢ ((x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \land z \in R_{1} (x)) \to rank (z) \subseteq rank [TC (z)]$
101	100	ralrimiva	$⊢ (x \in On \land \forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)]) \to \forall z \in R_{1} (x) rank (z) \subseteq rank [TC (z)]$
102	101	ex	$⊢ x \in On \to (\forall y \in x \forall u \in R_{1} (y) rank (u) \subseteq rank [TC (u)] \to \forall z \in R_{1} (x) rank (z) \subseteq rank [TC (z)])$
103	10 12 102	tfis3	$⊢ suc y \in On \to \forall z \in R_{1} (suc y) rank (z) \subseteq rank [TC (z)]$
104		fveq2	$⊢ z = A \to rank (z) = rank (A)$
105		fveq2	$⊢ z = A \to TC (z) = TC (A)$
106	105	imaeq2d	$⊢ z = A \to rank [TC (z)] = rank [TC (A)]$
107	104 106	sseq12d	$⊢ z = A \to (rank (z) \subseteq rank [TC (z)] \leftrightarrow rank (A) \subseteq rank [TC (A)])$
108	107	rspccv	$⊢ \forall z \in R_{1} (suc y) rank (z) \subseteq rank [TC (z)] \to (A \in R_{1} (suc y) \to rank (A) \subseteq rank [TC (A)])$
109	2 103 108	3syl	$⊢ y \in On \to (A \in R_{1} (suc y) \to rank (A) \subseteq rank [TC (A)])$
110	109	rexlimiv	$⊢ \exists y \in On A \in R_{1} (suc y) \to rank (A) \subseteq rank [TC (A)]$
111	1 110	sylbi	$⊢ A \in ⋃ R_{1} [On] \to rank (A) \subseteq rank [TC (A)]$
112		tcvalg	$⊢ A \in ⋃ R_{1} [On] \to TC (A) = ⋂ \{x \| (A \subseteq x \land Tr x)\}$
113		r1rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq R_{1} (rank (A))$
114		r1tr	$⊢ Tr R_{1} (rank (A))$
115		fvex	$⊢ R_{1} (rank (A)) \in V$
116		sseq2	$⊢ x = R_{1} (rank (A)) \to (A \subseteq x \leftrightarrow A \subseteq R_{1} (rank (A)))$
117		treq	$⊢ x = R_{1} (rank (A)) \to (Tr x \leftrightarrow Tr R_{1} (rank (A)))$
118	116 117	anbi12d	$⊢ x = R_{1} (rank (A)) \to ((A \subseteq x \land Tr x) \leftrightarrow (A \subseteq R_{1} (rank (A)) \land Tr R_{1} (rank (A))))$
119	115 118	elab	$⊢ R_{1} (rank (A)) \in \{x \| (A \subseteq x \land Tr x)\} \leftrightarrow (A \subseteq R_{1} (rank (A)) \land Tr R_{1} (rank (A)))$
120		intss1	$⊢ R_{1} (rank (A)) \in \{x \| (A \subseteq x \land Tr x)\} \to ⋂ \{x \| (A \subseteq x \land Tr x)\} \subseteq R_{1} (rank (A))$
121	119 120	sylbir	$⊢ (A \subseteq R_{1} (rank (A)) \land Tr R_{1} (rank (A))) \to ⋂ \{x \| (A \subseteq x \land Tr x)\} \subseteq R_{1} (rank (A))$
122	113 114 121	sylancl	$⊢ A \in ⋃ R_{1} [On] \to ⋂ \{x \| (A \subseteq x \land Tr x)\} \subseteq R_{1} (rank (A))$
123	112 122	eqsstrd	$⊢ A \in ⋃ R_{1} [On] \to TC (A) \subseteq R_{1} (rank (A))$
124		imass2	$⊢ TC (A) \subseteq R_{1} (rank (A)) \to rank [TC (A)] \subseteq rank [R_{1} (rank (A))]$
125		ffun	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to Fun rank$
126	55 125	ax-mp	$⊢ Fun rank$
127		fvelima	$⊢ (Fun rank \land x \in rank [R_{1} (rank (A))]) \to \exists y \in R_{1} (rank (A)) rank (y) = x$
128	126 127	mpan	$⊢ x \in rank [R_{1} (rank (A))] \to \exists y \in R_{1} (rank (A)) rank (y) = x$
129		rankr1ai	$⊢ y \in R_{1} (rank (A)) \to rank (y) \in rank (A)$
130		eleq1	$⊢ rank (y) = x \to (rank (y) \in rank (A) \leftrightarrow x \in rank (A))$
131	129 130	syl5ibcom	$⊢ y \in R_{1} (rank (A)) \to (rank (y) = x \to x \in rank (A))$
132	131	rexlimiv	$⊢ \exists y \in R_{1} (rank (A)) rank (y) = x \to x \in rank (A)$
133	128 132	syl	$⊢ x \in rank [R_{1} (rank (A))] \to x \in rank (A)$
134	133	ssriv	$⊢ rank [R_{1} (rank (A))] \subseteq rank (A)$
135	124 134	sstrdi	$⊢ TC (A) \subseteq R_{1} (rank (A)) \to rank [TC (A)] \subseteq rank (A)$
136	123 135	syl	$⊢ A \in ⋃ R_{1} [On] \to rank [TC (A)] \subseteq rank (A)$
137	111 136	eqssd	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = rank [TC (A)]$

Metamath Proof Explorer

Theorem tcrank

Proof