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 e. Inacc -> ( R1 ` A ) e. Tarski )

Proof

Step	Hyp	Ref	Expression
1		inawina	\|- ( A e. Inacc -> A e. InaccW )
2		winaon	\|- ( A e. InaccW -> A e. On )
3		winalim	\|- ( A e. InaccW -> Lim A )
4		r1lim	\|- ( ( A e. On /\ Lim A ) -> ( R1 ` A ) = U_ y e. A ( R1 ` y ) )
5	2 3 4	syl2anc	\|- ( A e. InaccW -> ( R1 ` A ) = U_ y e. A ( R1 ` y ) )
6	5	eleq2d	\|- ( A e. InaccW -> ( x e. ( R1 ` A ) <-> x e. U_ y e. A ( R1 ` y ) ) )
7		eliun	\|- ( x e. U_ y e. A ( R1 ` y ) <-> E. y e. A x e. ( R1 ` y ) )
8	6 7	bitrdi	\|- ( A e. InaccW -> ( x e. ( R1 ` A ) <-> E. y e. A x e. ( R1 ` y ) ) )
9		onelon	\|- ( ( A e. On /\ y e. A ) -> y e. On )
10	2 9	sylan	\|- ( ( A e. InaccW /\ y e. A ) -> y e. On )
11		r1pw	\|- ( y e. On -> ( x e. ( R1 ` y ) <-> ~P x e. ( R1 ` suc y ) ) )
12	10 11	syl	\|- ( ( A e. InaccW /\ y e. A ) -> ( x e. ( R1 ` y ) <-> ~P x e. ( R1 ` suc y ) ) )
13		limsuc	\|- ( Lim A -> ( y e. A <-> suc y e. A ) )
14	3 13	syl	\|- ( A e. InaccW -> ( y e. A <-> suc y e. A ) )
15		r1ord2	\|- ( A e. On -> ( suc y e. A -> ( R1 ` suc y ) C_ ( R1 ` A ) ) )
16	2 15	syl	\|- ( A e. InaccW -> ( suc y e. A -> ( R1 ` suc y ) C_ ( R1 ` A ) ) )
17	14 16	sylbid	\|- ( A e. InaccW -> ( y e. A -> ( R1 ` suc y ) C_ ( R1 ` A ) ) )
18	17	imp	\|- ( ( A e. InaccW /\ y e. A ) -> ( R1 ` suc y ) C_ ( R1 ` A ) )
19	18	sseld	\|- ( ( A e. InaccW /\ y e. A ) -> ( ~P x e. ( R1 ` suc y ) -> ~P x e. ( R1 ` A ) ) )
20	12 19	sylbid	\|- ( ( A e. InaccW /\ y e. A ) -> ( x e. ( R1 ` y ) -> ~P x e. ( R1 ` A ) ) )
21	20	rexlimdva	\|- ( A e. InaccW -> ( E. y e. A x e. ( R1 ` y ) -> ~P x e. ( R1 ` A ) ) )
22	8 21	sylbid	\|- ( A e. InaccW -> ( x e. ( R1 ` A ) -> ~P x e. ( R1 ` A ) ) )
23	1 22	syl	\|- ( A e. Inacc -> ( x e. ( R1 ` A ) -> ~P x e. ( R1 ` A ) ) )
24	23	imp	\|- ( ( A e. Inacc /\ x e. ( R1 ` A ) ) -> ~P x e. ( R1 ` A ) )
25		elssuni	\|- ( ~P x e. ( R1 ` A ) -> ~P x C_ U. ( R1 ` A ) )
26		r1tr2	\|- U. ( R1 ` A ) C_ ( R1 ` A )
27	25 26	sstrdi	\|- ( ~P x e. ( R1 ` A ) -> ~P x C_ ( R1 ` A ) )
28	24 27	jccil	\|- ( ( A e. Inacc /\ x e. ( R1 ` A ) ) -> ( ~P x C_ ( R1 ` A ) /\ ~P x e. ( R1 ` A ) ) )
29	28	ralrimiva	\|- ( A e. Inacc -> A. x e. ( R1 ` A ) ( ~P x C_ ( R1 ` A ) /\ ~P x e. ( R1 ` A ) ) )
30	1 2	syl	\|- ( A e. Inacc -> A e. On )
31		r1suc	\|- ( A e. On -> ( R1 ` suc A ) = ~P ( R1 ` A ) )
32	31	eleq2d	\|- ( A e. On -> ( x e. ( R1 ` suc A ) <-> x e. ~P ( R1 ` A ) ) )
33	30 32	syl	\|- ( A e. Inacc -> ( x e. ( R1 ` suc A ) <-> x e. ~P ( R1 ` A ) ) )
34		rankr1ai	\|- ( x e. ( R1 ` suc A ) -> ( rank ` x ) e. suc A )
35	33 34	biimtrrdi	\|- ( A e. Inacc -> ( x e. ~P ( R1 ` A ) -> ( rank ` x ) e. suc A ) )
36	35	imp	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( rank ` x ) e. suc A )
37		fvex	\|- ( rank ` x ) e. _V
38	37	elsuc	\|- ( ( rank ` x ) e. suc A <-> ( ( rank ` x ) e. A \/ ( rank ` x ) = A ) )
39	36 38	sylib	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( rank ` x ) e. A \/ ( rank ` x ) = A ) )
40	39	orcomd	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( rank ` x ) = A \/ ( rank ` x ) e. A ) )
41		fvex	\|- ( R1 ` A ) e. _V
42		elpwi	\|- ( x e. ~P ( R1 ` A ) -> x C_ ( R1 ` A ) )
43	42	ad2antlr	\|- ( ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) /\ ( rank ` x ) = A ) -> x C_ ( R1 ` A ) )
44		ssdomg	\|- ( ( R1 ` A ) e. _V -> ( x C_ ( R1 ` A ) -> x ~<_ ( R1 ` A ) ) )
45	41 43 44	mpsyl	\|- ( ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) /\ ( rank ` x ) = A ) -> x ~<_ ( R1 ` A ) )
46		rankcf	\|- -. x ~< ( cf ` ( rank ` x ) )
47		fveq2	\|- ( ( rank ` x ) = A -> ( cf ` ( rank ` x ) ) = ( cf ` A ) )
48		elina	\|- ( A e. Inacc <-> ( A =/= (/) /\ ( cf ` A ) = A /\ A. x e. A ~P x ~< A ) )
49	48	simp2bi	\|- ( A e. Inacc -> ( cf ` A ) = A )
50	47 49	sylan9eqr	\|- ( ( A e. Inacc /\ ( rank ` x ) = A ) -> ( cf ` ( rank ` x ) ) = A )
51	50	breq2d	\|- ( ( A e. Inacc /\ ( rank ` x ) = A ) -> ( x ~< ( cf ` ( rank ` x ) ) <-> x ~< A ) )
52	46 51	mtbii	\|- ( ( A e. Inacc /\ ( rank ` x ) = A ) -> -. x ~< A )
53		inar1	\|- ( A e. Inacc -> ( R1 ` A ) ~~ A )
54		sdomentr	\|- ( ( x ~< ( R1 ` A ) /\ ( R1 ` A ) ~~ A ) -> x ~< A )
55	54	expcom	\|- ( ( R1 ` A ) ~~ A -> ( x ~< ( R1 ` A ) -> x ~< A ) )
56	53 55	syl	\|- ( A e. Inacc -> ( x ~< ( R1 ` A ) -> x ~< A ) )
57	56	adantr	\|- ( ( A e. Inacc /\ ( rank ` x ) = A ) -> ( x ~< ( R1 ` A ) -> x ~< A ) )
58	52 57	mtod	\|- ( ( A e. Inacc /\ ( rank ` x ) = A ) -> -. x ~< ( R1 ` A ) )
59	58	adantlr	\|- ( ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) /\ ( rank ` x ) = A ) -> -. x ~< ( R1 ` A ) )
60		bren2	\|- ( x ~~ ( R1 ` A ) <-> ( x ~<_ ( R1 ` A ) /\ -. x ~< ( R1 ` A ) ) )
61	45 59 60	sylanbrc	\|- ( ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) /\ ( rank ` x ) = A ) -> x ~~ ( R1 ` A ) )
62	61	ex	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( rank ` x ) = A -> x ~~ ( R1 ` A ) ) )
63		r1elwf	\|- ( x e. ( R1 ` suc A ) -> x e. U. ( R1 " On ) )
64	33 63	biimtrrdi	\|- ( A e. Inacc -> ( x e. ~P ( R1 ` A ) -> x e. U. ( R1 " On ) ) )
65	64	imp	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> x e. U. ( R1 " On ) )
66		r1fnon	\|- R1 Fn On
67	66	fndmi	\|- dom R1 = On
68	30 67	eleqtrrdi	\|- ( A e. Inacc -> A e. dom R1 )
69	68	adantr	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> A e. dom R1 )
70		rankr1ag	\|- ( ( x e. U. ( R1 " On ) /\ A e. dom R1 ) -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
71	65 69 70	syl2anc	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( x e. ( R1 ` A ) <-> ( rank ` x ) e. A ) )
72	71	biimprd	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( rank ` x ) e. A -> x e. ( R1 ` A ) ) )
73	62 72	orim12d	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( ( ( rank ` x ) = A \/ ( rank ` x ) e. A ) -> ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) ) )
74	40 73	mpd	\|- ( ( A e. Inacc /\ x e. ~P ( R1 ` A ) ) -> ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) )
75	74	ralrimiva	\|- ( A e. Inacc -> A. x e. ~P ( R1 ` A ) ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) )
76		eltsk2g	\|- ( ( R1 ` A ) e. _V -> ( ( R1 ` A ) e. Tarski <-> ( A. x e. ( R1 ` A ) ( ~P x C_ ( R1 ` A ) /\ ~P x e. ( R1 ` A ) ) /\ A. x e. ~P ( R1 ` A ) ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) ) ) )
77	41 76	ax-mp	\|- ( ( R1 ` A ) e. Tarski <-> ( A. x e. ( R1 ` A ) ( ~P x C_ ( R1 ` A ) /\ ~P x e. ( R1 ` A ) ) /\ A. x e. ~P ( R1 ` A ) ( x ~~ ( R1 ` A ) \/ x e. ( R1 ` A ) ) ) )
78	29 75 77	sylanbrc	\|- ( A e. Inacc -> ( R1 ` A ) e. Tarski )

Metamath Proof Explorer

Theorem inatsk

Proof