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 44943
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 44589) 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 44942 is suctrALTcfVD 44943 without virtual deductions and was derived automatically from suctrALTcfVD 44943. 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 6464 . . . . . . . 8 𝐴 ⊆ suc 𝐴
2 idn1 44594 . . . . . . . . 9 (   Tr 𝐴   ▶   Tr 𝐴   )
3 idn1 44594 . . . . . . . . . 10 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑧𝑦𝑦 ∈ suc 𝐴)   )
4 simpl 482 . . . . . . . . . 10 ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧𝑦)
53, 4el1 44648 . . . . . . . . 9 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑧𝑦   )
6 idn1 44594 . . . . . . . . 9 (   𝑦𝐴   ▶   𝑦𝐴   )
7 trel 5268 . . . . . . . . . 10 (Tr 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
873impib 1117 . . . . . . . . 9 ((Tr 𝐴𝑧𝑦𝑦𝐴) → 𝑧𝐴)
92, 5, 6, 8el123 44784 . . . . . . . 8 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧𝐴   )
10 ssel2 3978 . . . . . . . 8 ((𝐴 ⊆ suc 𝐴𝑧𝐴) → 𝑧 ∈ suc 𝐴)
111, 9, 10el0321old 44737 . . . . . . 7 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1211int3 44632 . . . . . 6 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   (𝑦𝐴𝑧 ∈ suc 𝐴)   )
13 idn1 44594 . . . . . . . . 9 (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
14 eleq2 2830 . . . . . . . . . 10 (𝑦 = 𝐴 → (𝑧𝑦𝑧𝐴))
1514biimpac 478 . . . . . . . . 9 ((𝑧𝑦𝑦 = 𝐴) → 𝑧𝐴)
165, 13, 15el12 44746 . . . . . . . 8 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧𝐴   )
171, 16, 10el021old 44721 . . . . . . 7 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1817int2 44626 . . . . . 6 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴𝑧 ∈ suc 𝐴)   )
19 simpr 484 . . . . . . . 8 ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
203, 19el1 44648 . . . . . . 7 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
21 elsuci 6451 . . . . . . 7 (𝑦 ∈ suc 𝐴 → (𝑦𝐴𝑦 = 𝐴))
2220, 21el1 44648 . . . . . 6 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦𝐴𝑦 = 𝐴)   )
23 jao 963 . . . . . . 7 ((𝑦𝐴𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴𝑧 ∈ suc 𝐴) → ((𝑦𝐴𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)))
24233imp 1111 . . . . . 6 (((𝑦𝐴𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴𝑧 ∈ suc 𝐴) ∧ (𝑦𝐴𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴)
2512, 18, 22, 24el2122old 44739 . . . . 5 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   )
2625int2 44626 . . . 4 (   Tr 𝐴   ▶   ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
2726gen12 44638 . . 3 (   Tr 𝐴   ▶   𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
28 dftr2 5261 . . . 4 (Tr suc 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
2928biimpri 228 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
3027, 29el1 44648 . 2 (   Tr 𝐴   ▶   Tr suc 𝐴   )
3130in1 44591 1 (Tr 𝐴 → Tr suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 848  wal 1538   = wceq 1540  wcel 2108  wss 3951  Tr wtr 5259  suc csuc 6386
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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-sn 4627  df-uni 4908  df-tr 5260  df-suc 6390  df-vd1 44590  df-vhc2 44601  df-vhc3 44609
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator