Step |
Hyp |
Ref |
Expression |
1 |
|
prtlem18.1 |
⊢ ∼ = { 〈 𝑥 , 𝑦 〉 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) } |
2 |
|
rspe |
⊢ ( ( 𝑣 ∈ 𝐴 ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) |
3 |
2
|
expr |
⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 → ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) |
4 |
1
|
prtlem13 |
⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑣 ∈ 𝐴 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) |
5 |
3 4
|
syl6ibr |
⊢ ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 → 𝑧 ∼ 𝑤 ) ) |
6 |
5
|
a1i |
⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 → 𝑧 ∼ 𝑤 ) ) ) |
7 |
1
|
prtlem13 |
⊢ ( 𝑧 ∼ 𝑤 ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑤 ∈ 𝑝 ) ) |
8 |
|
prtlem17 |
⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑧 ∈ 𝑝 ∧ 𝑤 ∈ 𝑝 ) → 𝑤 ∈ 𝑣 ) ) ) |
9 |
7 8
|
syl7bi |
⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑧 ∼ 𝑤 → 𝑤 ∈ 𝑣 ) ) ) |
10 |
6 9
|
impbidd |
⊢ ( Prt 𝐴 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑧 ∈ 𝑣 ) → ( 𝑤 ∈ 𝑣 ↔ 𝑧 ∼ 𝑤 ) ) ) |