Theorem suctrALTcfVD 44896

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 44543) 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 44895 is suctrALTcfVD 44896 without virtual deductions and was derived automatically from suctrALTcfVD 44896. 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 6393	. . . . . . . 8 ⊢ 𝐴 ⊆ suc 𝐴
2		idn1 44548	. . . . . . . . 9 ⊢ (   Tr 𝐴   ▶   Tr 𝐴   )
3		idn1 44548	. . . . . . . . . 10 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )
4		simpl 482	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦)
5	3, 4	el1 44602	. . . . . . . . 9 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑧 ∈ 𝑦   )
6		idn1 44548	. . . . . . . . 9 ⊢ (   𝑦 ∈ 𝐴   ▶   𝑦 ∈ 𝐴   )
7		trel 5210	. . . . . . . . . 10 ⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
8	7	3impib 1116	. . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)
9	2, 5, 6, 8	el123 44737	. . . . . . . 8 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ 𝐴   )
10		ssel2 3932	. . . . . . . 8 ⊢ ((𝐴 ⊆ suc 𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ suc 𝐴)
11	1, 9, 10	el0321old 44690	. . . . . . 7 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
12	11	int3 44586	. . . . . 6 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )   ▶   (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)   )
13		idn1 44548	. . . . . . . . 9 ⊢ (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
14		eleq2 2817	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴))
15	14	biimpac 478	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴)
16	5, 13, 15	el12 44699	. . . . . . . 8 ⊢ (   (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ 𝐴   )
17	1, 16, 10	el021old 44675	. . . . . . 7 ⊢ (   (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
18	17	int2 44580	. . . . . 6 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)   )
19		simpr 484	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
20	3, 19	el1 44602	. . . . . . 7 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
21		elsuci 6380	. . . . . . 7 ⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))
22	20, 21	el1 44602	. . . . . 6 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)   )
23		jao 962	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)))
24	23	3imp 1110	. . . . . 6 ⊢ (((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴)
25	12, 18, 22, 24	el2122old 44692	. . . . 5 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   )
26	25	int2 44580	. . . 4 ⊢ (   Tr 𝐴   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
27	26	gen12 44592	. . 3 ⊢ (   Tr 𝐴   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
28		dftr2 5204	. . . 4 ⊢ (Tr suc 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
29	28	biimpri 228	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
30	27, 29	el1 44602	. 2 ⊢ (   Tr 𝐴   ▶   Tr suc 𝐴   )
31	30	in1 44545	1 ⊢ (Tr 𝐴 → Tr suc 𝐴)

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

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 3440  df-un 3910  df-ss 3922  df-sn 4580  df-uni 4862  df-tr 5203  df-suc 6317  df-vd1 44544  df-vhc2 44555  df-vhc3 44563

This theorem is referenced by: (None)