suctrALTcfVD

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

		Ref	Expression
	Assertion	suctrALTcfVD	⊢ ( Tr 𝐴 → Tr suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		sssucid	⊢ 𝐴 ⊆ suc 𝐴
2		idn1	⊢ ( Tr 𝐴 ▶ Tr 𝐴 )
3		idn1	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ▶ ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) )
4		simpl	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ 𝑦 )
5	3 4	el1	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ▶ 𝑧 ∈ 𝑦 )
6		idn1	⊢ ( 𝑦 ∈ 𝐴 ▶ 𝑦 ∈ 𝐴 )
7		trel	⊢ ( Tr 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
8	7	3impib	⊢ ( ( Tr 𝐴 ∧ 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
9	2 5 6 8	el123	⊢ ( ( Tr 𝐴 , ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) , 𝑦 ∈ 𝐴 ) ▶ 𝑧 ∈ 𝐴 )
10		ssel2	⊢ ( ( 𝐴 ⊆ suc 𝐴 ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ suc 𝐴 )
11	1 9 10	el0321old	⊢ ( ( Tr 𝐴 , ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) , 𝑦 ∈ 𝐴 ) ▶ 𝑧 ∈ suc 𝐴 )
12	11	int3	⊢ ( ( Tr 𝐴 , ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) ▶ ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) )
13		idn1	⊢ ( 𝑦 = 𝐴 ▶ 𝑦 = 𝐴 )
14		eleq2	⊢ ( 𝑦 = 𝐴 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝐴 ) )
15	14	biimpac	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 = 𝐴 ) → 𝑧 ∈ 𝐴 )
16	5 13 15	el12	⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) , 𝑦 = 𝐴 ) ▶ 𝑧 ∈ 𝐴 )
17	1 16 10	el021old	⊢ ( ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) , 𝑦 = 𝐴 ) ▶ 𝑧 ∈ suc 𝐴 )
18	17	int2	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ▶ ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) )
19		simpr	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑦 ∈ suc 𝐴 )
20	3 19	el1	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ▶ 𝑦 ∈ suc 𝐴 )
21		elsuci	⊢ ( 𝑦 ∈ suc 𝐴 → ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
22	20 21	el1	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ▶ ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) )
23		jao	⊢ ( ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) → ( ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) → ( ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) → 𝑧 ∈ suc 𝐴 ) ) )
24	23	3imp	⊢ ( ( ( 𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴 ) ∧ ( 𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴 ) ∧ ( 𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴 ) ) → 𝑧 ∈ suc 𝐴 )
25	12 18 22 24	el2122old	⊢ ( ( Tr 𝐴 , ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) ) ▶ 𝑧 ∈ suc 𝐴 )
26	25	int2	⊢ ( Tr 𝐴 ▶ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
27	26	gen12	⊢ ( Tr 𝐴 ▶ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
28		dftr2	⊢ ( Tr suc 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) )
29	28	biimpri	⊢ ( ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴 ) → 𝑧 ∈ suc 𝐴 ) → Tr suc 𝐴 )
30	27 29	el1	⊢ ( Tr 𝐴 ▶ Tr suc 𝐴 )
31	30	in1	⊢ ( Tr 𝐴 → Tr suc 𝐴 )

1::	\|- (. Tr A ->. Tr A ).
2::	\|- (. ......... ( z e. y /\ y e. suc A ) ->. ( z e. y /\ y e. suc A ) ).
3:2:	\|- (. ......... ( z e. y /\ y e. suc A ) ->. z e. y ).
4::	\|- (. ................................... ....... y e. A ->. y e. A ).
5:1,3,4:	\|- (. (. Tr A ,. ( z e. y /\ y e. suc A ) , y e. A ). ->. z e. A ).
6::	\|- A C_ suc A
7:5,6:	\|- (. (. Tr A ,. ( z e. y /\ y e. suc A ) , y e. A ). ->. z e. suc A ).
8:7:	\|- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. ( y e. A -> z e. suc A ) ).
9::	\|- (. ................................... ...... y = A ->. y = A ).
10:3,9:	\|- (. ........ (. ( z e. y /\ y e. suc A ) , y = A ). ->. z e. A ).
11:10,6:	\|- (. ........ (. ( z e. y /\ y e. suc A ) , y = A ). ->. z e. suc A ).
12:11:	\|- (. .......... ( z e. y /\ y e. suc A ) ->. ( y = A -> z e. suc A ) ).
13:2:	\|- (. .......... ( z e. y /\ y e. suc A ) ->. y e. suc A ).
14:13:	\|- (. .......... ( z e. y /\ y e. suc A ) ->. ( y e. A \/ y = A ) ).
15:8,12,14:	\|- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. z e. suc A ).
16:15:	\|- (. Tr A ->. ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ).
17:16:	\|- (. Tr A ->. A. z A. y ( ( z e. y /\ y e. suc A ) -> z e. suc A ) ).
18:17:	\|- (. Tr A ->. Tr suc A ).
qed:18:	\|- ( Tr A -> Tr suc A )

Metamath Proof Explorer

Theorem suctrALTcfVD

Proof