Metamath Proof Explorer

Theorem prtlem18

Description: Lemma for prter2 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem18.1 ⊢ ∼ ˙ = x y | ∃ u ∈ A x ∈ u ∧ y ∈ u
Assertion prtlem18 ⊢ Prt A → v ∈ A ∧ z ∈ v → w ∈ v ↔ z ∼ ˙ w

Proof

Step Hyp Ref Expression
1 prtlem18.1 ⊢ ∼ ˙ = x y | ∃ u ∈ A x ∈ u ∧ y ∈ u
2 rspe ⊢ v ∈ A ∧ z ∈ v ∧ w ∈ v → ∃ v ∈ A z ∈ v ∧ w ∈ v
3 2 expr ⊢ v ∈ A ∧ z ∈ v → w ∈ v → ∃ v ∈ A z ∈ v ∧ w ∈ v
4 1 prtlem13 ⊢ z ∼ ˙ w ↔ ∃ v ∈ A z ∈ v ∧ w ∈ v
5 3 4 imbitrrdi ⊢ v ∈ A ∧ z ∈ v → w ∈ v → z ∼ ˙ w
6 5 a1i ⊢ Prt A → v ∈ A ∧ z ∈ v → w ∈ v → z ∼ ˙ w
7 1 prtlem13 ⊢ z ∼ ˙ w ↔ ∃ p ∈ A z ∈ p ∧ w ∈ p
8 prtlem17 ⊢ Prt A → v ∈ A ∧ z ∈ v → ∃ p ∈ A z ∈ p ∧ w ∈ p → w ∈ v
9 7 8 syl7bi ⊢ Prt A → v ∈ A ∧ z ∈ v → z ∼ ˙ w → w ∈ v
10 6 9 impbidd ⊢ Prt A → v ∈ A ∧ z ∈ v → w ∈ v ↔ z ∼ ˙ w