Theorem inaprc 9212

Description: An equivalent to the Tarski-Grothendieck Axiom: there is a proper class of inaccessible cardinals. (Contributed by Mario Carneiro, 9-Jun-2013.)

Assertion

Ref	Expression
inaprc	|- Inacc e/ _V

Proof of Theorem inaprc

Dummy variables x w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inawina 9066	. . . . . 6 |- ( x e. Inacc -> x e. InaccW )
2		winaon 9064	. . . . . 6 |- ( x e. InaccW -> x e. On )
3	1, 2	syl 16	. . . . 5 |- ( x e. Inacc -> x e. On )
4	3	ssriv 3490	. . . 4 |- Inacc C_ On
5		ssorduni 6602	. . . 4 |- ( Inacc C_ On -> Ord U. Inacc )
6		ordsson 6606	. . . 4 |- ( Ord U. Inacc -> U. Inacc C_ On )
7	4, 5, 6	mp2b 10	. . 3 |- U. Inacc C_ On
8		vex 3096	. . . . . . . 8 |- y e. _V
9		grothtsk 9211	. . . . . . . 8 |- U. Tarski = _V
10	8, 9	eleqtrri 2528	. . . . . . 7 |- y e. U. Tarski
11		eluni2 4234	. . . . . . 7 |- ( y e. U. Tarski <-> E. w e. Tarski y e. w )
12	10, 11	mpbi 208	. . . . . 6 |- E. w e. Tarski y e. w
13		ne0i 3773	. . . . . . . . . 10 |- ( y e. w -> w =/= (/) )
14		tskcard 9157	. . . . . . . . . 10 |- ( ( w e. Tarski /\ w =/= (/) ) -> ( card ` w ) e. Inacc )
15	13, 14	sylan2 474	. . . . . . . . 9 |- ( ( w e. Tarski /\ y e. w ) -> ( card ` w ) e. Inacc )
16	15	adantl 466	. . . . . . . 8 |- ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> ( card ` w ) e. Inacc )
17		tsksdom 9132	. . . . . . . . . 10 |- ( ( w e. Tarski /\ y e. w ) -> y ~< w )
18	17	adantl 466	. . . . . . . . 9 |- ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> y ~< w )
19		tskwe2 9149	. . . . . . . . . . 11 |- ( w e. Tarski -> w e. dom card )
20	19	adantr 465	. . . . . . . . . 10 |- ( ( w e. Tarski /\ y e. w ) -> w e. dom card )
21		cardsdomel 8353	. . . . . . . . . 10 |- ( ( y e. On /\ w e. dom card ) -> ( y ~< w <-> y e. ( card ` w ) ) )
22	20, 21	sylan2 474	. . . . . . . . 9 |- ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> ( y ~< w <-> y e. ( card ` w ) ) )
23	18, 22	mpbid 210	. . . . . . . 8 |- ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> y e. ( card ` w ) )
24		eleq2 2514	. . . . . . . . 9 |- ( z = ( card ` w ) -> ( y e. z <-> y e. ( card ` w ) ) )
25	24	rspcev 3194	. . . . . . . 8 |- ( ( ( card ` w ) e. Inacc /\ y e. ( card ` w ) ) -> E. z e. Inacc y e. z )
26	16, 23, 25	syl2anc 661	. . . . . . 7 |- ( ( y e. On /\ ( w e. Tarski /\ y e. w ) ) -> E. z e. Inacc y e. z )
27	26	rexlimdvaa 2934	. . . . . 6 |- ( y e. On -> ( E. w e. Tarski y e. w -> E. z e. Inacc y e. z ) )
28	12, 27	mpi 17	. . . . 5 |- ( y e. On -> E. z e. Inacc y e. z )
29		eluni2 4234	. . . . 5 |- ( y e. U. Inacc <-> E. z e. Inacc y e. z )
30	28, 29	sylibr 212	. . . 4 |- ( y e. On -> y e. U. Inacc )
31	30	ssriv 3490	. . 3 |- On C_ U. Inacc
32	7, 31	eqssi 3502	. 2 |- U. Inacc = On
33		ssonprc 6608	. . 3 |- ( Inacc C_ On -> ( Inacc e/ _V <-> U. Inacc = On ) )
34	4, 33	ax-mp 5	. 2 |- ( Inacc e/ _V <-> U. Inacc = On )
35	32, 34	mpbir 209	1 |- Inacc e/ _V

Syntax hints:   <-> wb 184   /\ wa 369   = wceq 1381   e. wcel 1802   =/= wne 2636   e/ wnel 2637   E.wrex 2792   _Vcvv 3093   C_ wss 3458   (/)c0 3767   U.cuni 4230   class class class wbr 4433   Ord word 4863   Oncon0 4864   dom cdm 4985   ` cfv 5574   ~< csdm 7513   cardccrd 8314   InaccWcwina 9058   Inacccina 9059   Tarskictsk 9124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-inf2 8056  ax-ac2 8841  ax-groth 9199

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-iin 4314  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-se 4825  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-isom 5583  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-1st 6781  df-2nd 6782  df-smo 7015  df-recs 7040  df-rdg 7074  df-1o 7128  df-2o 7129  df-oadd 7132  df-er 7309  df-map 7420  df-ixp 7468  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-oi 7933  df-har 7982  df-r1 8180  df-card 8318  df-aleph 8319  df-cf 8320  df-acn 8321  df-ac 8495  df-wina 9060  df-ina 9061  df-tsk 9125

This theorem is referenced by: (None)