Theorem suctrALTcfVD 45381

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 45028) 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 45380 is suctrALTcfVD 45381 without virtual deductions and was derived automatically from suctrALTcfVD 45381. 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 6396	. . . . . . . 8 ⊢ 𝐴 ⊆ suc 𝐴
2		idn1 45033	. . . . . . . . 9 ⊢ (   Tr 𝐴   ▶   Tr 𝐴   )
3		idn1 45033	. . . . . . . . . 10 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )
4		simpl 484	. . . . . . . . . 10 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ 𝑦)
5	3, 4	el1 45087	. . . . . . . . 9 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑧 ∈ 𝑦   )
6		idn1 45033	. . . . . . . . 9 ⊢ (   𝑦 ∈ 𝐴   ▶   𝑦 ∈ 𝐴   )
7		trel 5190	. . . . . . . . . 10 ⊢ (Tr 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
8	7	3impib 1123	. . . . . . . . 9 ⊢ ((Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴)
9	2, 5, 6, 8	el123 45222	. . . . . . . 8 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ 𝐴   )
10		ssel2 3912	. . . . . . . 8 ⊢ ((𝐴 ⊆ suc 𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ suc 𝐴)
11	1, 9, 10	el0321old 45175	. . . . . . 7 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
12	11	int3 45071	. . . . . 6 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )   ▶   (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)   )
13		idn1 45033	. . . . . . . . 9 ⊢ (   𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
14		eleq2 2830	. . . . . . . . . 10 ⊢ (𝑦 = 𝐴 → (𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴))
15	14	biimpac 480	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴) → 𝑧 ∈ 𝐴)
16	5, 13, 15	el12 45184	. . . . . . . 8 ⊢ (   (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ 𝐴   )
17	1, 16, 10	el021old 45160	. . . . . . 7 ⊢ (   (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ,   𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
18	17	int2 45065	. . . . . 6 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)   )
19		simpr 486	. . . . . . . 8 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑦 ∈ suc 𝐴)
20	3, 19	el1 45087	. . . . . . 7 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
21		elsuci 6383	. . . . . . 7 ⊢ (𝑦 ∈ suc 𝐴 → (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴))
22	20, 21	el1 45087	. . . . . 6 ⊢ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)   )
23		jao 969	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) → ((𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴) → 𝑧 ∈ suc 𝐴)))
24	23	3imp 1117	. . . . . 6 ⊢ (((𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴) ∧ (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)) → 𝑧 ∈ suc 𝐴)
25	12, 18, 22, 24	el2122old 45177	. . . . 5 ⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )   ▶   𝑧 ∈ suc 𝐴   )
26	25	int2 45065	. . . 4 ⊢ (   Tr 𝐴   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
27	26	gen12 45077	. . 3 ⊢ (   Tr 𝐴   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
28		dftr2 5184	. . . 4 ⊢ (Tr suc 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴))
29	28	biimpri 230	. . 3 ⊢ (∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴) → Tr suc 𝐴)
30	27, 29	el1 45087	. 2 ⊢ (   Tr 𝐴   ▶   Tr suc 𝐴   )
31	30	in1 45030	1 ⊢ (Tr 𝐴 → Tr suc 𝐴)

Syntax hints:   → wi 4   ∧ wa 397   ∨ wo 854  ∀wal 1546   = wceq 1548   ∈ wcel 2121   ⊆ wss 3885  Tr wtr 5182  suc csuc 6316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-un 3890  df-ss 3902  df-sn 4559  df-uni 4842  df-tr 5183  df-suc 6320  df-vd1 45029  df-vhc2 45040  df-vhc3 45048

This theorem is referenced by: (None)