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 ⊢∼˙ErA→z∈A→z∼˙w↔∃v∈Az∈v∼˙∧w∈v∼˙

Proof

Step Hyp Ref Expression
1 simpr ⊢∼˙ErA∧z∈A→z∈A
2 simpl ⊢∼˙ErA∧z∈A→∼˙ErA
3 2 1 erref ⊢∼˙ErA∧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∈Av∼˙z∧v∼˙w
8 7 expr ⊢z∈A∧z∼˙z→z∼˙w→∃v∈Av∼˙z∧v∼˙w
9 1 3 8 syl2anc ⊢∼˙ErA∧z∈A→z∼˙w→∃v∈Av∼˙z∧v∼˙w
10 simplll ⊢∼˙ErA∧z∈A∧v∈A∧v∼˙z∧v∼˙w→∼˙ErA
11 simprl ⊢∼˙ErA∧z∈A∧v∈A∧v∼˙z∧v∼˙w→v∼˙z
12 simprr ⊢∼˙ErA∧z∈A∧v∈A∧v∼˙z∧v∼˙w→v∼˙w
13 10 11 12 ertr3d ⊢∼˙ErA∧z∈A∧v∈A∧v∼˙z∧v∼˙w→z∼˙w
14 13 rexlimdva2 ⊢∼˙ErA∧z∈A→∃v∈Av∼˙z∧v∼˙w→z∼˙w
15 9 14 impbid ⊢∼˙ErA∧z∈A→z∼˙w↔∃v∈Av∼˙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∈Az∈v∼˙∧w∈v∼˙↔∃v∈Av∼˙z∧v∼˙w
23 15 22 bitr4di ⊢∼˙ErA∧z∈A→z∼˙w↔∃v∈Az∈v∼˙∧w∈v∼˙
24 23 ex ⊢∼˙ErA→z∈A→z∼˙w↔∃v∈Az∈v∼˙∧w∈v∼˙