Step |
Hyp |
Ref |
Expression |
1 |
|
ptfinfin.1 |
⊢ 𝑋 = ∪ 𝐴 |
2 |
1
|
isptfin |
⊢ ( 𝐴 ∈ PtFin → ( 𝐴 ∈ PtFin ↔ ∀ 𝑝 ∈ 𝑋 { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } ∈ Fin ) ) |
3 |
2
|
ibi |
⊢ ( 𝐴 ∈ PtFin → ∀ 𝑝 ∈ 𝑋 { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } ∈ Fin ) |
4 |
|
eleq1 |
⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∈ 𝑥 ↔ 𝑃 ∈ 𝑥 ) ) |
5 |
4
|
rabbidv |
⊢ ( 𝑝 = 𝑃 → { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } = { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ) |
6 |
5
|
eleq1d |
⊢ ( 𝑝 = 𝑃 → ( { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } ∈ Fin ↔ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin ) ) |
7 |
6
|
rspccv |
⊢ ( ∀ 𝑝 ∈ 𝑋 { 𝑥 ∈ 𝐴 ∣ 𝑝 ∈ 𝑥 } ∈ Fin → ( 𝑃 ∈ 𝑋 → { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin ) ) |
8 |
3 7
|
syl |
⊢ ( 𝐴 ∈ PtFin → ( 𝑃 ∈ 𝑋 → { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin ) ) |
9 |
8
|
imp |
⊢ ( ( 𝐴 ∈ PtFin ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∈ Fin ) |