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	syl5bi	⊢ ( 𝐴 Fne 𝐵 → ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 ) )
14	13	ralrimiv	⊢ ( 𝐴 Fne 𝐵 → ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 )
15		ssint	⊢ ( ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ ∩ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ 𝑦 )
16	14 15	sylibr	⊢ ( 𝐴 Fne 𝐵 → ∩ { 𝑥 ∈ 𝐵 ∣ 𝑃 ∈ 𝑥 } ⊆ ∩ { 𝑥 ∈ 𝐴 ∣ 𝑃 ∈ 𝑥 } )