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 ⊢ A Fne B → ⋂ 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 ⊢ A Fne B ∧ y ∈ A ∧ P ∈ y → ∃ z ∈ B P ∈ z ∧ z ⊆ y
4 3 3expb ⊢ A Fne B ∧ y ∈ A ∧ P ∈ y → ∃ z ∈ B P ∈ 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 ∈ B P ∈ z ∧ z ⊆ y → ⋂ x ∈ B | P ∈ x ⊆ y
11 4 10 syl ⊢ A Fne B ∧ y ∈ A ∧ P ∈ y → ⋂ x ∈ B | P ∈ x ⊆ y
12 11 ex ⊢ A Fne B → y ∈ A ∧ P ∈ y → ⋂ x ∈ B | P ∈ x ⊆ y
13 2 12 syl5bi ⊢ A Fne B → y ∈ x ∈ A | P ∈ x → ⋂ x ∈ B | P ∈ x ⊆ y
14 13 ralrimiv ⊢ A Fne B → ∀ 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 ⊢ A Fne B → ⋂ x ∈ B | P ∈ x ⊆ ⋂ x ∈ A | P ∈ x