Theorem isbasis2g 7569

Description: Express the predicate "B is a basis for a topology."

Assertion

Ref	Expression
isbasis2g	|- (B e. C -> (B e. Bases <-> A.x e. B A.y e. B A.z e. (x i^i y)E.w e. B (z e. w /\ w (_ (x i^i y))))

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

Proof of Theorem isbasis2g

Step	Hyp	Ref	Expression
1		isbasisg 7568	. 2 |- (B e. C -> (B e. Bases <-> A.x e. B A.y e. B (x i^i y) (_ U.(B i^i P~(x i^i y))))
2		dfss3 2057	. . . 4 |- ((x i^i y) (_ U.(B i^i P~(x i^i y)) <-> A.z e. (x i^i y)z e. U.(B i^i P~(x i^i y)))
3		elin 2205	. . . . . . . . . 10 |- (w e. (B i^i P~(x i^i y)) <-> (w e. B /\ w e. P~(x i^i y)))
4		df-pw 2400	. . . . . . . . . . . 12 |- P~(x i^i y) = {w | w (_ (x i^i y)}
5	4	abeq2i 1569	. . . . . . . . . . 11 |- (w e. P~(x i^i y) <-> w (_ (x i^i y))
6	5	anbi2i 480	. . . . . . . . . 10 |- ((w e. B /\ w e. P~(x i^i y)) <-> (w e. B /\ w (_ (x i^i y)))
7	3, 6	bitr 173	. . . . . . . . 9 |- (w e. (B i^i P~(x i^i y)) <-> (w e. B /\ w (_ (x i^i y)))
8	7	anbi2i 480	. . . . . . . 8 |- ((z e. w /\ w e. (B i^i P~(x i^i y))) <-> (z e. w /\ (w e. B /\ w (_ (x i^i y))))
9		an12 484	. . . . . . . 8 |- ((z e. w /\ (w e. B /\ w (_ (x i^i y))) <-> (w e. B /\ (z e. w /\ w (_ (x i^i y))))
10	8, 9	bitr 173	. . . . . . 7 |- ((z e. w /\ w e. (B i^i P~(x i^i y))) <-> (w e. B /\ (z e. w /\ w (_ (x i^i y))))
11	10	exbii 1051	. . . . . 6 |- (E.w(z e. w /\ w e. (B i^i P~(x i^i y))) <-> E.w(w e. B /\ (z e. w /\ w (_ (x i^i y))))
12		eluni 2504	. . . . . 6 |- (z e. U.(B i^i P~(x i^i y)) <-> E.w(z e. w /\ w e. (B i^i P~(x i^i y))))
13		df-rex 1649	. . . . . 6 |- (E.w e. B (z e. w /\ w (_ (x i^i y)) <-> E.w(w e. B /\ (z e. w /\ w (_ (x i^i y))))
14	11, 12, 13	3bitr4 183	. . . . 5 |- (z e. U.(B i^i P~(x i^i y)) <-> E.w e. B (z e. w /\ w (_ (x i^i y)))
15	14	ralbii 1666	. . . 4 |- (A.z e. (x i^i y)z e. U.(B i^i P~(x i^i y)) <-> A.z e. (x i^i y)E.w e. B (z e. w /\ w (_ (x i^i y)))
16	2, 15	bitr 173	. . 3 |- ((x i^i y) (_ U.(B i^i P~(x i^i y)) <-> A.z e. (x i^i y)E.w e. B (z e. w /\ w (_ (x i^i y)))
17	16	2ralbii 1668	. 2 |- (A.x e. B A.y e. B (x i^i y) (_ U.(B i^i P~(x i^i y)) <-> A.x e. B A.y e. B A.z e. (x i^i y)E.w e. B (z e. w /\ w (_ (x i^i y)))
18	1, 17	syl6bb 536	1 |- (B e. C -> (B e. Bases <-> A.x e. B A.y e. B A.z e. (x i^i y)E.w e. B (z e. w /\ w (_ (x i^i y))))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   e. wcel 958  E.wex 980  A.wral 1644  E.wrex 1645   i^i cin 2044   (_ wss 2045  P~cpw 2399  U.cuni 2501  Basesctb 7547

This theorem is referenced by:  isbasis3g 7570  basis2t 7572  topbast 7584  basgen2t 7596  subbas 7601  retopbas 7612

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-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1648  df-rex 1649  df-v 1810  df-in 2049  df-ss 2051  df-pw 2400  df-uni 2502  df-bases 7551

Copyright terms: Public domain