inatsk

Description: ( R1A ) for A a strongly inaccessible cardinal is a Tarski class. (Contributed by Mario Carneiro, 8-Jun-2013)

		Ref	Expression
	Assertion	inatsk	$⊢ A \in Inacc \to R_{1} (A) \in Tarski$

Proof

Step	Hyp	Ref	Expression
1		inawina	$⊢ A \in Inacc \to A \in {Inacc}_{𝑤}$
2		winaon	$⊢ A \in {Inacc}_{𝑤} \to A \in On$
3		winalim	$⊢ A \in {Inacc}_{𝑤} \to Lim A$
4		r1lim	$⊢ (A \in On \land Lim A) \to R_{1} (A) = ⋃_{y \in A} R_{1} (y)$
5	2 3 4	syl2anc	$⊢ A \in {Inacc}_{𝑤} \to R_{1} (A) = ⋃_{y \in A} R_{1} (y)$
6	5	eleq2d	$⊢ A \in {Inacc}_{𝑤} \to (x \in R_{1} (A) \leftrightarrow x \in ⋃_{y \in A} R_{1} (y))$
7		eliun	$⊢ x \in ⋃_{y \in A} R_{1} (y) \leftrightarrow \exists y \in A x \in R_{1} (y)$
8	6 7	bitrdi	$⊢ A \in {Inacc}_{𝑤} \to (x \in R_{1} (A) \leftrightarrow \exists y \in A x \in R_{1} (y))$
9		onelon	$⊢ (A \in On \land y \in A) \to y \in On$
10	2 9	sylan	$⊢ (A \in {Inacc}_{𝑤} \land y \in A) \to y \in On$
11		r1pw	$⊢ y \in On \to (x \in R_{1} (y) \leftrightarrow 𝒫 x \in R_{1} (suc y))$
12	10 11	syl	$⊢ (A \in {Inacc}_{𝑤} \land y \in A) \to (x \in R_{1} (y) \leftrightarrow 𝒫 x \in R_{1} (suc y))$
13		limsuc	$⊢ Lim A \to (y \in A \leftrightarrow suc y \in A)$
14	3 13	syl	$⊢ A \in {Inacc}_{𝑤} \to (y \in A \leftrightarrow suc y \in A)$
15		r1ord2	$⊢ A \in On \to (suc y \in A \to R_{1} (suc y) \subseteq R_{1} (A))$
16	2 15	syl	$⊢ A \in {Inacc}_{𝑤} \to (suc y \in A \to R_{1} (suc y) \subseteq R_{1} (A))$
17	14 16	sylbid	$⊢ A \in {Inacc}_{𝑤} \to (y \in A \to R_{1} (suc y) \subseteq R_{1} (A))$
18	17	imp	$⊢ (A \in {Inacc}_{𝑤} \land y \in A) \to R_{1} (suc y) \subseteq R_{1} (A)$
19	18	sseld	$⊢ (A \in {Inacc}_{𝑤} \land y \in A) \to (𝒫 x \in R_{1} (suc y) \to 𝒫 x \in R_{1} (A))$
20	12 19	sylbid	$⊢ (A \in {Inacc}_{𝑤} \land y \in A) \to (x \in R_{1} (y) \to 𝒫 x \in R_{1} (A))$
21	20	rexlimdva	$⊢ A \in {Inacc}_{𝑤} \to (\exists y \in A x \in R_{1} (y) \to 𝒫 x \in R_{1} (A))$
22	8 21	sylbid	$⊢ A \in {Inacc}_{𝑤} \to (x \in R_{1} (A) \to 𝒫 x \in R_{1} (A))$
23	1 22	syl	$⊢ A \in Inacc \to (x \in R_{1} (A) \to 𝒫 x \in R_{1} (A))$
24	23	imp	$⊢ (A \in Inacc \land x \in R_{1} (A)) \to 𝒫 x \in R_{1} (A)$
25		elssuni	$⊢ 𝒫 x \in R_{1} (A) \to 𝒫 x \subseteq ⋃ R_{1} (A)$
26		r1tr2	$⊢ ⋃ R_{1} (A) \subseteq R_{1} (A)$
27	25 26	sstrdi	$⊢ 𝒫 x \in R_{1} (A) \to 𝒫 x \subseteq R_{1} (A)$
28	24 27	jccil	$⊢ (A \in Inacc \land x \in R_{1} (A)) \to (𝒫 x \subseteq R_{1} (A) \land 𝒫 x \in R_{1} (A))$
29	28	ralrimiva	$⊢ A \in Inacc \to \forall x \in R_{1} (A) (𝒫 x \subseteq R_{1} (A) \land 𝒫 x \in R_{1} (A))$
30	1 2	syl	$⊢ A \in Inacc \to A \in On$
31		r1suc	$⊢ A \in On \to R_{1} (suc A) = 𝒫 R_{1} (A)$
32	31	eleq2d	$⊢ A \in On \to (x \in R_{1} (suc A) \leftrightarrow x \in 𝒫 R_{1} (A))$
33	30 32	syl	$⊢ A \in Inacc \to (x \in R_{1} (suc A) \leftrightarrow x \in 𝒫 R_{1} (A))$
34		rankr1ai	$⊢ x \in R_{1} (suc A) \to rank (x) \in suc A$
35	33 34	syl6bir	$⊢ A \in Inacc \to (x \in 𝒫 R_{1} (A) \to rank (x) \in suc A)$
36	35	imp	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to rank (x) \in suc A$
37		fvex	$⊢ rank (x) \in V$
38	37	elsuc	$⊢ rank (x) \in suc A \leftrightarrow (rank (x) \in A \lor rank (x) = A)$
39	36 38	sylib	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to (rank (x) \in A \lor rank (x) = A)$
40	39	orcomd	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to (rank (x) = A \lor rank (x) \in A)$
41		fvex	$⊢ R_{1} (A) \in V$
42		elpwi	$⊢ x \in 𝒫 R_{1} (A) \to x \subseteq R_{1} (A)$
43	42	ad2antlr	$⊢ ((A \in Inacc \land x \in 𝒫 R_{1} (A)) \land rank (x) = A) \to x \subseteq R_{1} (A)$
44		ssdomg	$⊢ R_{1} (A) \in V \to (x \subseteq R_{1} (A) \to x ≼ R_{1} (A))$
45	41 43 44	mpsyl	$⊢ ((A \in Inacc \land x \in 𝒫 R_{1} (A)) \land rank (x) = A) \to x ≼ R_{1} (A)$
46		rankcf	$⊢ \neg x ≺ cf (rank (x))$
47		fveq2	$⊢ rank (x) = A \to cf (rank (x)) = cf (A)$
48		elina	$⊢ A \in Inacc \leftrightarrow (A \neq \emptyset \land cf (A) = A \land \forall x \in A 𝒫 x ≺ A)$
49	48	simp2bi	$⊢ A \in Inacc \to cf (A) = A$
50	47 49	sylan9eqr	$⊢ (A \in Inacc \land rank (x) = A) \to cf (rank (x)) = A$
51	50	breq2d	$⊢ (A \in Inacc \land rank (x) = A) \to (x ≺ cf (rank (x)) \leftrightarrow x ≺ A)$
52	46 51	mtbii	$⊢ (A \in Inacc \land rank (x) = A) \to \neg x ≺ A$
53		inar1	$⊢ A \in Inacc \to R_{1} (A) \approx A$
54		sdomentr	$⊢ (x ≺ R_{1} (A) \land R_{1} (A) \approx A) \to x ≺ A$
55	54	expcom	$⊢ R_{1} (A) \approx A \to (x ≺ R_{1} (A) \to x ≺ A)$
56	53 55	syl	$⊢ A \in Inacc \to (x ≺ R_{1} (A) \to x ≺ A)$
57	56	adantr	$⊢ (A \in Inacc \land rank (x) = A) \to (x ≺ R_{1} (A) \to x ≺ A)$
58	52 57	mtod	$⊢ (A \in Inacc \land rank (x) = A) \to \neg x ≺ R_{1} (A)$
59	58	adantlr	$⊢ ((A \in Inacc \land x \in 𝒫 R_{1} (A)) \land rank (x) = A) \to \neg x ≺ R_{1} (A)$
60		bren2	$⊢ x \approx R_{1} (A) \leftrightarrow (x ≼ R_{1} (A) \land \neg x ≺ R_{1} (A))$
61	45 59 60	sylanbrc	$⊢ ((A \in Inacc \land x \in 𝒫 R_{1} (A)) \land rank (x) = A) \to x \approx R_{1} (A)$
62	61	ex	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to (rank (x) = A \to x \approx R_{1} (A))$
63		r1elwf	$⊢ x \in R_{1} (suc A) \to x \in ⋃ R_{1} [On]$
64	33 63	syl6bir	$⊢ A \in Inacc \to (x \in 𝒫 R_{1} (A) \to x \in ⋃ R_{1} [On])$
65	64	imp	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to x \in ⋃ R_{1} [On]$
66		r1fnon	$⊢ R_{1} Fn On$
67	66	fndmi	$⊢ dom R_{1} = On$
68	30 67	eleqtrrdi	$⊢ A \in Inacc \to A \in dom R_{1}$
69	68	adantr	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to A \in dom R_{1}$
70		rankr1ag	$⊢ (x \in ⋃ R_{1} [On] \land A \in dom R_{1}) \to (x \in R_{1} (A) \leftrightarrow rank (x) \in A)$
71	65 69 70	syl2anc	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to (x \in R_{1} (A) \leftrightarrow rank (x) \in A)$
72	71	biimprd	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to (rank (x) \in A \to x \in R_{1} (A))$
73	62 72	orim12d	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to ((rank (x) = A \lor rank (x) \in A) \to (x \approx R_{1} (A) \lor x \in R_{1} (A)))$
74	40 73	mpd	$⊢ (A \in Inacc \land x \in 𝒫 R_{1} (A)) \to (x \approx R_{1} (A) \lor x \in R_{1} (A))$
75	74	ralrimiva	$⊢ A \in Inacc \to \forall x \in 𝒫 R_{1} (A) (x \approx R_{1} (A) \lor x \in R_{1} (A))$
76		eltsk2g	$⊢ R_{1} (A) \in V \to (R_{1} (A) \in Tarski \leftrightarrow (\forall x \in R_{1} (A) (𝒫 x \subseteq R_{1} (A) \land 𝒫 x \in R_{1} (A)) \land \forall x \in 𝒫 R_{1} (A) (x \approx R_{1} (A) \lor x \in R_{1} (A))))$
77	41 76	ax-mp	$⊢ R_{1} (A) \in Tarski \leftrightarrow (\forall x \in R_{1} (A) (𝒫 x \subseteq R_{1} (A) \land 𝒫 x \in R_{1} (A)) \land \forall x \in 𝒫 R_{1} (A) (x \approx R_{1} (A) \lor x \in R_{1} (A)))$
78	29 75 77	sylanbrc	$⊢ A \in Inacc \to R_{1} (A) \in Tarski$

Metamath Proof Explorer

Theorem inatsk

Proof