Theorem suctrALTcfVD 44912

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 44559) 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 44911 is suctrALTcfVD 44912 without virtual deductions and was derived automatically from suctrALTcfVD 44912. 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.

Step	Hyp	Ref	Expression
1		sssucid 6414	. . . . . . . 8 ⊢ 𝐴 ⊆ suc 𝐴
2		idn1 44564	. . . . . . . . 9 ⊢ (   Tr 𝐴   ▶   Tr 𝐴   )
3		idn1 44564	. . . . . . . . . 10 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )
4		simpl 482	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦)
5	3, 4	el1 44618	. . . . . . . . 9 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑧 ∈ 𝑦   )
6		idn1 44564	. . . . . . . . 9 ⊢ (   𝑦 ∈ 𝐴   ▶   𝑦 ∈ 𝐴   )
7		trel 5223	. . . . . . . . . 10 ⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
8	7	3impib 1116	. . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)
9	2, 5, 6, 8	el123 44753	. . . . . . . 8 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ 𝐴   )
10		ssel2 3941	. . . . . . . 8 ⊢ ((𝐴 ⊆ suc 𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ suc 𝐴)
11	1, 9, 10	el0321old 44706	. . . . . . 7 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
12	11	int3 44602	. . . . . 6 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )   ▶   (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)   )
13		idn1 44564	. . . . . . . . 9 ⊢ (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
14		eleq2 2817	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴))
15	14	biimpac 478	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴)
16	5, 13, 15	el12 44715	. . . . . . . 8 ⊢ (   (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ 𝐴   )
17	1, 16, 10	el021old 44691	. . . . . . 7 ⊢ (   (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
18	17	int2 44596	. . . . . 6 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)   )
19		simpr 484	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
20	3, 19	el1 44618	. . . . . . 7 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
21		elsuci 6401	. . . . . . 7 ⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))
22	20, 21	el1 44618	. . . . . 6 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)   )
23		jao 962	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)))
24	23	3imp 1110	. . . . . 6 ⊢ (((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴)
25	12, 18, 22, 24	el2122old 44708	. . . . 5 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   )
26	25	int2 44596	. . . 4 ⊢ (   Tr 𝐴   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
27	26	gen12 44608	. . 3 ⊢ (   Tr 𝐴   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
28		dftr2 5216	. . . 4 ⊢ (Tr suc 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
29	28	biimpri 228	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
30	27, 29	el1 44618	. 2 ⊢ (   Tr 𝐴   ▶   Tr suc 𝐴   )
31	30	in1 44561	1 ⊢ (Tr 𝐴 → Tr suc 𝐴)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ⊆ wss 3914  Tr wtr 5214  suc csuc 6334

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931  df-sn 4590  df-uni 4872  df-tr 5215  df-suc 6338  df-vd1 44560  df-vhc2 44571  df-vhc3 44579

This theorem is referenced by: (None)