Proof of Theorem prtlem10
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | simpr 484 | . . . . 5
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) | 
| 2 |  | simpl 482 | . . . . . 6
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → ∼ Er 𝐴) | 
| 3 | 2, 1 | erref 8766 | . . . . 5
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∼ 𝑧) | 
| 4 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑣 = 𝑧 → (𝑣 ∼ 𝑧 ↔ 𝑧 ∼ 𝑧)) | 
| 5 |  | breq1 5145 | . . . . . . . 8
⊢ (𝑣 = 𝑧 → (𝑣 ∼ 𝑤 ↔ 𝑧 ∼ 𝑤)) | 
| 6 | 4, 5 | anbi12d 632 | . . . . . . 7
⊢ (𝑣 = 𝑧 → ((𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤) ↔ (𝑧 ∼ 𝑧 ∧ 𝑧 ∼ 𝑤))) | 
| 7 | 6 | rspcev 3621 | . . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ (𝑧 ∼ 𝑧 ∧ 𝑧 ∼ 𝑤)) → ∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) | 
| 8 | 7 | expr 456 | . . . . 5
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑧 ∼ 𝑧) → (𝑧 ∼ 𝑤 → ∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤))) | 
| 9 | 1, 3, 8 | syl2anc 584 | . . . 4
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑧 ∼ 𝑤 → ∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤))) | 
| 10 |  | simplll 774 | . . . . . 6
⊢ ((((
∼
Er 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) → ∼ Er 𝐴) | 
| 11 |  | simprl 770 | . . . . . 6
⊢ ((((
∼
Er 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) → 𝑣 ∼ 𝑧) | 
| 12 |  | simprr 772 | . . . . . 6
⊢ ((((
∼
Er 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) → 𝑣 ∼ 𝑤) | 
| 13 | 10, 11, 12 | ertr3d 8764 | . . . . 5
⊢ ((((
∼
Er 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) → 𝑧 ∼ 𝑤) | 
| 14 | 13 | rexlimdva2 3156 | . . . 4
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤) → 𝑧 ∼ 𝑤)) | 
| 15 | 9, 14 | impbid 212 | . . 3
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤))) | 
| 16 |  | vex 3483 | . . . . . 6
⊢ 𝑧 ∈ V | 
| 17 |  | vex 3483 | . . . . . 6
⊢ 𝑣 ∈ V | 
| 18 | 16, 17 | elec 8792 | . . . . 5
⊢ (𝑧 ∈ [𝑣] ∼ ↔ 𝑣 ∼ 𝑧) | 
| 19 |  | vex 3483 | . . . . . 6
⊢ 𝑤 ∈ V | 
| 20 | 19, 17 | elec 8792 | . . . . 5
⊢ (𝑤 ∈ [𝑣] ∼ ↔ 𝑣 ∼ 𝑤) | 
| 21 | 18, 20 | anbi12i 628 | . . . 4
⊢ ((𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ) ↔ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) | 
| 22 | 21 | rexbii 3093 | . . 3
⊢
(∃𝑣 ∈
𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ) ↔
∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) | 
| 23 | 15, 22 | bitr4di 289 | . 2
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼
))) | 
| 24 | 23 | ex 412 | 1
⊢ ( ∼ Er
𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼
)))) |