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) (Revised by Mario Carneiro, 12-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | prtlem18.1 | ⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) } | |
| Assertion | prtlem18 | ⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | prtlem18.1 | ⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) } | |
| 2 | rspe | ⊢ ( ( 𝑣 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) | |
| 3 | 2 | expr | ⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 → ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) |
| 4 | 1 | prtlem13 | ⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) |
| 5 | 3 4 | imbitrrdi | ⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 → 𝑧 ∼ 𝑤 ) ) |
| 6 | 5 | a1i | ⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 → 𝑧 ∼ 𝑤 ) ) ) |
| 7 | 1 | prtlem13 | ⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑤 ∈ 𝑝 ) ) |
| 8 | prtlem17 | ⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑤 ∈ 𝑝 ) → 𝑤 ∈ 𝑣 ) ) ) | |
| 9 | 7 8 | syl7bi | ⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑧 ∼ 𝑤 → 𝑤 ∈ 𝑣 ) ) ) |
| 10 | 6 9 | impbidd | ⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤 ) ) ) |