Theorem sspwtrALT2 44812

Description: Short predicate calculus proof of the right-to-left implication of dftr4 5221. A class which is a subclass of its power class is transitive. This proof was constructed by applying Metamath's minimize command to the proof of sspwtrALT 44811, which is the virtual deduction proof sspwtr 44810 without virtual deductions. (Contributed by Alan Sare, 3-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
sspwtrALT2	⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)

Proof of Theorem sspwtrALT2

Dummy variables 𝑧 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3940	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐴 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴))
2	1	adantld 490	. . . . 5 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝒫 𝐴))
3		elpwi 4570	. . . . 5 ⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴)
4	2, 3	syl6 35	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ 𝐴))
5		simpl 482	. . . . 5 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦)
6	5	a1i 11	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦))
7		ssel 3940	. . . 4 ⊢ (𝑦 ⊆ 𝐴 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴))
8	4, 6, 7	syl6c 70	. . 3 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
9	8	alrimivv 1928	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
10		dftr2 5216	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
11	9, 10	sylibr 234	1 ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4   ∧ wa 395  ∀wal 1538   ∈ wcel 2109   ⊆ wss 3914  𝒫 cpw 4563  Tr wtr 5214

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-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-pw 4565  df-uni 4872  df-tr 5215

This theorem is referenced by: (None)