Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax6e2ndVD Structured version   Visualization version   GIF version

Theorem ax6e2ndVD 38627
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 38267) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2nd 38256 is ax6e2ndVD 38627 without virtual deductions and was automatically derived from ax6e2ndVD 38627. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
1:: 𝑦𝑦 = 𝑣
2:: 𝑢 ∈ V
3:1,2: (𝑢 ∈ V ∧ ∃𝑦𝑦 = 𝑣)
4:3: 𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)
5:: (𝑢 ∈ V ↔ ∃𝑥𝑥 = 𝑢)
6:5: ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥𝑥 = 𝑢𝑦 = 𝑣))
7:6: (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦 (∃𝑥𝑥 = 𝑢𝑦 = 𝑣))
8:4,7: 𝑦(∃𝑥𝑥 = 𝑢𝑦 = 𝑣)
9:: (𝑧 = 𝑣 → ∀𝑥𝑧 = 𝑣)
10:: (𝑦 = 𝑣 → ∀𝑧𝑦 = 𝑣)
11:: (   𝑧 = 𝑦   ▶   𝑧 = 𝑦   )
12:11: (   𝑧 = 𝑦   ▶   (𝑧 = 𝑣𝑦 = 𝑣)   )
120:11: (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
13:9,10,120: (¬ ∀𝑥𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥𝑦 = 𝑣))
14:: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   ¬ ∀𝑥𝑥 = 𝑦   )
15:14,13: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)   )
16:15: (¬ ∀𝑥𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥𝑦 = 𝑣))
17:16: (∀𝑥¬ ∀𝑥𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥𝑦 = 𝑣))
18:: (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑥¬ ∀𝑥𝑥 = 𝑦 )
19:17,18: (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀ 𝑥𝑦 = 𝑣))
20:14,19: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   𝑥(𝑦 = 𝑣 𝑥𝑦 = 𝑣)   )
21:20: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   ((∃𝑥𝑥 = 𝑢 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣))   )
22:21: (¬ ∀𝑥𝑥 = 𝑦 → ((∃𝑥𝑥 = 𝑢 𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
23:22: (∀𝑦¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
24:: (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦¬ ∀𝑥𝑥 = 𝑦 )
25:23,24: (¬ ∀𝑥𝑥 = 𝑦 → ∀𝑦((∃𝑥𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
26:14,25: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   𝑦((∃𝑥𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣))   )
27:26: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   (∃𝑦(∃𝑥𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))   )
28:8,27: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)   )
29:28: (   ¬ ∀𝑥𝑥 = 𝑦   ▶   𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣)   )
qed:29: (¬ ∀𝑥𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢 𝑦 = 𝑣))
Assertion
Ref Expression
ax6e2ndVD (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
Distinct variable groups:   𝑥,𝑢   𝑦,𝑢   𝑥,𝑣

Proof of Theorem ax6e2ndVD
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 vex 3189 . . . . . . 7 𝑢 ∈ V
2 ax6e 2249 . . . . . . 7 𝑦 𝑦 = 𝑣
31, 2pm3.2i 471 . . . . . 6 (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣)
4 19.42v 1915 . . . . . . 7 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣))
54biimpri 218 . . . . . 6 ((𝑢 ∈ V ∧ ∃𝑦 𝑦 = 𝑣) → ∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣))
63, 5e0a 38481 . . . . 5 𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣)
7 isset 3193 . . . . . . 7 (𝑢 ∈ V ↔ ∃𝑥 𝑥 = 𝑢)
87anbi1i 730 . . . . . 6 ((𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ (∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
98exbii 1771 . . . . 5 (∃𝑦(𝑢 ∈ V ∧ 𝑦 = 𝑣) ↔ ∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣))
106, 9mpbi 220 . . . 4 𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣)
11 idn1 38272 . . . . . 6 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶    ¬ ∀𝑥 𝑥 = 𝑦   )
12 hbnae 2316 . . . . . . 7 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦)
13 hbn1 2017 . . . . . . . . . . . 12 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
14 ax-5 1836 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑣 → ∀𝑥 𝑧 = 𝑣)
15 ax-5 1836 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑣 → ∀𝑧 𝑦 = 𝑣)
16 idn1 38272 . . . . . . . . . . . . . . . . . 18 (   𝑧 = 𝑦   ▶   𝑧 = 𝑦   )
17 equequ1 1949 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
1816, 17e1a 38334 . . . . . . . . . . . . . . . . 17 (   𝑧 = 𝑦   ▶   (𝑧 = 𝑣𝑦 = 𝑣)   )
1918in1 38269 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑦 → (𝑧 = 𝑣𝑦 = 𝑣))
2014, 15, 19dvelimh 2335 . . . . . . . . . . . . . . 15 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2111, 20e1a 38334 . . . . . . . . . . . . . 14 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)   )
2221in1 38269 . . . . . . . . . . . . 13 (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2322alimi 1736 . . . . . . . . . . . 12 (∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2413, 23syl 17 . . . . . . . . . . 11 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣))
2511, 24e1a 38334 . . . . . . . . . 10 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣)   )
26 19.41rg 38248 . . . . . . . . . 10 (∀𝑥(𝑦 = 𝑣 → ∀𝑥 𝑦 = 𝑣) → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2725, 26e1a 38334 . . . . . . . . 9 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣))   )
2827in1 38269 . . . . . . . 8 (¬ ∀𝑥 𝑥 = 𝑦 → ((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
2928alimi 1736 . . . . . . 7 (∀𝑦 ¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3012, 29syl 17 . . . . . 6 (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3111, 30e1a 38334 . . . . 5 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣))   )
32 exim 1758 . . . . 5 (∀𝑦((∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3331, 32e1a 38334 . . . 4 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣))   )
34 pm2.27 42 . . . 4 (∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ((∃𝑦(∃𝑥 𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)) → ∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)))
3510, 33, 34e01 38398 . . 3 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣)   )
36 excomim 2040 . . 3 (∃𝑦𝑥(𝑥 = 𝑢𝑦 = 𝑣) → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
3735, 36e1a 38334 . 2 (    ¬ ∀𝑥 𝑥 = 𝑦   ▶   𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣)   )
3837in1 38269 1 (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥𝑦(𝑥 = 𝑢𝑦 = 𝑣))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384  wal 1478   = wceq 1480  wex 1701  wcel 1987  Vcvv 3186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-v 3188  df-vd1 38268
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator