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 43684
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 43330) 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 43683 is suctrALTcfVD 43684 without virtual deductions and was derived automatically from suctrALTcfVD 43684. 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 6445 . . . . . . . 8 𝐴 ⊆ suc 𝐴
2 idn1 43335 . . . . . . . . 9 (   Tr 𝐴   ▶   Tr 𝐴   )
3 idn1 43335 . . . . . . . . . 10 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑧𝑦𝑦 ∈ suc 𝐴)   )
4 simpl 484 . . . . . . . . . 10 ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧𝑦)
53, 4el1 43389 . . . . . . . . 9 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑧𝑦   )
6 idn1 43335 . . . . . . . . 9 (   𝑦𝐴   ▶   𝑦𝐴   )
7 trel 5275 . . . . . . . . . 10 (Tr 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
873impib 1117 . . . . . . . . 9 ((Tr 𝐴𝑧𝑦𝑦𝐴) → 𝑧𝐴)
92, 5, 6, 8el123 43525 . . . . . . . 8 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧𝐴   )
10 ssel2 3978 . . . . . . . 8 ((𝐴 ⊆ suc 𝐴𝑧𝐴) → 𝑧 ∈ suc 𝐴)
111, 9, 10el0321old 43478 . . . . . . 7 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1211int3 43373 . . . . . 6 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   (𝑦𝐴𝑧 ∈ suc 𝐴)   )
13 idn1 43335 . . . . . . . . 9 (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
14 eleq2 2823 . . . . . . . . . 10 (𝑦 = 𝐴 → (𝑧𝑦𝑧𝐴))
1514biimpac 480 . . . . . . . . 9 ((𝑧𝑦𝑦 = 𝐴) → 𝑧𝐴)
165, 13, 15el12 43487 . . . . . . . 8 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧𝐴   )
171, 16, 10el021old 43462 . . . . . . 7 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1817int2 43367 . . . . . 6 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴𝑧 ∈ suc 𝐴)   )
19 simpr 486 . . . . . . . 8 ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
203, 19el1 43389 . . . . . . 7 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
21 elsuci 6432 . . . . . . 7 (𝑦 ∈ suc 𝐴 → (𝑦𝐴𝑦 = 𝐴))
2220, 21el1 43389 . . . . . 6 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦𝐴𝑦 = 𝐴)   )
23 jao 960 . . . . . . 7 ((𝑦𝐴𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴𝑧 ∈ suc 𝐴) → ((𝑦𝐴𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)))
24233imp 1112 . . . . . 6 (((𝑦𝐴𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴𝑧 ∈ suc 𝐴) ∧ (𝑦𝐴𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴)
2512, 18, 22, 24el2122old 43480 . . . . 5 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   )
2625int2 43367 . . . 4 (   Tr 𝐴   ▶   ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
2726gen12 43379 . . 3 (   Tr 𝐴   ▶   𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
28 dftr2 5268 . . . 4 (Tr suc 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
2928biimpri 227 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
3027, 29el1 43389 . 2 (   Tr 𝐴   ▶   Tr suc 𝐴   )
3130in1 43332 1 (Tr 𝐴 → Tr suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wo 846  wal 1540   = wceq 1542  wcel 2107  wss 3949  Tr wtr 5266  suc csuc 6367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-uni 4910  df-tr 5267  df-suc 6371  df-vd1 43331  df-vhc2 43342  df-vhc3 43350
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator