Proof of Theorem prtlem10
Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . . 5
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
2 | | simpl 486 |
. . . . . 6
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → ∼ Er 𝐴) |
3 | 2, 1 | erref 8411 |
. . . . 5
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → 𝑧 ∼ 𝑧) |
4 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑣 = 𝑧 → (𝑣 ∼ 𝑧 ↔ 𝑧 ∼ 𝑧)) |
5 | | breq1 5056 |
. . . . . . . 8
⊢ (𝑣 = 𝑧 → (𝑣 ∼ 𝑤 ↔ 𝑧 ∼ 𝑤)) |
6 | 4, 5 | anbi12d 634 |
. . . . . . 7
⊢ (𝑣 = 𝑧 → ((𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤) ↔ (𝑧 ∼ 𝑧 ∧ 𝑧 ∼ 𝑤))) |
7 | 6 | rspcev 3537 |
. . . . . 6
⊢ ((𝑧 ∈ 𝐴 ∧ (𝑧 ∼ 𝑧 ∧ 𝑧 ∼ 𝑤)) → ∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) |
8 | 7 | expr 460 |
. . . . 5
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑧 ∼ 𝑧) → (𝑧 ∼ 𝑤 → ∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤))) |
9 | 1, 3, 8 | syl2anc 587 |
. . . 4
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑧 ∼ 𝑤 → ∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤))) |
10 | | simplll 775 |
. . . . . 6
⊢ ((((
∼
Er 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) → ∼ Er 𝐴) |
11 | | simprl 771 |
. . . . . 6
⊢ ((((
∼
Er 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) → 𝑣 ∼ 𝑧) |
12 | | simprr 773 |
. . . . . 6
⊢ ((((
∼
Er 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) → 𝑣 ∼ 𝑤) |
13 | 10, 11, 12 | ertr3d 8409 |
. . . . 5
⊢ ((((
∼
Er 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 ∈ 𝐴) ∧ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) → 𝑧 ∼ 𝑤) |
14 | 13 | rexlimdva2 3206 |
. . . 4
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤) → 𝑧 ∼ 𝑤)) |
15 | 9, 14 | impbid 215 |
. . 3
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤))) |
16 | | vex 3412 |
. . . . . 6
⊢ 𝑧 ∈ V |
17 | | vex 3412 |
. . . . . 6
⊢ 𝑣 ∈ V |
18 | 16, 17 | elec 8435 |
. . . . 5
⊢ (𝑧 ∈ [𝑣] ∼ ↔ 𝑣 ∼ 𝑧) |
19 | | vex 3412 |
. . . . . 6
⊢ 𝑤 ∈ V |
20 | 19, 17 | elec 8435 |
. . . . 5
⊢ (𝑤 ∈ [𝑣] ∼ ↔ 𝑣 ∼ 𝑤) |
21 | 18, 20 | anbi12i 630 |
. . . 4
⊢ ((𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ) ↔ (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) |
22 | 21 | rexbii 3170 |
. . 3
⊢
(∃𝑣 ∈
𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼ ) ↔
∃𝑣 ∈ 𝐴 (𝑣 ∼ 𝑧 ∧ 𝑣 ∼ 𝑤)) |
23 | 15, 22 | bitr4di 292 |
. 2
⊢ (( ∼ Er
𝐴 ∧ 𝑧 ∈ 𝐴) → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼
))) |
24 | 23 | ex 416 |
1
⊢ ( ∼ Er
𝐴 → (𝑧 ∈ 𝐴 → (𝑧 ∼ 𝑤 ↔ ∃𝑣 ∈ 𝐴 (𝑧 ∈ [𝑣] ∼ ∧ 𝑤 ∈ [𝑣] ∼
)))) |