Theorem indistop 7598

Description: The indiscrete topology on a set A. Part of Example 2 in [Munkres] p. 77. (Contributed by FL, 16-Jul-2006.)

Hypothesis

Ref	Expression
indistop.1	⊢ A ∈ V

Assertion

Ref	Expression
indistop	⊢ {∅, A} ∈ Top

Proof of Theorem indistop

Step	Hyp	Ref	Expression
1		prex 2776	. . 3 ⊢ {∅, A} ∈ V
2		istopg 7546	. . 3 ⊢ ({∅, A} ∈ V → ({∅, A} ∈ Top ↔ (∀x(x ⊆ {∅, A} → ∪x ∈ {∅, A}) ⋀ ∀x ∈ {∅, A}∀y ∈ {∅, A} (x ∩ y) ∈ {∅, A})))
3	1, 2	ax-mp 7	. 2 ⊢ ({∅, A} ∈ Top ↔ (∀x(x ⊆ {∅, A} → ∪x ∈ {∅, A}) ⋀ ∀x ∈ {∅, A}∀y ∈ {∅, A} (x ∩ y) ∈ {∅, A}))
4		sspr 2471	. . . 4 ⊢ (x ⊆ {∅, A} ↔ ((x = ∅ ⋁ x = {∅}) ⋁ (x = {A} ⋁ x = {∅, A})))
5		unieq 2505	. . . . . . 7 ⊢ (x = ∅ → ∪x = ∪∅)
6		uni0 2520	. . . . . . . 8 ⊢ ∪∅ = ∅
7		0ex 2706	. . . . . . . . 9 ⊢ ∅ ∈ V
8	7	pri1 2446	. . . . . . . 8 ⊢ ∅ ∈ {∅, A}
9	6, 8	eqeltr 1541	. . . . . . 7 ⊢ ∪∅ ∈ {∅, A}
10	5, 9	syl6eqel 1553	. . . . . 6 ⊢ (x = ∅ → ∪x ∈ {∅, A})
11		unieq 2505	. . . . . . 7 ⊢ (x = {∅} → ∪x = ∪{∅})
12	8	a1i 8	. . . . . . . 8 ⊢ (x = {∅} → ∅ ∈ {∅, A})
13	7	unisn 2512	. . . . . . . 8 ⊢ ∪{∅} = ∅
14	12, 13	syl5eqel 1549	. . . . . . 7 ⊢ (x = {∅} → ∪{∅} ∈ {∅, A})
15	11, 14	eqeltrd 1545	. . . . . 6 ⊢ (x = {∅} → ∪x ∈ {∅, A})
16	10, 15	jaoi 341	. . . . 5 ⊢ ((x = ∅ ⋁ x = {∅}) → ∪x ∈ {∅, A})
17		unieq 2505	. . . . . . 7 ⊢ (x = {A} → ∪x = ∪{A})
18		indistop.1	. . . . . . . . . 10 ⊢ A ∈ V
19	18	pri2 2447	. . . . . . . . 9 ⊢ A ∈ {∅, A}
20	19	a1i 8	. . . . . . . 8 ⊢ (x = {A} → A ∈ {∅, A})
21	18	unisn 2512	. . . . . . . 8 ⊢ ∪{A} = A
22	20, 21	syl5eqel 1549	. . . . . . 7 ⊢ (x = {A} → ∪{A} ∈ {∅, A})
23	17, 22	eqeltrd 1545	. . . . . 6 ⊢ (x = {A} → ∪x ∈ {∅, A})
24		unieq 2505	. . . . . . 7 ⊢ (x = {∅, A} → ∪x = ∪{∅, A})
25		uncom 2172	. . . . . . . . . 10 ⊢ (A ∪ ∅) = (∅ ∪ A)
26		un0 2293	. . . . . . . . . . 11 ⊢ (A ∪ ∅) = A
27	26, 19	eqeltr 1541	. . . . . . . . . 10 ⊢ (A ∪ ∅) ∈ {∅, A}
28	25, 27	eqeltrr 1542	. . . . . . . . 9 ⊢ (∅ ∪ A) ∈ {∅, A}
29	28	a1i 8	. . . . . . . 8 ⊢ (x = {∅, A} → (∅ ∪ A) ∈ {∅, A})
30	7, 18	unipr 2510	. . . . . . . 8 ⊢ ∪{∅, A} = (∅ ∪ A)
31	29, 30	syl5eqel 1549	. . . . . . 7 ⊢ (x = {∅, A} → ∪{∅, A} ∈ {∅, A})
32	24, 31	eqeltrd 1545	. . . . . 6 ⊢ (x = {∅, A} → ∪x ∈ {∅, A})
33	23, 32	jaoi 341	. . . . 5 ⊢ ((x = {A} ⋁ x = {∅, A}) → ∪x ∈ {∅, A})
34	16, 33	jaoi 341	. . . 4 ⊢ (((x = ∅ ⋁ x = {∅}) ⋁ (x = {A} ⋁ x = {∅, A})) → ∪x ∈ {∅, A})
35	4, 34	sylbi 199	. . 3 ⊢ (x ⊆ {∅, A} → ∪x ∈ {∅, A})
36	35	ax-gen 961	. 2 ⊢ ∀x(x ⊆ {∅, A} → ∪x ∈ {∅, A})
37		pm3.26 319	. . . . . . . . . . . . 13 ⊢ ((y = ∅ ⋀ x = ∅) → y = ∅)
38	37	ineq2d 2213	. . . . . . . . . . . 12 ⊢ ((y = ∅ ⋀ x = ∅) → (x ∩ y) = (x ∩ ∅))
39		in0 2294	. . . . . . . . . . . 12 ⊢ (x ∩ ∅) = ∅
40	38, 39	syl6eq 1520	. . . . . . . . . . 11 ⊢ ((y = ∅ ⋀ x = ∅) → (x ∩ y) = ∅)
41	40, 8	syl6eqel 1553	. . . . . . . . . 10 ⊢ ((y = ∅ ⋀ x = ∅) → (x ∩ y) ∈ {∅, A})
42	41	ex 373	. . . . . . . . 9 ⊢ (y = ∅ → (x = ∅ → (x ∩ y) ∈ {∅, A}))
43		pm3.27 323	. . . . . . . . . . . . 13 ⊢ ((y = A ⋀ x = ∅) → x = ∅)
44	43	ineq1d 2212	. . . . . . . . . . . 12 ⊢ ((y = A ⋀ x = ∅) → (x ∩ y) = (∅ ∩ y))
45		incom 2204	. . . . . . . . . . . . 13 ⊢ (∅ ∩ y) = (y ∩ ∅)
46		in0 2294	. . . . . . . . . . . . 13 ⊢ (y ∩ ∅) = ∅
47	45, 46	eqtr 1492	. . . . . . . . . . . 12 ⊢ (∅ ∩ y) = ∅
48	44, 47	syl6eq 1520	. . . . . . . . . . 11 ⊢ ((y = A ⋀ x = ∅) → (x ∩ y) = ∅)
49	48, 8	syl6eqel 1553	. . . . . . . . . 10 ⊢ ((y = A ⋀ x = ∅) → (x ∩ y) ∈ {∅, A})
50	49	ex 373	. . . . . . . . 9 ⊢ (y = A → (x = ∅ → (x ∩ y) ∈ {∅, A}))
51	42, 50	jaoi 341	. . . . . . . 8 ⊢ ((y = ∅ ⋁ y = A) → (x = ∅ → (x ∩ y) ∈ {∅, A}))
52	51	com12 11	. . . . . . 7 ⊢ (x = ∅ → ((y = ∅ ⋁ y = A) → (x ∩ y) ∈ {∅, A}))
53		ineq12 2208	. . . . . . . . . . . . 13 ⊢ ((x = A ⋀ y = ∅) → (x ∩ y) = (A ∩ ∅))
54	53	ancoms 436	. . . . . . . . . . . 12 ⊢ ((y = ∅ ⋀ x = A) → (x ∩ y) = (A ∩ ∅))
55		in0 2294	. . . . . . . . . . . 12 ⊢ (A ∩ ∅) = ∅
56	54, 55	syl6eq 1520	. . . . . . . . . . 11 ⊢ ((y = ∅ ⋀ x = A) → (x ∩ y) = ∅)
57	56, 8	syl6eqel 1553	. . . . . . . . . 10 ⊢ ((y = ∅ ⋀ x = A) → (x ∩ y) ∈ {∅, A})
58	57	ex 373	. . . . . . . . 9 ⊢ (y = ∅ → (x = A → (x ∩ y) ∈ {∅, A}))
59		ineq12 2208	. . . . . . . . . . . . 13 ⊢ ((x = A ⋀ y = A) → (x ∩ y) = (A ∩ A))
60	59	ancoms 436	. . . . . . . . . . . 12 ⊢ ((y = A ⋀ x = A) → (x ∩ y) = (A ∩ A))
61		inidm 2218	. . . . . . . . . . . 12 ⊢ (A ∩ A) = A
62	60, 61	syl6eq 1520	. . . . . . . . . . 11 ⊢ ((y = A ⋀ x = A) → (x ∩ y) = A)
63	62, 19	syl6eqel 1553	. . . . . . . . . 10 ⊢ ((y = A ⋀ x = A) → (x ∩ y) ∈ {∅, A})
64	63	ex 373	. . . . . . . . 9 ⊢ (y = A → (x = A → (x ∩ y) ∈ {∅, A}))
65	58, 64	jaoi 341	. . . . . . . 8 ⊢ ((y = ∅ ⋁ y = A) → (x = A → (x ∩ y) ∈ {∅, A}))
66	65	com12 11	. . . . . . 7 ⊢ (x = A → ((y = ∅ ⋁ y = A) → (x ∩ y) ∈ {∅, A}))
67	52, 66	jaoi 341	. . . . . 6 ⊢ ((x = ∅ ⋁ x = A) → ((y = ∅ ⋁ y = A) → (x ∩ y) ∈ {∅, A}))
68		visset 1809	. . . . . . 7 ⊢ y ∈ V
69	68	elpr 2420	. . . . . 6 ⊢ (y ∈ {∅, A} ↔ (y = ∅ ⋁ y = A))
70	67, 69	syl5ib 206	. . . . 5 ⊢ ((x = ∅ ⋁ x = A) → (y ∈ {∅, A} → (x ∩ y) ∈ {∅, A}))
71	70	19.21aiv 1284	. . . 4 ⊢ ((x = ∅ ⋁ x = A) → ∀y(y ∈ {∅, A} → (x ∩ y) ∈ {∅, A}))
72		visset 1809	. . . . 5 ⊢ x ∈ V
73	72	elpr 2420	. . . 4 ⊢ (x ∈ {∅, A} ↔ (x = ∅ ⋁ x = A))
74		df-ral 1646	. . . 4 ⊢ (∀y ∈ {∅, A} (x ∩ y) ∈ {∅, A} ↔ ∀y(y ∈ {∅, A} → (x ∩ y) ∈ {∅, A}))
75	71, 73, 74	3imtr4 219	. . 3 ⊢ (x ∈ {∅, A} → ∀y ∈ {∅, A} (x ∩ y) ∈ {∅, A})
76	75	rgen 1695	. 2 ⊢ ∀x ∈ {∅, A}∀y ∈ {∅, A} (x ∩ y) ∈ {∅, A}
77	3, 36, 76	mpbir2an 729	1 ⊢ {∅, A} ∈ Top

Syntax hints:   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∀wral 1642  Vcvv 1807   ∪ cun 2041   ∩ cin 2042   ⊆ wss 2043  ∅c0 2276  {csn 2405  {cpr 2406  ∪cuni 2498  Topctop 7538

This theorem is referenced by:  indistps 7603  mapudiscn 10435

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-v 1808  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-uni 2499  df-top 7542

Copyright terms: Public domain