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 ‘ 𝑌 ) )