Metamath Proof Explorer

Theorem prtlem10

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

Ref Expression
Assertion prtlem10 ⊢ ∼ ˙ Er A → z ∈ A → z ∼ ˙ w ↔ ∃ v ∈ A z ∈ v ∼ ˙ ∧ w ∈ v ∼ ˙

Proof

Step Hyp Ref Expression
1 simpr ⊢ ∼ ˙ Er A ∧ z ∈ A → z ∈ A
2 simpl ⊢ ∼ ˙ Er A ∧ z ∈ A → ∼ ˙ Er A
3 2 1 erref ⊢ ∼ ˙ Er A ∧ z ∈ A → z ∼ ˙ z
4 breq1 ⊢ v = z → v ∼ ˙ z ↔ z ∼ ˙ z
5 breq1 ⊢ v = z → v ∼ ˙ w ↔ z ∼ ˙ w
6 4 5 anbi12d ⊢ v = z → v ∼ ˙ z ∧ v ∼ ˙ w ↔ z ∼ ˙ z ∧ z ∼ ˙ w
7 6 rspcev ⊢ z ∈ A ∧ z ∼ ˙ z ∧ z ∼ ˙ w → ∃ v ∈ A v ∼ ˙ z ∧ v ∼ ˙ w
8 7 expr ⊢ z ∈ A ∧ z ∼ ˙ z → z ∼ ˙ w → ∃ v ∈ A v ∼ ˙ z ∧ v ∼ ˙ w
9 1 3 8 syl2anc ⊢ ∼ ˙ Er A ∧ z ∈ A → z ∼ ˙ w → ∃ v ∈ A v ∼ ˙ z ∧ v ∼ ˙ w
10 simplll ⊢ ∼ ˙ Er A ∧ z ∈ A ∧ v ∈ A ∧ v ∼ ˙ z ∧ v ∼ ˙ w → ∼ ˙ Er A
11 simprl ⊢ ∼ ˙ Er A ∧ z ∈ A ∧ v ∈ A ∧ v ∼ ˙ z ∧ v ∼ ˙ w → v ∼ ˙ z
12 simprr ⊢ ∼ ˙ Er A ∧ z ∈ A ∧ v ∈ A ∧ v ∼ ˙ z ∧ v ∼ ˙ w → v ∼ ˙ w
13 10 11 12 ertr3d ⊢ ∼ ˙ Er A ∧ z ∈ A ∧ v ∈ A ∧ v ∼ ˙ z ∧ v ∼ ˙ w → z ∼ ˙ w
14 13 rexlimdva2 ⊢ ∼ ˙ Er A ∧ z ∈ A → ∃ v ∈ A v ∼ ˙ z ∧ v ∼ ˙ w → z ∼ ˙ w
15 9 14 impbid ⊢ ∼ ˙ Er A ∧ z ∈ A → z ∼ ˙ w ↔ ∃ v ∈ A v ∼ ˙ z ∧ v ∼ ˙ w
16 vex ⊢ z ∈ V
17 vex ⊢ v ∈ V
18 16 17 elec ⊢ z ∈ v ∼ ˙ ↔ v ∼ ˙ z
19 vex ⊢ w ∈ V
20 19 17 elec ⊢ w ∈ v ∼ ˙ ↔ v ∼ ˙ w
21 18 20 anbi12i ⊢ z ∈ v ∼ ˙ ∧ w ∈ v ∼ ˙ ↔ v ∼ ˙ z ∧ v ∼ ˙ w
22 21 rexbii ⊢ ∃ v ∈ A z ∈ v ∼ ˙ ∧ w ∈ v ∼ ˙ ↔ ∃ v ∈ A v ∼ ˙ z ∧ v ∼ ˙ w
23 15 22 bitr4di ⊢ ∼ ˙ Er A ∧ z ∈ A → z ∼ ˙ w ↔ ∃ v ∈ A z ∈ v ∼ ˙ ∧ w ∈ v ∼ ˙
24 23 ex ⊢ ∼ ˙ Er A → z ∈ A → z ∼ ˙ w ↔ ∃ v ∈ A z ∈ v ∼ ˙ ∧ w ∈ v ∼ ˙