Theorem isptfin

Description: The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010)

	Ref	Expression
Hypothesis	isptfin.1	⊢ 𝑋 = ∪ 𝐴
Assertion	isptfin	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ PtFin ↔ ∀ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦 } ∈ Fin ) )

Proof

Step	Hyp	Ref	Expression
1		isptfin.1	⊢ 𝑋 = ∪ 𝐴
2		unieq	⊢ ( 𝑎 = 𝐴 → ∪ 𝑎 = ∪ 𝐴 )
3	2 1	eqtr4di	⊢ ( 𝑎 = 𝐴 → ∪ 𝑎 = 𝑋 )
4		rabeq	⊢ ( 𝑎 = 𝐴 → { 𝑦 ∈ 𝑎 ∣ 𝑥 ∈ 𝑦 } = { 𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦 } )
5	4	eleq1d	⊢ ( 𝑎 = 𝐴 → ( { 𝑦 ∈ 𝑎 ∣ 𝑥 ∈ 𝑦 } ∈ Fin ↔ { 𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦 } ∈ Fin ) )
6	3 5	raleqbidv	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ ∪ 𝑎 { 𝑦 ∈ 𝑎 ∣ 𝑥 ∈ 𝑦 } ∈ Fin ↔ ∀ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦 } ∈ Fin ) )
7		df-ptfin	⊢ PtFin = { 𝑎 ∣ ∀ 𝑥 ∈ ∪ 𝑎 { 𝑦 ∈ 𝑎 ∣ 𝑥 ∈ 𝑦 } ∈ Fin }
8	6 7	elab2g	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ PtFin ↔ ∀ 𝑥 ∈ 𝑋 { 𝑦 ∈ 𝐴 ∣ 𝑥 ∈ 𝑦 } ∈ Fin ) )