Theorem isbasis3g 7613

Description: Express the predicate "B is a basis for a topology." Definition of basis in [Munkres] p. 78.

Assertion

Ref	Expression
isbasis3g	⊢ (B ∈ C → (B ∈ Bases ↔ (∀x ∈ B x ⊆ ∪B ⋀ ∀x ∈ ∪B∃y ∈ B x ∈ y ⋀ ∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y)))))

Distinct variable group:   x,w,y,z,B

Proof of Theorem isbasis3g

Step	Hyp	Ref	Expression
1		isbasis2g 7612	. 2 ⊢ (B ∈ C → (B ∈ Bases ↔ ∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y))))
2		elssuni 2526	. . . . . 6 ⊢ (x ∈ B → x ⊆ ∪B)
3	2	rgen 1698	. . . . 5 ⊢ ∀x ∈ B x ⊆ ∪B
4		eluni2 2507	. . . . . . 7 ⊢ (x ∈ ∪B ↔ ∃y ∈ B x ∈ y)
5	4	biimp 151	. . . . . 6 ⊢ (x ∈ ∪B → ∃y ∈ B x ∈ y)
6	5	rgen 1698	. . . . 5 ⊢ ∀x ∈ ∪B∃y ∈ B x ∈ y
7	3, 6	pm3.2i 285	. . . 4 ⊢ (∀x ∈ B x ⊆ ∪B ⋀ ∀x ∈ ∪B∃y ∈ B x ∈ y)
8	7	biantrur 725	. . 3 ⊢ (∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y)) ↔ ((∀x ∈ B x ⊆ ∪B ⋀ ∀x ∈ ∪B∃y ∈ B x ∈ y) ⋀ ∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y))))
9		df-3an 777	. . 3 ⊢ ((∀x ∈ B x ⊆ ∪B ⋀ ∀x ∈ ∪B∃y ∈ B x ∈ y ⋀ ∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y))) ↔ ((∀x ∈ B x ⊆ ∪B ⋀ ∀x ∈ ∪B∃y ∈ B x ∈ y) ⋀ ∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y))))
10	8, 9	bitr4 176	. 2 ⊢ (∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y)) ↔ (∀x ∈ B x ⊆ ∪B ⋀ ∀x ∈ ∪B∃y ∈ B x ∈ y ⋀ ∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y))))
11	1, 10	syl6bb 536	1 ⊢ (B ∈ C → (B ∈ Bases ↔ (∀x ∈ B x ⊆ ∪B ⋀ ∀x ∈ ∪B∃y ∈ B x ∈ y ⋀ ∀x ∈ B ∀y ∈ B ∀z ∈ (x ∩ y)∃w ∈ B (z ∈ w ⋀ w ⊆ (x ∩ y)))))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 775   ∈ wcel 958  ∀wral 1645  ∃wrex 1646   ∩ cin 2046   ⊆ wss 2047  ∪cuni 2503  Basesctb 7590

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-rex 1650  df-v 1812  df-in 2051  df-ss 2053  df-pw 2402  df-uni 2504  df-bases 7594

Copyright terms: Public domain