Metamath Proof Explorer

Theorem fneint

Description: If a cover is finer than another, every point can be approached more closely by intersections. (Contributed by Jeff Hankins, 11-Oct-2009)

Ref Expression
Assertion fneint ⊢AFneB→⋂x∈B|P∈x⊆⋂x∈A|P∈x

Proof

Step Hyp Ref Expression
1 eleq2w ⊢x=y→P∈x↔P∈y
2 1 elrab ⊢y∈x∈A|P∈x↔y∈A∧P∈y
3 fnessex ⊢AFneB∧y∈A∧P∈y→∃z∈BP∈z∧z⊆y
4 3 3expb ⊢AFneB∧y∈A∧P∈y→∃z∈BP∈z∧z⊆y
5 eleq2w ⊢x=z→P∈x↔P∈z
6 5 intminss ⊢z∈B∧P∈z→⋂x∈B|P∈x⊆z
7 sstr ⊢⋂x∈B|P∈x⊆z∧z⊆y→⋂x∈B|P∈x⊆y
8 6 7 sylan ⊢z∈B∧P∈z∧z⊆y→⋂x∈B|P∈x⊆y
9 8 expl ⊢z∈B→P∈z∧z⊆y→⋂x∈B|P∈x⊆y
10 9 rexlimiv ⊢∃z∈BP∈z∧z⊆y→⋂x∈B|P∈x⊆y
11 4 10 syl ⊢AFneB∧y∈A∧P∈y→⋂x∈B|P∈x⊆y
12 11 ex ⊢AFneB→y∈A∧P∈y→⋂x∈B|P∈x⊆y
13 2 12 biimtrid ⊢AFneB→y∈x∈A|P∈x→⋂x∈B|P∈x⊆y
14 13 ralrimiv ⊢AFneB→∀y∈x∈A|P∈x⋂x∈B|P∈x⊆y
15 ssint ⊢⋂x∈B|P∈x⊆⋂x∈A|P∈x↔∀y∈x∈A|P∈x⋂x∈B|P∈x⊆y
16 14 15 sylibr ⊢AFneB→⋂x∈B|P∈x⊆⋂x∈A|P∈x