r1tskina

Description: There is a direct relationship between transitive Tarski classes and inaccessible cardinals: the Tarski classes that occur in the cumulative hierarchy are exactly at the strongly inaccessible cardinals. (Contributed by Mario Carneiro, 8-Jun-2013)

		Ref	Expression
	Assertion	r1tskina	$⊢ A \in On \to (R_{1} (A) \in Tarski \leftrightarrow (A = \emptyset \lor A \in Inacc))$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
2		simplr	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to R_{1} (A) \in Tarski$
3		simpll	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to A \in On$
4		onwf	$⊢ On \subseteq ⋃ R_{1} [On]$
5	4	sseli	$⊢ A \in On \to A \in ⋃ R_{1} [On]$
6		eqid	$⊢ rank (A) = rank (A)$
7		rankr1c	$⊢ A \in ⋃ R_{1} [On] \to (rank (A) = rank (A) \leftrightarrow (\neg A \in R_{1} (rank (A)) \land A \in R_{1} (suc rank (A))))$
8	6 7	mpbii	$⊢ A \in ⋃ R_{1} [On] \to (\neg A \in R_{1} (rank (A)) \land A \in R_{1} (suc rank (A)))$
9	5 8	syl	$⊢ A \in On \to (\neg A \in R_{1} (rank (A)) \land A \in R_{1} (suc rank (A)))$
10	9	simpld	$⊢ A \in On \to \neg A \in R_{1} (rank (A))$
11		r1fnon	$⊢ R_{1} Fn On$
12	11	fndmi	$⊢ dom R_{1} = On$
13	12	eleq2i	$⊢ A \in dom R_{1} \leftrightarrow A \in On$
14		rankonid	$⊢ A \in dom R_{1} \leftrightarrow rank (A) = A$
15	13 14	bitr3i	$⊢ A \in On \leftrightarrow rank (A) = A$
16		fveq2	$⊢ rank (A) = A \to R_{1} (rank (A)) = R_{1} (A)$
17	15 16	sylbi	$⊢ A \in On \to R_{1} (rank (A)) = R_{1} (A)$
18	10 17	neleqtrd	$⊢ A \in On \to \neg A \in R_{1} (A)$
19	18	adantl	$⊢ (R_{1} (A) \in Tarski \land A \in On) \to \neg A \in R_{1} (A)$
20		onssr1	$⊢ A \in dom R_{1} \to A \subseteq R_{1} (A)$
21	13 20	sylbir	$⊢ A \in On \to A \subseteq R_{1} (A)$
22		tsken	$⊢ (R_{1} (A) \in Tarski \land A \subseteq R_{1} (A)) \to (A \approx R_{1} (A) \lor A \in R_{1} (A))$
23	21 22	sylan2	$⊢ (R_{1} (A) \in Tarski \land A \in On) \to (A \approx R_{1} (A) \lor A \in R_{1} (A))$
24	23	ord	$⊢ (R_{1} (A) \in Tarski \land A \in On) \to (\neg A \approx R_{1} (A) \to A \in R_{1} (A))$
25	19 24	mt3d	$⊢ (R_{1} (A) \in Tarski \land A \in On) \to A \approx R_{1} (A)$
26	2 3 25	syl2anc	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to A \approx R_{1} (A)$
27		carden2b	$⊢ A \approx R_{1} (A) \to card (A) = card (R_{1} (A))$
28	26 27	syl	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to card (A) = card (R_{1} (A))$
29		simpl	$⊢ (A \in On \land R_{1} (A) \in Tarski) \to A \in On$
30		simplr	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land x \in A) \to R_{1} (A) \in Tarski$
31	21	adantr	$⊢ (A \in On \land R_{1} (A) \in Tarski) \to A \subseteq R_{1} (A)$
32	31	sselda	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land x \in A) \to x \in R_{1} (A)$
33		tsksdom	$⊢ (R_{1} (A) \in Tarski \land x \in R_{1} (A)) \to x ≺ R_{1} (A)$
34	30 32 33	syl2anc	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land x \in A) \to x ≺ R_{1} (A)$
35		simpll	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land x \in A) \to A \in On$
36	25	ensymd	$⊢ (R_{1} (A) \in Tarski \land A \in On) \to R_{1} (A) \approx A$
37	30 35 36	syl2anc	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land x \in A) \to R_{1} (A) \approx A$
38		sdomentr	$⊢ (x ≺ R_{1} (A) \land R_{1} (A) \approx A) \to x ≺ A$
39	34 37 38	syl2anc	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land x \in A) \to x ≺ A$
40	39	ralrimiva	$⊢ (A \in On \land R_{1} (A) \in Tarski) \to \forall x \in A x ≺ A$
41		iscard	$⊢ card (A) = A \leftrightarrow (A \in On \land \forall x \in A x ≺ A)$
42	29 40 41	sylanbrc	$⊢ (A \in On \land R_{1} (A) \in Tarski) \to card (A) = A$
43	42	adantr	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to card (A) = A$
44	28 43	eqtr3d	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to card (R_{1} (A)) = A$
45		r10	$⊢ R_{1} (\emptyset) = \emptyset$
46		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
47	46	biimpar	$⊢ (A \in On \land A \neq \emptyset) \to \emptyset \in A$
48		r1sdom	$⊢ (A \in On \land \emptyset \in A) \to R_{1} (\emptyset) ≺ R_{1} (A)$
49	47 48	syldan	$⊢ (A \in On \land A \neq \emptyset) \to R_{1} (\emptyset) ≺ R_{1} (A)$
50	45 49	eqbrtrrid	$⊢ (A \in On \land A \neq \emptyset) \to \emptyset ≺ R_{1} (A)$
51		fvex	$⊢ R_{1} (A) \in V$
52	51	0sdom	$⊢ \emptyset ≺ R_{1} (A) \leftrightarrow R_{1} (A) \neq \emptyset$
53	50 52	sylib	$⊢ (A \in On \land A \neq \emptyset) \to R_{1} (A) \neq \emptyset$
54	53	adantlr	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to R_{1} (A) \neq \emptyset$
55		tskcard	$⊢ (R_{1} (A) \in Tarski \land R_{1} (A) \neq \emptyset) \to card (R_{1} (A)) \in Inacc$
56	2 54 55	syl2anc	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to card (R_{1} (A)) \in Inacc$
57	44 56	eqeltrrd	$⊢ ((A \in On \land R_{1} (A) \in Tarski) \land A \neq \emptyset) \to A \in Inacc$
58	57	ex	$⊢ (A \in On \land R_{1} (A) \in Tarski) \to (A \neq \emptyset \to A \in Inacc)$
59	1 58	syl5bir	$⊢ (A \in On \land R_{1} (A) \in Tarski) \to (\neg A = \emptyset \to A \in Inacc)$
60	59	orrd	$⊢ (A \in On \land R_{1} (A) \in Tarski) \to (A = \emptyset \lor A \in Inacc)$
61	60	ex	$⊢ A \in On \to (R_{1} (A) \in Tarski \to (A = \emptyset \lor A \in Inacc))$
62		fveq2	$⊢ A = \emptyset \to R_{1} (A) = R_{1} (\emptyset)$
63	62 45	eqtrdi	$⊢ A = \emptyset \to R_{1} (A) = \emptyset$
64		0tsk	$⊢ \emptyset \in Tarski$
65	63 64	eqeltrdi	$⊢ A = \emptyset \to R_{1} (A) \in Tarski$
66		inatsk	$⊢ A \in Inacc \to R_{1} (A) \in Tarski$
67	65 66	jaoi	$⊢ (A = \emptyset \lor A \in Inacc) \to R_{1} (A) \in Tarski$
68	61 67	impbid1	$⊢ A \in On \to (R_{1} (A) \in Tarski \leftrightarrow (A = \emptyset \lor A \in Inacc))$

Metamath Proof Explorer

Theorem r1tskina

Proof