Proof of Theorem prtlem15
Step | Hyp | Ref
| Expression |
1 | | anabs7 664 |
. . . . . . 7
⊢ (((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦))) ↔ ((𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦))) |
2 | | an43 658 |
. . . . . . . 8
⊢ (((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) ↔ ((𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦))) |
3 | 2 | anbi2i 626 |
. . . . . . 7
⊢ (((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦))) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦) ∧ (𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦)))) |
4 | 1, 3, 2 | 3bitr4ri 307 |
. . . . . 6
⊢ (((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) ↔ ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)))) |
5 | | prtlem14 36625 |
. . . . . . . 8
⊢ (Prt
𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → 𝑥 = 𝑦))) |
6 | | an3 659 |
. . . . . . . . 9
⊢ (((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦)) |
7 | | elequ2 2125 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑣 ∈ 𝑥 ↔ 𝑣 ∈ 𝑦)) |
8 | 7 | anbi2d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦))) |
9 | 6, 8 | syl5ibr 249 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥))) |
10 | 5, 9 | syl8 76 |
. . . . . . 7
⊢ (Prt
𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) → (((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥))))) |
11 | 10 | imp4a 426 |
. . . . . 6
⊢ (Prt
𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑤 ∈ 𝑥 ∧ 𝑤 ∈ 𝑦) ∧ ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦))) → (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥)))) |
12 | 4, 11 | syl7bi 258 |
. . . . 5
⊢ (Prt
𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥)))) |
13 | 12 | expdimp 456 |
. . . 4
⊢ ((Prt
𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐴 → (((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥)))) |
14 | 13 | rexlimdv 3202 |
. . 3
⊢ ((Prt
𝐴 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥))) |
15 | 14 | reximdva 3193 |
. 2
⊢ (Prt
𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑥 ∈ 𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥))) |
16 | | elequ2 2125 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝑢 ∈ 𝑥 ↔ 𝑢 ∈ 𝑧)) |
17 | | elequ2 2125 |
. . . 4
⊢ (𝑥 = 𝑧 → (𝑣 ∈ 𝑥 ↔ 𝑣 ∈ 𝑧)) |
18 | 16, 17 | anbi12d 634 |
. . 3
⊢ (𝑥 = 𝑧 → ((𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧))) |
19 | 18 | cbvrexvw 3359 |
. 2
⊢
(∃𝑥 ∈
𝐴 (𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑥) ↔ ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧)) |
20 | 15, 19 | syl6ib 254 |
1
⊢ (Prt
𝐴 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝑢 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) ∧ (𝑤 ∈ 𝑦 ∧ 𝑣 ∈ 𝑦)) → ∃𝑧 ∈ 𝐴 (𝑢 ∈ 𝑧 ∧ 𝑣 ∈ 𝑧))) |