Metamath Proof Explorer

Theorem 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.)

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 )

Ref Expression
Assertion suctrALTcfVD ⊢ Tr ⁡ A → Tr ⁡ suc ⁡ A

Proof

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