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

Theorem infeq5 9435
Description: The statement "there exists a set that is a proper subset of its union" is equivalent to the Axiom of Infinity (shown on the right-hand side in the form of omex 9441.) The left-hand side provides us with a very short way to express the Axiom of Infinity using only elementary symbols. This proof of equivalence does not depend on the Axiom of Infinity. (Contributed by NM, 23-Mar-2004.) (Revised by Mario Carneiro, 16-Nov-2014.)
Assertion
Ref Expression
infeq5 (∃𝑥 𝑥 𝑥 ↔ ω ∈ V)

Proof of Theorem infeq5
Dummy variables 𝑦 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-pss 3911 . . . . 5 (𝑥 𝑥 ↔ (𝑥 𝑥𝑥 𝑥))
2 unieq 4855 . . . . . . . . . 10 (𝑥 = ∅ → 𝑥 = ∅)
3 uni0 4875 . . . . . . . . . 10 ∅ = ∅
42, 3eqtr2di 2793 . . . . . . . . 9 (𝑥 = ∅ → ∅ = 𝑥)
5 eqtr 2759 . . . . . . . . 9 ((𝑥 = ∅ ∧ ∅ = 𝑥) → 𝑥 = 𝑥)
64, 5mpdan 685 . . . . . . . 8 (𝑥 = ∅ → 𝑥 = 𝑥)
76necon3i 2974 . . . . . . 7 (𝑥 𝑥𝑥 ≠ ∅)
87anim1i 616 . . . . . 6 ((𝑥 𝑥𝑥 𝑥) → (𝑥 ≠ ∅ ∧ 𝑥 𝑥))
98ancoms 460 . . . . 5 ((𝑥 𝑥𝑥 𝑥) → (𝑥 ≠ ∅ ∧ 𝑥 𝑥))
101, 9sylbi 216 . . . 4 (𝑥 𝑥 → (𝑥 ≠ ∅ ∧ 𝑥 𝑥))
1110eximi 1835 . . 3 (∃𝑥 𝑥 𝑥 → ∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 𝑥))
12 eqid 2736 . . . . 5 (𝑦 ∈ V ↦ {𝑤𝑥 ∣ (𝑤𝑥) ⊆ 𝑦}) = (𝑦 ∈ V ↦ {𝑤𝑥 ∣ (𝑤𝑥) ⊆ 𝑦})
13 eqid 2736 . . . . 5 (rec((𝑦 ∈ V ↦ {𝑤𝑥 ∣ (𝑤𝑥) ⊆ 𝑦}), ∅) ↾ ω) = (rec((𝑦 ∈ V ↦ {𝑤𝑥 ∣ (𝑤𝑥) ⊆ 𝑦}), ∅) ↾ ω)
14 vex 3441 . . . . 5 𝑥 ∈ V
1512, 13, 14, 14inf3lem7 9432 . . . 4 ((𝑥 ≠ ∅ ∧ 𝑥 𝑥) → ω ∈ V)
1615exlimiv 1931 . . 3 (∃𝑥(𝑥 ≠ ∅ ∧ 𝑥 𝑥) → ω ∈ V)
1711, 16syl 17 . 2 (∃𝑥 𝑥 𝑥 → ω ∈ V)
18 infeq5i 9434 . 2 (ω ∈ V → ∃𝑥 𝑥 𝑥)
1917, 18impbii 208 1 (∃𝑥 𝑥 𝑥 ↔ ω ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1539  wex 1779  wcel 2104  wne 2941  {crab 3284  Vcvv 3437  cin 3891  wss 3892  wpss 3893  c0 4262   cuni 4844  cmpt 5164  cres 5598  ωcom 7740  reccrdg 8267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5218  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7616  ax-reg 9391
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-iun 4933  df-br 5082  df-opab 5144  df-mpt 5165  df-tr 5199  df-id 5496  df-eprel 5502  df-po 5510  df-so 5511  df-fr 5551  df-we 5553  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-pred 6213  df-ord 6280  df-on 6281  df-lim 6282  df-suc 6283  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-ov 7306  df-om 7741  df-2nd 7860  df-frecs 8124  df-wrecs 8155  df-recs 8229  df-rdg 8268
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator