Theorem prtlem17

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010)

	Ref	Expression
Assertion	prtlem17	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) )
2		an32	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝐴 ) )
3		prtlem14	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ∈ 𝑦 ) → 𝑥 = 𝑦 ) ) )
4		elequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑦 ) )
5	4	biimprd	⊢ ( 𝑥 = 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑥 ) )
6	3 5	syl8	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ∈ 𝑦 ) → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑥 ) ) ) )
7	6	exp4a	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ 𝑥 → ( 𝑧 ∈ 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑥 ) ) ) ) )
8	7	impd	⊢ ( Prt 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ) → ( 𝑧 ∈ 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑥 ) ) ) )
9	2 8	syl5bir	⊢ ( Prt 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑥 ) ) ) )
10	9	expd	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑦 ∈ 𝐴 → ( 𝑧 ∈ 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑥 ) ) ) ) )
11	10	imp5a	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑦 ∈ 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑥 ) ) ) )
12	11	imp4b	⊢ ( ( Prt 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝑤 ∈ 𝑥 ) )
13	12	exlimdv	⊢ ( ( Prt 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ) → ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝑤 ∈ 𝑥 ) )
14	1 13	syl5bi	⊢ ( ( Prt 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑥 ) )
15	14	ex	⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑥 ) ) )