Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  axgroth6 Structured version   Visualization version   Unicode version

Theorem axgroth6 9271
 Description: The Tarski-Grothendieck axiom using abbreviations. This version is called Tarski's axiom: given a set , there exists a set containing , the subsets of the members of , the power sets of the members of , and the subsets of of cardinality less than that of . (Contributed by NM, 21-Jun-2009.)
Assertion
Ref Expression
axgroth6
Distinct variable group:   ,,

Proof of Theorem axgroth6
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 axgroth5 9267 . 2
2 biid 244 . . . 4
3 pweq 3945 . . . . . . . . 9
43sseq1d 3445 . . . . . . . 8
54cbvralv 3005 . . . . . . 7
6 ssid 3437 . . . . . . . . . 10
7 sseq2 3440 . . . . . . . . . . 11
87rspcev 3136 . . . . . . . . . 10
96, 8mpan2 685 . . . . . . . . 9
10 pweq 3945 . . . . . . . . . . . . 13
1110sseq1d 3445 . . . . . . . . . . . 12
1211rspccv 3133 . . . . . . . . . . 11
13 pwss 3957 . . . . . . . . . . . 12
14 vex 3034 . . . . . . . . . . . . . 14
1514pwex 4584 . . . . . . . . . . . . 13
16 sseq1 3439 . . . . . . . . . . . . . 14
17 eleq1 2537 . . . . . . . . . . . . . 14
1816, 17imbi12d 327 . . . . . . . . . . . . 13
1915, 18spcv 3126 . . . . . . . . . . . 12
2013, 19sylbi 200 . . . . . . . . . . 11
2112, 20syl6 33 . . . . . . . . . 10
2221rexlimdv 2870 . . . . . . . . 9
239, 22impbid2 209 . . . . . . . 8
2423ralbidv 2829 . . . . . . 7
255, 24sylbi 200 . . . . . 6
2625pm5.32i 649 . . . . 5
27 r19.26 2904 . . . . 5
28 r19.26 2904 . . . . 5
2926, 27, 283bitr4i 285 . . . 4
30 selpw 3949 . . . . . 6
31 impexp 453 . . . . . . . . 9
32 vex 3034 . . . . . . . . . . . 12
33 ssdomg 7633 . . . . . . . . . . . 12
3432, 33ax-mp 5 . . . . . . . . . . 11
3534pm4.71i 644 . . . . . . . . . 10
3635imbi1i 332 . . . . . . . . 9
37 brsdom 7610 . . . . . . . . . . . 12
3837imbi1i 332 . . . . . . . . . . 11
39 impexp 453 . . . . . . . . . . 11
4038, 39bitri 257 . . . . . . . . . 10
4140imbi2i 319 . . . . . . . . 9
4231, 36, 413bitr4ri 286 . . . . . . . 8
4342pm5.74ri 254 . . . . . . 7
44 pm4.64 379 . . . . . . 7
4543, 44syl6bb 269 . . . . . 6
4630, 45sylbi 200 . . . . 5
4746ralbiia 2822 . . . 4
482, 29, 473anbi123i 1219 . . 3
4948exbii 1726 . 2
501, 49mpbir 214 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 189   wo 375   wa 376   w3a 1007  wal 1450   wceq 1452  wex 1671   wcel 1904  wral 2756  wrex 2757  cvv 3031   wss 3390  cpw 3942   class class class wbr 4395   cen 7584   cdom 7585   csdm 7586 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-groth 9266 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-dom 7589  df-sdom 7590 This theorem is referenced by:  grothomex  9272  grothac  9273
 Copyright terms: Public domain W3C validator