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

Theorem axgroth6 10238
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 10234 . 2 𝑦(𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))
2 biid 262 . . . 4 (𝑥𝑦𝑥𝑦)
3 pweq 4538 . . . . . . . . 9 (𝑧 = 𝑣 → 𝒫 𝑧 = 𝒫 𝑣)
43sseq1d 3995 . . . . . . . 8 (𝑧 = 𝑣 → (𝒫 𝑧𝑦 ↔ 𝒫 𝑣𝑦))
54cbvralvw 3447 . . . . . . 7 (∀𝑧𝑦 𝒫 𝑧𝑦 ↔ ∀𝑣𝑦 𝒫 𝑣𝑦)
6 ssid 3986 . . . . . . . . . 10 𝒫 𝑧 ⊆ 𝒫 𝑧
7 sseq2 3990 . . . . . . . . . . 11 (𝑤 = 𝒫 𝑧 → (𝒫 𝑧𝑤 ↔ 𝒫 𝑧 ⊆ 𝒫 𝑧))
87rspcev 3620 . . . . . . . . . 10 ((𝒫 𝑧𝑦 ∧ 𝒫 𝑧 ⊆ 𝒫 𝑧) → ∃𝑤𝑦 𝒫 𝑧𝑤)
96, 8mpan2 687 . . . . . . . . 9 (𝒫 𝑧𝑦 → ∃𝑤𝑦 𝒫 𝑧𝑤)
10 pweq 4538 . . . . . . . . . . . . 13 (𝑣 = 𝑤 → 𝒫 𝑣 = 𝒫 𝑤)
1110sseq1d 3995 . . . . . . . . . . . 12 (𝑣 = 𝑤 → (𝒫 𝑣𝑦 ↔ 𝒫 𝑤𝑦))
1211rspccv 3617 . . . . . . . . . . 11 (∀𝑣𝑦 𝒫 𝑣𝑦 → (𝑤𝑦 → 𝒫 𝑤𝑦))
13 pwss 4555 . . . . . . . . . . . 12 (𝒫 𝑤𝑦 ↔ ∀𝑣(𝑣𝑤𝑣𝑦))
14 vpwex 5269 . . . . . . . . . . . . 13 𝒫 𝑧 ∈ V
15 sseq1 3989 . . . . . . . . . . . . . 14 (𝑣 = 𝒫 𝑧 → (𝑣𝑤 ↔ 𝒫 𝑧𝑤))
16 eleq1 2897 . . . . . . . . . . . . . 14 (𝑣 = 𝒫 𝑧 → (𝑣𝑦 ↔ 𝒫 𝑧𝑦))
1715, 16imbi12d 346 . . . . . . . . . . . . 13 (𝑣 = 𝒫 𝑧 → ((𝑣𝑤𝑣𝑦) ↔ (𝒫 𝑧𝑤 → 𝒫 𝑧𝑦)))
1814, 17spcv 3603 . . . . . . . . . . . 12 (∀𝑣(𝑣𝑤𝑣𝑦) → (𝒫 𝑧𝑤 → 𝒫 𝑧𝑦))
1913, 18sylbi 218 . . . . . . . . . . 11 (𝒫 𝑤𝑦 → (𝒫 𝑧𝑤 → 𝒫 𝑧𝑦))
2012, 19syl6 35 . . . . . . . . . 10 (∀𝑣𝑦 𝒫 𝑣𝑦 → (𝑤𝑦 → (𝒫 𝑧𝑤 → 𝒫 𝑧𝑦)))
2120rexlimdv 3280 . . . . . . . . 9 (∀𝑣𝑦 𝒫 𝑣𝑦 → (∃𝑤𝑦 𝒫 𝑧𝑤 → 𝒫 𝑧𝑦))
229, 21impbid2 227 . . . . . . . 8 (∀𝑣𝑦 𝒫 𝑣𝑦 → (𝒫 𝑧𝑦 ↔ ∃𝑤𝑦 𝒫 𝑧𝑤))
2322ralbidv 3194 . . . . . . 7 (∀𝑣𝑦 𝒫 𝑣𝑦 → (∀𝑧𝑦 𝒫 𝑧𝑦 ↔ ∀𝑧𝑦𝑤𝑦 𝒫 𝑧𝑤))
245, 23sylbi 218 . . . . . 6 (∀𝑧𝑦 𝒫 𝑧𝑦 → (∀𝑧𝑦 𝒫 𝑧𝑦 ↔ ∀𝑧𝑦𝑤𝑦 𝒫 𝑧𝑤))
2524pm5.32i 575 . . . . 5 ((∀𝑧𝑦 𝒫 𝑧𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦) ↔ (∀𝑧𝑦 𝒫 𝑧𝑦 ∧ ∀𝑧𝑦𝑤𝑦 𝒫 𝑧𝑤))
26 r19.26 3167 . . . . 5 (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) ↔ (∀𝑧𝑦 𝒫 𝑧𝑦 ∧ ∀𝑧𝑦 𝒫 𝑧𝑦))
27 r19.26 3167 . . . . 5 (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ↔ (∀𝑧𝑦 𝒫 𝑧𝑦 ∧ ∀𝑧𝑦𝑤𝑦 𝒫 𝑧𝑤))
2825, 26, 273bitr4i 304 . . . 4 (∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) ↔ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤))
29 velpw 4543 . . . . . 6 (𝑧 ∈ 𝒫 𝑦𝑧𝑦)
30 impexp 451 . . . . . . . . 9 (((𝑧𝑦𝑧𝑦) → (¬ 𝑧𝑦𝑧𝑦)) ↔ (𝑧𝑦 → (𝑧𝑦 → (¬ 𝑧𝑦𝑧𝑦))))
31 ssdomg 8543 . . . . . . . . . . . 12 (𝑦 ∈ V → (𝑧𝑦𝑧𝑦))
3231elv 3497 . . . . . . . . . . 11 (𝑧𝑦𝑧𝑦)
3332pm4.71i 560 . . . . . . . . . 10 (𝑧𝑦 ↔ (𝑧𝑦𝑧𝑦))
3433imbi1i 351 . . . . . . . . 9 ((𝑧𝑦 → (¬ 𝑧𝑦𝑧𝑦)) ↔ ((𝑧𝑦𝑧𝑦) → (¬ 𝑧𝑦𝑧𝑦)))
35 brsdom 8520 . . . . . . . . . . . 12 (𝑧𝑦 ↔ (𝑧𝑦 ∧ ¬ 𝑧𝑦))
3635imbi1i 351 . . . . . . . . . . 11 ((𝑧𝑦𝑧𝑦) ↔ ((𝑧𝑦 ∧ ¬ 𝑧𝑦) → 𝑧𝑦))
37 impexp 451 . . . . . . . . . . 11 (((𝑧𝑦 ∧ ¬ 𝑧𝑦) → 𝑧𝑦) ↔ (𝑧𝑦 → (¬ 𝑧𝑦𝑧𝑦)))
3836, 37bitri 276 . . . . . . . . . 10 ((𝑧𝑦𝑧𝑦) ↔ (𝑧𝑦 → (¬ 𝑧𝑦𝑧𝑦)))
3938imbi2i 337 . . . . . . . . 9 ((𝑧𝑦 → (𝑧𝑦𝑧𝑦)) ↔ (𝑧𝑦 → (𝑧𝑦 → (¬ 𝑧𝑦𝑧𝑦))))
4030, 34, 393bitr4ri 305 . . . . . . . 8 ((𝑧𝑦 → (𝑧𝑦𝑧𝑦)) ↔ (𝑧𝑦 → (¬ 𝑧𝑦𝑧𝑦)))
4140pm5.74ri 273 . . . . . . 7 (𝑧𝑦 → ((𝑧𝑦𝑧𝑦) ↔ (¬ 𝑧𝑦𝑧𝑦)))
42 pm4.64 843 . . . . . . 7 ((¬ 𝑧𝑦𝑧𝑦) ↔ (𝑧𝑦𝑧𝑦))
4341, 42syl6bb 288 . . . . . 6 (𝑧𝑦 → ((𝑧𝑦𝑧𝑦) ↔ (𝑧𝑦𝑧𝑦)))
4429, 43sylbi 218 . . . . 5 (𝑧 ∈ 𝒫 𝑦 → ((𝑧𝑦𝑧𝑦) ↔ (𝑧𝑦𝑧𝑦)))
4544ralbiia 3161 . . . 4 (∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦) ↔ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))
462, 28, 453anbi123i 1147 . . 3 ((𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦)) ↔ (𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦)))
4746exbii 1839 . 2 (∃𝑦(𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦)) ↔ ∃𝑦(𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ ∃𝑤𝑦 𝒫 𝑧𝑤) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦)))
481, 47mpbir 232 1 𝑦(𝑥𝑦 ∧ ∀𝑧𝑦 (𝒫 𝑧𝑦 ∧ 𝒫 𝑧𝑦) ∧ ∀𝑧 ∈ 𝒫 𝑦(𝑧𝑦𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841  w3a 1079  wal 1526   = wceq 1528  wex 1771  wcel 2105  wral 3135  wrex 3136  Vcvv 3492  wss 3933  𝒫 cpw 4535   class class class wbr 5057  cen 8494  cdom 8495  csdm 8496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-groth 10233
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-dom 8499  df-sdom 8500
This theorem is referenced by:  grothomex  10239  grothac  10240
  Copyright terms: Public domain W3C validator