This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 → ( 𝑧 ∈ 𝐴 → ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ [ 𝑣 ] ∼ ∧ 𝑤 ∈ [ 𝑣 ] ∼ ) ) ) )

Proof

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