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 42432
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 42078) 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 42431 is suctrALTcfVD 42432 without virtual deductions and was derived automatically from suctrALTcfVD 42432. 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 6328 . . . . . . . 8 𝐴 ⊆ suc 𝐴
2 idn1 42083 . . . . . . . . 9 (   Tr 𝐴   ▶   Tr 𝐴   )
3 idn1 42083 . . . . . . . . . 10 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑧𝑦𝑦 ∈ suc 𝐴)   )
4 simpl 482 . . . . . . . . . 10 ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧𝑦)
53, 4el1 42137 . . . . . . . . 9 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑧𝑦   )
6 idn1 42083 . . . . . . . . 9 (   𝑦𝐴   ▶   𝑦𝐴   )
7 trel 5194 . . . . . . . . . 10 (Tr 𝐴 → ((𝑧𝑦𝑦𝐴) → 𝑧𝐴))
873impib 1114 . . . . . . . . 9 ((Tr 𝐴𝑧𝑦𝑦𝐴) → 𝑧𝐴)
92, 5, 6, 8el123 42273 . . . . . . . 8 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧𝐴   )
10 ssel2 3912 . . . . . . . 8 ((𝐴 ⊆ suc 𝐴𝑧𝐴) → 𝑧 ∈ suc 𝐴)
111, 9, 10el0321old 42226 . . . . . . 7 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1211int3 42121 . . . . . 6 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   (𝑦𝐴𝑧 ∈ suc 𝐴)   )
13 idn1 42083 . . . . . . . . 9 (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
14 eleq2 2827 . . . . . . . . . 10 (𝑦 = 𝐴 → (𝑧𝑦𝑧𝐴))
1514biimpac 478 . . . . . . . . 9 ((𝑧𝑦𝑦 = 𝐴) → 𝑧𝐴)
165, 13, 15el12 42235 . . . . . . . 8 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧𝐴   )
171, 16, 10el021old 42210 . . . . . . 7 (   (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
1817int2 42115 . . . . . 6 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴𝑧 ∈ suc 𝐴)   )
19 simpr 484 . . . . . . . 8 ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
203, 19el1 42137 . . . . . . 7 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
21 elsuci 6317 . . . . . . 7 (𝑦 ∈ suc 𝐴 → (𝑦𝐴𝑦 = 𝐴))
2220, 21el1 42137 . . . . . 6 (   (𝑧𝑦𝑦 ∈ suc 𝐴)   ▶   (𝑦𝐴𝑦 = 𝐴)   )
23 jao 957 . . . . . . 7 ((𝑦𝐴𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴𝑧 ∈ suc 𝐴) → ((𝑦𝐴𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)))
24233imp 1109 . . . . . 6 (((𝑦𝐴𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴𝑧 ∈ suc 𝐴) ∧ (𝑦𝐴𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴)
2512, 18, 22, 24el2122old 42228 . . . . 5 (   (   Tr 𝐴   ,   (𝑧𝑦𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   )
2625int2 42115 . . . 4 (   Tr 𝐴   ▶   ((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
2726gen12 42127 . . 3 (   Tr 𝐴   ▶   𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
28 dftr2 5189 . . . 4 (Tr suc 𝐴 ↔ ∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
2928biimpri 227 . . 3 (∀𝑧𝑦((𝑧𝑦𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
3027, 29el1 42137 . 2 (   Tr 𝐴   ▶   Tr suc 𝐴   )
3130in1 42080 1 (Tr 𝐴 → Tr suc 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 843  wal 1537   = wceq 1539  wcel 2108  wss 3883  Tr wtr 5187  suc csuc 6253
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-sn 4559  df-uni 4837  df-tr 5188  df-suc 6257  df-vd1 42079  df-vhc2 42090  df-vhc3 42098
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator