Theorem sspwtrALT2 43666

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

Syntax hints:   → wi 4   ∧ wa 396  ∀wal 1539   ∈ wcel 2106   ⊆ wss 3948  𝒫 cpw 4602  Tr wtr 5265

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 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-pw 4604  df-uni 4909  df-tr 5266

This theorem is referenced by: (None)