Theorem fctop 7610

Description: The finite complement topology on a set A. Example 3 in [Munkres] p. 77. (Contributed by FL, 15-Aug-2006.)

Hypothesis

Ref	Expression
indistop.1	⊢ A ∈ V

Assertion

Ref	Expression
fctop	⊢ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ∈ Top

Distinct variable group:   x,n,A

Proof of Theorem fctop

Step	Hyp	Ref	Expression
1		indistop.1	. . . 4 ⊢ A ∈ V
2		abssexg 2743	. . . 4 ⊢ (A ∈ V → {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ∈ V)
3	1, 2	ax-mp 7	. . 3 ⊢ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ∈ V
4		istopg 7556	. . 3 ⊢ ({x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ∈ V → ({x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ∈ Top ↔ (∀y(y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → ∪y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}) ⋀ ∀y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}∀z ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} (y ∩ z) ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))})))
5	3, 4	ax-mp 7	. 2 ⊢ ({x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ∈ Top ↔ (∀y(y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → ∪y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}) ⋀ ∀y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}∀z ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} (y ∩ z) ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}))
6		uniss 2517	. . . . . 6 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → ∪y ⊆ ∪{x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))})
7		pm3.26 319	. . . . . . . . . . 11 ⊢ ((x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅)) → x ⊆ A)
8	7	a1i 8	. . . . . . . . . 10 ⊢ (x ∈ V → ((x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅)) → x ⊆ A))
9	8	ss2rabi 2125	. . . . . . . . 9 ⊢ {x ∈ V∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⊆ {x ∈ V∣x ⊆ A}
10		uniss 2517	. . . . . . . . 9 ⊢ ({x ∈ V∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⊆ {x ∈ V∣x ⊆ A} → ∪{x ∈ V∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⊆ ∪{x ∈ V∣x ⊆ A})
11	9, 10	ax-mp 7	. . . . . . . 8 ⊢ ∪{x ∈ V∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⊆ ∪{x ∈ V∣x ⊆ A}
12		rabab 1819	. . . . . . . . 9 ⊢ {x ∈ V∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} = {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}
13	12	unieqi 2507	. . . . . . . 8 ⊢ ∪{x ∈ V∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} = ∪{x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}
14		unimax 2528	. . . . . . . . 9 ⊢ (A ∈ V → ∪{x ∈ V∣x ⊆ A} = A)
15	1, 14	ax-mp 7	. . . . . . . 8 ⊢ ∪{x ∈ V∣x ⊆ A} = A
16	11, 13, 15	3sstr3 2096	. . . . . . 7 ⊢ ∪{x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⊆ A
17		sstr 2069	. . . . . . 7 ⊢ ((∪y ⊆ ∪{x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ ∪{x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⊆ A) → ∪y ⊆ A)
18	16, 17	mpan2 695	. . . . . 6 ⊢ (∪y ⊆ ∪{x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → ∪y ⊆ A)
19	6, 18	syl 10	. . . . 5 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → ∪y ⊆ A)
20		ssel2 2061	. . . . . . . . . . . . . . . 16 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ y) → z ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))})
21		visset 1810	. . . . . . . . . . . . . . . . 17 ⊢ z ∈ V
22		sseq1 2079	. . . . . . . . . . . . . . . . . 18 ⊢ (x = z → (x ⊆ A ↔ z ⊆ A))
23		difeq2 2151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (x = z → (A ∖ x) = (A ∖ z))
24	23	breq1d 2625	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = z → ((A ∖ x) ≈ n ↔ (A ∖ z) ≈ n))
25	24	rexbidv 1662	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = z → (∃n ∈ ω (A ∖ x) ≈ n ↔ ∃n ∈ ω (A ∖ z) ≈ n))
26		eqeq1 1479	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = z → (x = ∅ ↔ z = ∅))
27	25, 26	orbi12d 626	. . . . . . . . . . . . . . . . . 18 ⊢ (x = z → ((∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅) ↔ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅)))
28	22, 27	anbi12d 627	. . . . . . . . . . . . . . . . 17 ⊢ (x = z → ((x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅)) ↔ (z ⊆ A ⋀ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅))))
29	21, 28	elab 1894	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ↔ (z ⊆ A ⋀ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅)))
30	20, 29	sylib 198	. . . . . . . . . . . . . . 15 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ y) → (z ⊆ A ⋀ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅)))
31	30	pm3.27d 325	. . . . . . . . . . . . . 14 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ y) → (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅))
32	31	ord 232	. . . . . . . . . . . . 13 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ y) → (¬ ∃n ∈ ω (A ∖ z) ≈ n → z = ∅))
33	32	con1d 93	. . . . . . . . . . . 12 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ y) → (¬ z = ∅ → ∃n ∈ ω (A ∖ z) ≈ n))
34	33	imp 350	. . . . . . . . . . 11 ⊢ (((y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) → ∃n ∈ ω (A ∖ z) ≈ n)
35		ssfi 4524	. . . . . . . . . . . . . 14 ⊢ ((∃n ∈ ω (A ∖ z) ≈ n ⋀ (A ∖ ∪y) ⊆ (A ∖ z)) → ∃n ∈ ω (A ∖ ∪y) ≈ n)
36		elssuni 2522	. . . . . . . . . . . . . . 15 ⊢ (z ∈ y → z ⊆ ∪y)
37		sscon 2168	. . . . . . . . . . . . . . 15 ⊢ (z ⊆ ∪y → (A ∖ ∪y) ⊆ (A ∖ z))
38	36, 37	syl 10	. . . . . . . . . . . . . 14 ⊢ (z ∈ y → (A ∖ ∪y) ⊆ (A ∖ z))
39	35, 38	sylan2 451	. . . . . . . . . . . . 13 ⊢ ((∃n ∈ ω (A ∖ z) ≈ n ⋀ z ∈ y) → ∃n ∈ ω (A ∖ ∪y) ≈ n)
40	39	expcom 374	. . . . . . . . . . . 12 ⊢ (z ∈ y → (∃n ∈ ω (A ∖ z) ≈ n → ∃n ∈ ω (A ∖ ∪y) ≈ n))
41	40	ad2antlr 405	. . . . . . . . . . 11 ⊢ (((y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) → (∃n ∈ ω (A ∖ z) ≈ n → ∃n ∈ ω (A ∖ ∪y) ≈ n))
42	34, 41	mpd 26	. . . . . . . . . 10 ⊢ (((y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) → ∃n ∈ ω (A ∖ ∪y) ≈ n)
43	42	exp31 376	. . . . . . . . 9 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → (z ∈ y → (¬ z = ∅ → ∃n ∈ ω (A ∖ ∪y) ≈ n)))
44	43	r19.23adv 1744	. . . . . . . 8 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → (∃z ∈ y ¬ z = ∅ → ∃n ∈ ω (A ∖ ∪y) ≈ n))
45		uni0c 2520	. . . . . . . . . 10 ⊢ (∪y = ∅ ↔ ∀z ∈ y z = ∅)
46	45	negbii 187	. . . . . . . . 9 ⊢ (¬ ∪y = ∅ ↔ ¬ ∀z ∈ y z = ∅)
47		rexnal 1652	. . . . . . . . 9 ⊢ (∃z ∈ y ¬ z = ∅ ↔ ¬ ∀z ∈ y z = ∅)
48	46, 47	bitr4 176	. . . . . . . 8 ⊢ (¬ ∪y = ∅ ↔ ∃z ∈ y ¬ z = ∅)
49	44, 48	syl5ib 206	. . . . . . 7 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → (¬ ∪y = ∅ → ∃n ∈ ω (A ∖ ∪y) ≈ n))
50	49	con1d 93	. . . . . 6 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → (¬ ∃n ∈ ω (A ∖ ∪y) ≈ n → ∪y = ∅))
51	50	orrd 233	. . . . 5 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → (∃n ∈ ω (A ∖ ∪y) ≈ n ⋁ ∪y = ∅))
52	19, 51	jca 288	. . . 4 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → (∪y ⊆ A ⋀ (∃n ∈ ω (A ∖ ∪y) ≈ n ⋁ ∪y = ∅)))
53		visset 1810	. . . . . 6 ⊢ y ∈ V
54	53	uniex 2866	. . . . 5 ⊢ ∪y ∈ V
55		sseq1 2079	. . . . . 6 ⊢ (x = ∪y → (x ⊆ A ↔ ∪y ⊆ A))
56		difeq2 2151	. . . . . . . . 9 ⊢ (x = ∪y → (A ∖ x) = (A ∖ ∪y))
57	56	breq1d 2625	. . . . . . . 8 ⊢ (x = ∪y → ((A ∖ x) ≈ n ↔ (A ∖ ∪y) ≈ n))
58	57	rexbidv 1662	. . . . . . 7 ⊢ (x = ∪y → (∃n ∈ ω (A ∖ x) ≈ n ↔ ∃n ∈ ω (A ∖ ∪y) ≈ n))
59		eqeq1 1479	. . . . . . 7 ⊢ (x = ∪y → (x = ∅ ↔ ∪y = ∅))
60	58, 59	orbi12d 626	. . . . . 6 ⊢ (x = ∪y → ((∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅) ↔ (∃n ∈ ω (A ∖ ∪y) ≈ n ⋁ ∪y = ∅)))
61	55, 60	anbi12d 627	. . . . 5 ⊢ (x = ∪y → ((x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅)) ↔ (∪y ⊆ A ⋀ (∃n ∈ ω (A ∖ ∪y) ≈ n ⋁ ∪y = ∅))))
62	54, 61	elab 1894	. . . 4 ⊢ (∪y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ↔ (∪y ⊆ A ⋀ (∃n ∈ ω (A ∖ ∪y) ≈ n ⋁ ∪y = ∅)))
63	52, 62	sylibr 200	. . 3 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → ∪y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))})
64	63	ax-gen 962	. 2 ⊢ ∀y(y ⊆ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} → ∪y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))})
65		ssinss1 2234	. . . . . 6 ⊢ (y ⊆ A → (y ∩ z) ⊆ A)
66	65	ad2antrr 404	. . . . 5 ⊢ (((y ⊆ A ⋀ (∃n ∈ ω (A ∖ y) ≈ n ⋁ y = ∅)) ⋀ (z ⊆ A ⋀ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅))) → (y ∩ z) ⊆ A)
67		unfi 4537	. . . . . . . . 9 ⊢ ((∃n ∈ ω (A ∖ y) ≈ n ⋀ ∃n ∈ ω (A ∖ z) ≈ n) → ∃n ∈ ω ((A ∖ y) ∪ (A ∖ z)) ≈ n)
68		difindi 2256	. . . . . . . . . . 11 ⊢ (A ∖ (y ∩ z)) = ((A ∖ y) ∪ (A ∖ z))
69	68	breq1i 2622	. . . . . . . . . 10 ⊢ ((A ∖ (y ∩ z)) ≈ n ↔ ((A ∖ y) ∪ (A ∖ z)) ≈ n)
70	69	rexbii 1666	. . . . . . . . 9 ⊢ (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ↔ ∃n ∈ ω ((A ∖ y) ∪ (A ∖ z)) ≈ n)
71	67, 70	sylibr 200	. . . . . . . 8 ⊢ ((∃n ∈ ω (A ∖ y) ≈ n ⋀ ∃n ∈ ω (A ∖ z) ≈ n) → ∃n ∈ ω (A ∖ (y ∩ z)) ≈ n)
72	71	orcd 272	. . . . . . 7 ⊢ ((∃n ∈ ω (A ∖ y) ≈ n ⋀ ∃n ∈ ω (A ∖ z) ≈ n) → (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅))
73		ineq1 2207	. . . . . . . . 9 ⊢ (y = ∅ → (y ∩ z) = (∅ ∩ z))
74		incom 2205	. . . . . . . . . 10 ⊢ (∅ ∩ z) = (z ∩ ∅)
75		in0 2295	. . . . . . . . . 10 ⊢ (z ∩ ∅) = ∅
76	74, 75	eqtr 1493	. . . . . . . . 9 ⊢ (∅ ∩ z) = ∅
77	73, 76	syl6eq 1521	. . . . . . . 8 ⊢ (y = ∅ → (y ∩ z) = ∅)
78	77	olcd 273	. . . . . . 7 ⊢ (y = ∅ → (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅))
79		ineq2 2208	. . . . . . . . 9 ⊢ (z = ∅ → (y ∩ z) = (y ∩ ∅))
80		in0 2295	. . . . . . . . 9 ⊢ (y ∩ ∅) = ∅
81	79, 80	syl6eq 1521	. . . . . . . 8 ⊢ (z = ∅ → (y ∩ z) = ∅)
82	81	olcd 273	. . . . . . 7 ⊢ (z = ∅ → (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅))
83	72, 78, 82	ccase2 756	. . . . . 6 ⊢ (((∃n ∈ ω (A ∖ y) ≈ n ⋁ y = ∅) ⋀ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅)) → (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅))
84	83	ad2ant2l 408	. . . . 5 ⊢ (((y ⊆ A ⋀ (∃n ∈ ω (A ∖ y) ≈ n ⋁ y = ∅)) ⋀ (z ⊆ A ⋀ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅))) → (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅))
85	66, 84	jca 288	. . . 4 ⊢ (((y ⊆ A ⋀ (∃n ∈ ω (A ∖ y) ≈ n ⋁ y = ∅)) ⋀ (z ⊆ A ⋀ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅))) → ((y ∩ z) ⊆ A ⋀ (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅)))
86		sseq1 2079	. . . . . . 7 ⊢ (x = y → (x ⊆ A ↔ y ⊆ A))
87		difeq2 2151	. . . . . . . . . 10 ⊢ (x = y → (A ∖ x) = (A ∖ y))
88	87	breq1d 2625	. . . . . . . . 9 ⊢ (x = y → ((A ∖ x) ≈ n ↔ (A ∖ y) ≈ n))
89	88	rexbidv 1662	. . . . . . . 8 ⊢ (x = y → (∃n ∈ ω (A ∖ x) ≈ n ↔ ∃n ∈ ω (A ∖ y) ≈ n))
90		eqeq1 1479	. . . . . . . 8 ⊢ (x = y → (x = ∅ ↔ y = ∅))
91	89, 90	orbi12d 626	. . . . . . 7 ⊢ (x = y → ((∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅) ↔ (∃n ∈ ω (A ∖ y) ≈ n ⋁ y = ∅)))
92	86, 91	anbi12d 627	. . . . . 6 ⊢ (x = y → ((x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅)) ↔ (y ⊆ A ⋀ (∃n ∈ ω (A ∖ y) ≈ n ⋁ y = ∅))))
93	53, 92	elab 1894	. . . . 5 ⊢ (y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ↔ (y ⊆ A ⋀ (∃n ∈ ω (A ∖ y) ≈ n ⋁ y = ∅)))
94	93, 29	anbi12i 482	. . . 4 ⊢ ((y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}) ↔ ((y ⊆ A ⋀ (∃n ∈ ω (A ∖ y) ≈ n ⋁ y = ∅)) ⋀ (z ⊆ A ⋀ (∃n ∈ ω (A ∖ z) ≈ n ⋁ z = ∅))))
95	53	inex1 2712	. . . . 5 ⊢ (y ∩ z) ∈ V
96		sseq1 2079	. . . . . 6 ⊢ (x = (y ∩ z) → (x ⊆ A ↔ (y ∩ z) ⊆ A))
97		difeq2 2151	. . . . . . . 8 ⊢ (x = (y ∩ z) → (A ∖ x) = (A ∖ (y ∩ z)))
98		breq1 2618	. . . . . . . . 9 ⊢ ((A ∖ x) = (A ∖ (y ∩ z)) → ((A ∖ x) ≈ n ↔ (A ∖ (y ∩ z)) ≈ n))
99	98	rexbidv 1662	. . . . . . . 8 ⊢ ((A ∖ x) = (A ∖ (y ∩ z)) → (∃n ∈ ω (A ∖ x) ≈ n ↔ ∃n ∈ ω (A ∖ (y ∩ z)) ≈ n))
100	97, 99	syl 10	. . . . . . 7 ⊢ (x = (y ∩ z) → (∃n ∈ ω (A ∖ x) ≈ n ↔ ∃n ∈ ω (A ∖ (y ∩ z)) ≈ n))
101		eqeq1 1479	. . . . . . 7 ⊢ (x = (y ∩ z) → (x = ∅ ↔ (y ∩ z) = ∅))
102	100, 101	orbi12d 626	. . . . . 6 ⊢ (x = (y ∩ z) → ((∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅) ↔ (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅)))
103	96, 102	anbi12d 627	. . . . 5 ⊢ (x = (y ∩ z) → ((x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅)) ↔ ((y ∩ z) ⊆ A ⋀ (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅))))
104	95, 103	elab 1894	. . . 4 ⊢ ((y ∩ z) ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ↔ ((y ∩ z) ⊆ A ⋀ (∃n ∈ ω (A ∖ (y ∩ z)) ≈ n ⋁ (y ∩ z) = ∅)))
105	85, 94, 104	3imtr4 219	. . 3 ⊢ ((y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ⋀ z ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}) → (y ∩ z) ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))})
106	105	rgen2a 1697	. 2 ⊢ ∀y ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}∀z ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} (y ∩ z) ∈ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))}
107	5, 64, 106	mpbir2an 729	1 ⊢ {x∣(x ⊆ A ⋀ (∃n ∈ ω (A ∖ x) ≈ n ⋁ x = ∅))} ∈ Top

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 953   = wceq 955   ∈ wcel 957  {cab 1462  ∀wral 1643  ∃wrex 1644  {crab 1646  Vcvv 1808   ∖ cdif 2041   ∪ cun 2042   ∩ cin 2043   ⊆ wss 2044  ∅c0 2277  ∪cuni 2499   class class class wbr 2615  ωcom 3127   ≈ cen 4357  Topctop 7548

This theorem is referenced by:  fctop2 7611

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-rep 2689  ax-sep 2699  ax-nul 2706  ax-pow 2738  ax-pr 2775  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-ral 1647  df-rex 1648  df-reu 1649  df-rab 1650  df-v 1809  df-sbc 1939  df-csb 1999  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-pss 2052  df-nul 2278  df-if 2359  df-pw 2399  df-sn 2409  df-pr 2410  df-tp 2412  df-op 2413  df-uni 2500  df-int 2530  df-iun 2564  df-br 2616  df-opab 2663  df-tr 2677  df-eprel 2828  df-id 2831  df-po 2836  df-so 2846  df-fr 2913  df-we 2930  df-ord 2947  df-on 2948  df-lim 2949  df-suc 2950  df-om 3128  df-xp 3180  df-rel 3181  df-cnv 3182  df-co 3183  df-dm 3184  df-rn 3185  df-res 3186  df-ima 3187  df-fun 3188  df-fn 3189  df-f 3190  df-f1 3191  df-fo 3192  df-f1o 3193  df-fv 3194  df-rdg 3927  df-opr 3960  df-oprab 3961  df-oadd 4128  df-er 4254  df-en 4360  df-top 7552

Copyright terms: Public domain