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

Metamath Proof Explorer

Theorem fbasweak

Description: A filter base on any set is also a filter base on any larger set. (Contributed by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fbasweak ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐹 ∈ ( fBas ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐹 ⊆ 𝒫 𝑌 )
2 simp1 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
3 elfvdm ⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas )
4 3 3ad2ant1 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝑋 ∈ dom fBas )
5 isfbas ⊢ ( 𝑋 ∈ dom fBas → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
6 4 5 syl ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
7 2 6 mpbid ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) )
8 7 simprd ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) )
9 isfbas ⊢ ( 𝑌 ∈ 𝑉 → ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ↔ ( 𝐹 ⊆ 𝒫 𝑌 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
10 9 3ad2ant3 ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → ( 𝐹 ∈ ( fBas ‘ 𝑌 ) ↔ ( 𝐹 ⊆ 𝒫 𝑌 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝐹 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ≠ ∅ ) ) ) )
11 1 8 10 mpbir2and ⊢ ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝐹 ⊆ 𝒫 𝑌 ∧ 𝑌 ∈ 𝑉 ) → 𝐹 ∈ ( fBas ‘ 𝑌 ) )