Theorem sspwtrALT2 43353

Description: Short predicate calculus proof of the right-to-left implication of dftr4 5265. 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 43352, which is the virtual deduction proof sspwtr 43351 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 3971	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐴 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴))
2	1	adantld 491	. . . . 5 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝒫 𝐴))
3		elpwi 4603	. . . . 5 ⊢ (𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴)
4	2, 3	syl6 35	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑦 ⊆ 𝐴))
5		simpl 483	. . . . 5 ⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦)
6	5	a1i 11	. . . 4 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝑦))
7		ssel 3971	. . . 4 ⊢ (𝑦 ⊆ 𝐴 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴))
8	4, 6, 7	syl6c 70	. . 3 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
9	8	alrimivv 1931	. 2 ⊢ (𝐴 ⊆ 𝒫 𝐴 → ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
10		dftr2 5260	. 2 ⊢ (Tr 𝐴 ↔ ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴) → 𝑧 ∈ 𝐴))
11	9, 10	sylibr 233	1 ⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1539   ∈ wcel 2106   ⊆ wss 3944  𝒫 cpw 4596  Tr wtr 5258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961  df-pw 4598  df-uni 4902  df-tr 5259

This theorem is referenced by: (None)