This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 Fne 𝐵 → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ ∩ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } )

Proof

Step Hyp Ref Expression
1 eleq2w ⊢ ( 𝑥 = 𝑦 → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑦 ) )
2 1 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑃 ∈ 𝑦 ) )
3 fnessex ⊢ ( ( 𝐴 Fne 𝐵 ∧ 𝑦 ∈ 𝐴 ∧ 𝑃 ∈ 𝑦 ) → ∃ 𝑧 ∈ 𝐵 ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
4 3 3expb ⊢ ( ( 𝐴 Fne 𝐵 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑃 ∈ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐵 ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) )
5 eleq2w ⊢ ( 𝑥 = 𝑧 → ( 𝑃 ∈ 𝑥 ↔ 𝑃 ∈ 𝑧 ) )
6 5 intminss ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑃 ∈ 𝑧 ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑧 )
7 sstr ⊢ ( ( ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 )
8 6 7 sylan ⊢ ( ( ( 𝑧 ∈ 𝐵 ∧ 𝑃 ∈ 𝑧 ) ∧ 𝑧 ⊆ 𝑦 ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 )
9 8 expl ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 ) )
10 9 rexlimiv ⊢ ( ∃ 𝑧 ∈ 𝐵 ( 𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦 ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 )
11 4 10 syl ⊢ ( ( 𝐴 Fne 𝐵 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑃 ∈ 𝑦 ) ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 )
12 11 ex ⊢ ( 𝐴 Fne 𝐵 → ( ( 𝑦 ∈ 𝐴 ∧ 𝑃 ∈ 𝑦 ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 ) )
13 2 12 biimtrid ⊢ ( 𝐴 Fne 𝐵 → ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 ) )
14 13 ralrimiv ⊢ ( 𝐴 Fne 𝐵 → ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 )
15 ssint ⊢ ( ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ ∩ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 )
16 14 15 sylibr ⊢ ( 𝐴 Fne 𝐵 → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ ∩ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } )