Theorem sspwtrALT2

Description: Short predicate calculus proof of the right-to-left implication of dftr4 . 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 , which is the virtual deduction proof sspwtr without virtual deductions. (Contributed by Alan Sare, 3-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ssel	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( 𝑦 ∈ 𝐴 → 𝑦 ∈ 𝒫 𝐴 ) )
2	1	adantld	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝒫 𝐴 ) )
3		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝐴 → 𝑦 ⊆ 𝐴 )
4	2 3	syl6	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ⊆ 𝐴 ) )
5		simpl	⊢ ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝑦 )
6	5	a1i	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝑦 ) )
7		ssel	⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐴 ) )
8	4 6 7	syl6c	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
9	8	alrimivv	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
10		dftr2	⊢ ( Tr 𝐴 ↔ ∀ 𝑧 ∀ 𝑦 ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 ) )
11	9 10	sylibr	⊢ ( 𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴 )