baspartn - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > baspartn		Structured version Visualization version Unicode version

Theorem baspartn 19962

Description: A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.)

**Assertion**
Ref	Expression
baspartn	$/\$ $\/$

(

)

**Proof of Theorem baspartn**
Step	Hyp	Ref	Expression
1		id 22	. . . . . . . . 9
2		pwidg 3963	. . . . . . . . 9
3	1, 2	elind 3617	. . . . . . . 8
4		elssuni 4226	. . . . . . . 8
5	3, 4	syl 17	. . . . . . 7
6		inidm 3640	. . . . . . . . 9
7		ineq2 3627	. . . . . . . . 9
8	6, 7	syl5eqr 2498	. . . . . . . 8
9	8	pweqd 3955	. . . . . . . . . 10
10	9	ineq2d 3633	. . . . . . . . 9
11	10	unieqd 4207	. . . . . . . 8
12	8, 11	sseq12d 3460	. . . . . . 7
13	5, 12	syl5ibcom 224	. . . . . 6
14		0ss 3762	. . . . . . . 8
15		sseq1 3452	. . . . . . . 8
16	14, 15	mpbiri 237	. . . . . . 7
17	16	a1i 11	. . . . . 6
18	13, 17	jaod 382	. . . . 5 $\/$
19	18	ralimdv 2797	. . . 4 $\/$
20	19	ralimia 2778	. . 3 $\/$
21	20	adantl 468	. 2 $/\$ $\/$
22		isbasisg 19955	. . 3
23	22	adantr 467	. 2 $/\$ $\/$
24	21, 23	mpbird 236	1 $/\$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371

wceq 1443

wcel 1886

wral 2736

cin 3402

wss 3403

c0 3730

cpw 3950

cuni 4197

ctb 19913

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ral 2741 df-rex 2742 df-v 3046 df-dif 3406 df-in 3410 df-ss 3417 df-nul 3731 df-pw 3952 df-uni 4198 df-bases 19915

This theorem is referenced by: kelac2lem 35916