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

Theorem suctrALTcfVD 42567
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 42213) using conjunction-form virtual hypothesis collections. The conjunction-form version of completeusersproof.cmd. It allows the User to avoid superflous virtual hypotheses. This proof was completed automatically by a tools program which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. suctrALTcf 42566 is suctrALTcfVD 42567 without virtual deductions and was derived automatically from suctrALTcfVD 42567. The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
1:: (   Tr 𝐴   ▶   Tr 𝐴   )
2:: (   ......... (𝑧𝑦𝑦 suc 𝐴)   ▶   (𝑧𝑦𝑦 ∈ suc 𝐴)   )
3:2: (   ......... (𝑧𝑦𝑦 suc 𝐴)   ▶   𝑧𝑦   )
4:: (   ................................... ....... 𝑦𝐴   ▶   𝑦𝐴   )
5:1,3,4: (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴) , 𝑦𝐴   )   ▶   𝑧𝐴   )
6:: 𝐴 ⊆ suc 𝐴
7:5,6: (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴) , 𝑦𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
8:7: (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)    )   ▶   (𝑦𝐴𝑧 ∈ suc 𝐴)   )
9:: (   ................................... ...... 𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
10:3,9: (   ........ (   (𝑧𝑦𝑦 suc 𝐴), 𝑦 = 𝐴   )   ▶   𝑧𝐴   )
11:10,6: (   ........ (   (𝑧𝑦𝑦 suc 𝐴), 𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
12:11: (   .......... (𝑧𝑦𝑦 suc 𝐴)   ▶   (𝑦 = 𝐴𝑧 ∈ suc 𝐴)   )
13:2: (   .......... (𝑧𝑦𝑦 suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
14:13: (   .......... (𝑧𝑦𝑦 suc 𝐴)   ▶   (𝑦𝐴𝑦 = 𝐴)   )
15:8,12,14: (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)    )   ▶   𝑧 ∈ suc 𝐴   )
16:15: (   Tr 𝐴   ▶   ((𝑧𝑦𝑦 suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
17:16: (   Tr 𝐴   ▶   𝑧𝑦((𝑧 𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
18:17: (   Tr 𝐴   ▶   Tr suc 𝐴   )
qed:18: (Tr 𝐴 → Tr suc 𝐴)
Assertion
Ref Expression
suctrALTcfVD (Tr 𝐴 → Tr suc 𝐴)

Proof of Theorem suctrALTcfVD
Dummy variables 𝑧 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sssucid 6349 . . . . . . . 8 𝐴 ⊆ suc 𝐴
2 idn1 42218 . . . . . . . . 9 (   Tr 𝐴   ▶   Tr 𝐴   )
3 idn1 42218 . . . . . . . . . 10 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑧𝑦𝑦 ∈ suc 𝐴)   )
4 simpl 482 . . . . . . . . . 10 ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧𝑦)
53, 4el1 42272 . . . . . . . . 9 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑧𝑦   )
6 idn1 42218 . . . . . . . . 9 (   𝑦𝐴   ▶   𝑦𝐴   )
7 trel 5201 . . . . . . . . . 10 (Tr 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
873impib 1114 . . . . . . . . 9 ((Tr 𝐴𝑧𝑦𝑦𝐴) → 𝑧𝐴)
92, 5, 6, 8el123 42408 . . . . . . . 8 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧𝐴   )
10 ssel2 3918 . . . . . . . 8 ((𝐴 ⊆ suc 𝐴𝑧𝐴) → 𝑧 ∈ suc 𝐴)
111, 9, 10el0321old 42361 . . . . . . 7 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1211int3 42256 . . . . . 6 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   (𝑦𝐴𝑧 ∈ suc 𝐴)   )
13 idn1 42218 . . . . . . . . 9 (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
14 eleq2 2822 . . . . . . . . . 10 (𝑦 = 𝐴 → (𝑧𝑦𝑧𝐴))
1514biimpac 478 . . . . . . . . 9 ((𝑧𝑦𝑦 = 𝐴) → 𝑧𝐴)
165, 13, 15el12 42370 . . . . . . . 8 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧𝐴   )
171, 16, 10el021old 42345 . . . . . . 7 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1817int2 42250 . . . . . 6 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴𝑧 ∈ suc 𝐴)   )
19 simpr 484 . . . . . . . 8 ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
203, 19el1 42272 . . . . . . 7 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
21 elsuci 6336 . . . . . . 7 (𝑦 ∈ suc 𝐴 → (𝑦𝐴𝑦 = 𝐴))
2220, 21el1 42272 . . . . . 6 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦𝐴𝑦 = 𝐴)   )
23 jao 957 . . . . . . 7 ((𝑦𝐴𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴𝑧 ∈ suc 𝐴) → ((𝑦𝐴𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)))
24233imp 1109 . . . . . 6 (((𝑦𝐴𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴𝑧 ∈ suc 𝐴) ∧ (𝑦𝐴𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴)
2512, 18, 22, 24el2122old 42363 . . . . 5 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   )
2625int2 42250 . . . 4 (   Tr 𝐴   ▶   ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
2726gen12 42262 . . 3 (   Tr 𝐴   ▶   𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
28 dftr2 5196 . . . 4 (Tr suc 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
2928biimpri 227 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
3027, 29el1 42272 . 2 (   Tr 𝐴   ▶   Tr suc 𝐴   )
3130in1 42215 1 (Tr 𝐴 → Tr suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 843  wal 1535   = wceq 1537  wcel 2101  wss 3889  Tr wtr 5194  suc csuc 6272
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-un 3894  df-in 3896  df-ss 3906  df-sn 4565  df-uni 4842  df-tr 5195  df-suc 6276  df-vd1 42214  df-vhc2 42225  df-vhc3 42233
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator