This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | prtlem17 | ⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑥 ) ) ) |
| 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 | biimtrrid | ⊢ ( Prt 𝐴 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑥 ) ) ) ) |
| 10 | 9 | expd | ⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑦 ∈ 𝐴 → ( 𝑧 ∈ 𝑦 → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝑥 ) ) ) ) ) |
| 11 | 10 | imp5a | ⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ( 𝑦 ∈ 𝐴 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑥 ) ) ) ) |
| 12 | 11 | imp4b | ⊢ ( ( Prt 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝑤 ∈ 𝑥 ) ) |
| 13 | 12 | exlimdv | ⊢ ( ( Prt 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ) → ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) ) → 𝑤 ∈ 𝑥 ) ) |
| 14 | 1 13 | biimtrid | ⊢ ( ( Prt 𝐴 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑥 ) ) |
| 15 | 14 | ex | ⊢ ( Prt 𝐴 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝑧 ∈ 𝑦 ∧ 𝑤 ∈ 𝑦 ) → 𝑤 ∈ 𝑥 ) ) ) |