Theorem isbasis3g

Description: Express the predicate "the set B is a basis for a topology". Definition of basis in Munkres p. 78. (Contributed by NM, 17-Jul-2006)

	Ref	Expression
Assertion	isbasis3g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isbasis2g	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
2		elssuni	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ⊆ ∪ 𝐵 )
3	2	rgen	⊢ ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵
4		eluni2	⊢ ( 𝑥 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
5	4	biimpi	⊢ ( 𝑥 ∈ ∪ 𝐵 → ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
6	5	rgen	⊢ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦
7	3 6	pm3.2i	⊢ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 )
8	7	biantrur	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
9		df-3an	⊢ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ↔ ( ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
10	8 9	bitr4i	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) )
11	1 10	bitrdi	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐵 ∈ TopBases ↔ ( ∀ 𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀ 𝑥 ∈ ∪ 𝐵 ∃ 𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ∃ 𝑤 ∈ 𝐵 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )