Theorem cctop 7594

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

Hypothesis

Ref	Expression
indistop.1	⊢ A ∈ V

Assertion

Ref	Expression
cctop	⊢ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ∈ Top

Distinct variable group:   x,A

Proof of Theorem cctop

Step	Hyp	Ref	Expression
1		indistop.1	. . . 4 ⊢ A ∈ V
2		abssexg 2737	. . . 4 ⊢ (A ∈ V → {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ∈ V)
3	1, 2	ax-mp 7	. . 3 ⊢ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ∈ V
4		istopg 7538	. . 3 ⊢ ({x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ∈ V → ({x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ∈ Top ↔ (∀y(y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → ∪y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}) ⋀ ∀y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}∀z ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} (y ∩ z) ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))})))
5	3, 4	ax-mp 7	. 2 ⊢ ({x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ∈ Top ↔ (∀y(y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → ∪y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}) ⋀ ∀y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}∀z ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} (y ∩ z) ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}))
6		uniss 2511	. . . . . 6 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → ∪y ⊆ ∪{x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))})
7		pm3.26 319	. . . . . . . . . . 11 ⊢ ((x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅)) → x ⊆ A)
8	7	a1i 8	. . . . . . . . . 10 ⊢ (x ∈ V → ((x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅)) → x ⊆ A))
9	8	ss2rabi 2118	. . . . . . . . 9 ⊢ {x ∈ V∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⊆ {x ∈ V∣x ⊆ A}
10		uniss 2511	. . . . . . . . 9 ⊢ ({x ∈ V∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⊆ {x ∈ V∣x ⊆ A} → ∪{x ∈ V∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⊆ ∪{x ∈ V∣x ⊆ A})
11	9, 10	ax-mp 7	. . . . . . . 8 ⊢ ∪{x ∈ V∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⊆ ∪{x ∈ V∣x ⊆ A}
12		rabab 1813	. . . . . . . . 9 ⊢ {x ∈ V∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} = {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}
13	12	unieqi 2501	. . . . . . . 8 ⊢ ∪{x ∈ V∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} = ∪{x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}
14		unimax 2522	. . . . . . . . 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 2089	. . . . . . 7 ⊢ ∪{x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⊆ A
17		sstr 2062	. . . . . . 7 ⊢ ((∪y ⊆ ∪{x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ ∪{x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⊆ A) → ∪y ⊆ A)
18	16, 17	mpan2 694	. . . . . 6 ⊢ (∪y ⊆ ∪{x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → ∪y ⊆ A)
19	6, 18	syl 10	. . . . 5 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → ∪y ⊆ A)
20		ssel2 2054	. . . . . . . . . . . . . . . 16 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) → z ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))})
21		visset 1804	. . . . . . . . . . . . . . . . 17 ⊢ z ∈ V
22		sseq1 2072	. . . . . . . . . . . . . . . . . 18 ⊢ (x = z → (x ⊆ A ↔ z ⊆ A))
23		difeq2 2144	. . . . . . . . . . . . . . . . . . . 20 ⊢ (x = z → (A ∖ x) = (A ∖ z))
24	23	breq1d 2619	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = z → ((A ∖ x) ≼ ω ↔ (A ∖ z) ≼ ω))
25		eqeq1 1473	. . . . . . . . . . . . . . . . . . 19 ⊢ (x = z → (x = ∅ ↔ z = ∅))
26	24, 25	orbi12d 625	. . . . . . . . . . . . . . . . . 18 ⊢ (x = z → (((A ∖ x) ≼ ω ⋁ x = ∅) ↔ ((A ∖ z) ≼ ω ⋁ z = ∅)))
27	22, 26	anbi12d 626	. . . . . . . . . . . . . . . . 17 ⊢ (x = z → ((x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅)) ↔ (z ⊆ A ⋀ ((A ∖ z) ≼ ω ⋁ z = ∅))))
28	21, 27	elab 1888	. . . . . . . . . . . . . . . 16 ⊢ (z ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ↔ (z ⊆ A ⋀ ((A ∖ z) ≼ ω ⋁ z = ∅)))
29	20, 28	sylib 198	. . . . . . . . . . . . . . 15 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) → (z ⊆ A ⋀ ((A ∖ z) ≼ ω ⋁ z = ∅)))
30	29	pm3.27d 325	. . . . . . . . . . . . . 14 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) → ((A ∖ z) ≼ ω ⋁ z = ∅))
31	30	ord 232	. . . . . . . . . . . . 13 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) → (¬ (A ∖ z) ≼ ω → z = ∅))
32	31	con1d 93	. . . . . . . . . . . 12 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) → (¬ z = ∅ → (A ∖ z) ≼ ω))
33	32	imp 350	. . . . . . . . . . 11 ⊢ (((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) → (A ∖ z) ≼ ω)
34		domtr 4396	. . . . . . . . . . . 12 ⊢ (((A ∖ ∪y) ≼ (A ∖ z) ⋀ (A ∖ z) ≼ ω) → (A ∖ ∪y) ≼ ω)
35		pm3.27 323	. . . . . . . . . . . . . . 15 ⊢ ((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) → z ∈ y)
36	35	ad2antrr 404	. . . . . . . . . . . . . 14 ⊢ ((((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) ⋀ (A ∖ z) ≼ ω) → z ∈ y)
37		elssuni 2516	. . . . . . . . . . . . . 14 ⊢ (z ∈ y → z ⊆ ∪y)
38	36, 37	syl 10	. . . . . . . . . . . . 13 ⊢ ((((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) ⋀ (A ∖ z) ≼ ω) → z ⊆ ∪y)
39		sscon 2161	. . . . . . . . . . . . 13 ⊢ (z ⊆ ∪y → (A ∖ ∪y) ⊆ (A ∖ z))
40		difexg 2712	. . . . . . . . . . . . . . 15 ⊢ (A ∈ V → (A ∖ z) ∈ V)
41	1, 40	ax-mp 7	. . . . . . . . . . . . . 14 ⊢ (A ∖ z) ∈ V
42		ssdom2g 4390	. . . . . . . . . . . . . 14 ⊢ ((A ∖ z) ∈ V → ((A ∖ ∪y) ⊆ (A ∖ z) → (A ∖ ∪y) ≼ (A ∖ z)))
43	41, 42	ax-mp 7	. . . . . . . . . . . . 13 ⊢ ((A ∖ ∪y) ⊆ (A ∖ z) → (A ∖ ∪y) ≼ (A ∖ z))
44	38, 39, 43	3syl 20	. . . . . . . . . . . 12 ⊢ ((((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) ⋀ (A ∖ z) ≼ ω) → (A ∖ ∪y) ≼ (A ∖ z))
45		pm3.27 323	. . . . . . . . . . . 12 ⊢ ((((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) ⋀ (A ∖ z) ≼ ω) → (A ∖ z) ≼ ω)
46	34, 44, 45	sylanc 471	. . . . . . . . . . 11 ⊢ ((((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) ⋀ (A ∖ z) ≼ ω) → (A ∖ ∪y) ≼ ω)
47	33, 46	mpdan 702	. . . . . . . . . 10 ⊢ (((y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ y) ⋀ ¬ z = ∅) → (A ∖ ∪y) ≼ ω)
48	47	exp31 376	. . . . . . . . 9 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → (z ∈ y → (¬ z = ∅ → (A ∖ ∪y) ≼ ω)))
49	48	r19.23adv 1738	. . . . . . . 8 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → (∃z ∈ y ¬ z = ∅ → (A ∖ ∪y) ≼ ω))
50		uni0b 2513	. . . . . . . . . . 11 ⊢ (∪y = ∅ ↔ y ⊆ {∅})
51		dfss3 2049	. . . . . . . . . . 11 ⊢ (y ⊆ {∅} ↔ ∀z ∈ y z ∈ {∅})
52		elsn 2411	. . . . . . . . . . . 12 ⊢ (z ∈ {∅} ↔ z = ∅)
53	52	ralbii 1659	. . . . . . . . . . 11 ⊢ (∀z ∈ y z ∈ {∅} ↔ ∀z ∈ y z = ∅)
54	50, 51, 53	3bitr 177	. . . . . . . . . 10 ⊢ (∪y = ∅ ↔ ∀z ∈ y z = ∅)
55	54	negbii 187	. . . . . . . . 9 ⊢ (¬ ∪y = ∅ ↔ ¬ ∀z ∈ y z = ∅)
56		rexnal 1646	. . . . . . . . 9 ⊢ (∃z ∈ y ¬ z = ∅ ↔ ¬ ∀z ∈ y z = ∅)
57	55, 56	bitr4 176	. . . . . . . 8 ⊢ (¬ ∪y = ∅ ↔ ∃z ∈ y ¬ z = ∅)
58	49, 57	syl5ib 206	. . . . . . 7 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → (¬ ∪y = ∅ → (A ∖ ∪y) ≼ ω))
59	58	con1d 93	. . . . . 6 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → (¬ (A ∖ ∪y) ≼ ω → ∪y = ∅))
60	59	orrd 233	. . . . 5 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → ((A ∖ ∪y) ≼ ω ⋁ ∪y = ∅))
61	19, 60	jca 288	. . . 4 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → (∪y ⊆ A ⋀ ((A ∖ ∪y) ≼ ω ⋁ ∪y = ∅)))
62		visset 1804	. . . . . 6 ⊢ y ∈ V
63	62	uniex 2861	. . . . 5 ⊢ ∪y ∈ V
64		sseq1 2072	. . . . . 6 ⊢ (x = ∪y → (x ⊆ A ↔ ∪y ⊆ A))
65		difeq2 2144	. . . . . . . 8 ⊢ (x = ∪y → (A ∖ x) = (A ∖ ∪y))
66	65	breq1d 2619	. . . . . . 7 ⊢ (x = ∪y → ((A ∖ x) ≼ ω ↔ (A ∖ ∪y) ≼ ω))
67		eqeq1 1473	. . . . . . 7 ⊢ (x = ∪y → (x = ∅ ↔ ∪y = ∅))
68	66, 67	orbi12d 625	. . . . . 6 ⊢ (x = ∪y → (((A ∖ x) ≼ ω ⋁ x = ∅) ↔ ((A ∖ ∪y) ≼ ω ⋁ ∪y = ∅)))
69	64, 68	anbi12d 626	. . . . 5 ⊢ (x = ∪y → ((x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅)) ↔ (∪y ⊆ A ⋀ ((A ∖ ∪y) ≼ ω ⋁ ∪y = ∅))))
70	63, 69	elab 1888	. . . 4 ⊢ (∪y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ↔ (∪y ⊆ A ⋀ ((A ∖ ∪y) ≼ ω ⋁ ∪y = ∅)))
71	61, 70	sylibr 200	. . 3 ⊢ (y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → ∪y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))})
72	71	ax-gen 960	. 2 ⊢ ∀y(y ⊆ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} → ∪y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))})
73		ssinss1 2227	. . . . . 6 ⊢ (y ⊆ A → (y ∩ z) ⊆ A)
74	73	ad2antrr 404	. . . . 5 ⊢ (((y ⊆ A ⋀ ((A ∖ y) ≼ ω ⋁ y = ∅)) ⋀ (z ⊆ A ⋀ ((A ∖ z) ≼ ω ⋁ z = ∅))) → (y ∩ z) ⊆ A)
75		unctb 7519	. . . . . . . . 9 ⊢ (((A ∖ y) ≼ ω ⋀ (A ∖ z) ≼ ω) → ((A ∖ y) ∪ (A ∖ z)) ≼ ω)
76		difindi 2249	. . . . . . . . 9 ⊢ (A ∖ (y ∩ z)) = ((A ∖ y) ∪ (A ∖ z))
77	75, 76	syl5eqbr 2638	. . . . . . . 8 ⊢ (((A ∖ y) ≼ ω ⋀ (A ∖ z) ≼ ω) → (A ∖ (y ∩ z)) ≼ ω)
78	77	orcd 272	. . . . . . 7 ⊢ (((A ∖ y) ≼ ω ⋀ (A ∖ z) ≼ ω) → ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅))
79		ineq1 2200	. . . . . . . . 9 ⊢ (y = ∅ → (y ∩ z) = (∅ ∩ z))
80		incom 2198	. . . . . . . . . 10 ⊢ (∅ ∩ z) = (z ∩ ∅)
81		in0 2288	. . . . . . . . . 10 ⊢ (z ∩ ∅) = ∅
82	80, 81	eqtr 1487	. . . . . . . . 9 ⊢ (∅ ∩ z) = ∅
83	79, 82	syl6eq 1515	. . . . . . . 8 ⊢ (y = ∅ → (y ∩ z) = ∅)
84	83	olcd 273	. . . . . . 7 ⊢ (y = ∅ → ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅))
85		ineq2 2201	. . . . . . . . 9 ⊢ (z = ∅ → (y ∩ z) = (y ∩ ∅))
86		in0 2288	. . . . . . . . 9 ⊢ (y ∩ ∅) = ∅
87	85, 86	syl6eq 1515	. . . . . . . 8 ⊢ (z = ∅ → (y ∩ z) = ∅)
88	87	olcd 273	. . . . . . 7 ⊢ (z = ∅ → ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅))
89	78, 84, 88	ccase2 755	. . . . . 6 ⊢ ((((A ∖ y) ≼ ω ⋁ y = ∅) ⋀ ((A ∖ z) ≼ ω ⋁ z = ∅)) → ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅))
90	89	ad2ant2l 408	. . . . 5 ⊢ (((y ⊆ A ⋀ ((A ∖ y) ≼ ω ⋁ y = ∅)) ⋀ (z ⊆ A ⋀ ((A ∖ z) ≼ ω ⋁ z = ∅))) → ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅))
91	74, 90	jca 288	. . . 4 ⊢ (((y ⊆ A ⋀ ((A ∖ y) ≼ ω ⋁ y = ∅)) ⋀ (z ⊆ A ⋀ ((A ∖ z) ≼ ω ⋁ z = ∅))) → ((y ∩ z) ⊆ A ⋀ ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅)))
92		sseq1 2072	. . . . . . 7 ⊢ (x = y → (x ⊆ A ↔ y ⊆ A))
93		difeq2 2144	. . . . . . . . 9 ⊢ (x = y → (A ∖ x) = (A ∖ y))
94	93	breq1d 2619	. . . . . . . 8 ⊢ (x = y → ((A ∖ x) ≼ ω ↔ (A ∖ y) ≼ ω))
95		eqeq1 1473	. . . . . . . 8 ⊢ (x = y → (x = ∅ ↔ y = ∅))
96	94, 95	orbi12d 625	. . . . . . 7 ⊢ (x = y → (((A ∖ x) ≼ ω ⋁ x = ∅) ↔ ((A ∖ y) ≼ ω ⋁ y = ∅)))
97	92, 96	anbi12d 626	. . . . . 6 ⊢ (x = y → ((x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅)) ↔ (y ⊆ A ⋀ ((A ∖ y) ≼ ω ⋁ y = ∅))))
98	62, 97	elab 1888	. . . . 5 ⊢ (y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ↔ (y ⊆ A ⋀ ((A ∖ y) ≼ ω ⋁ y = ∅)))
99	98, 28	anbi12i 481	. . . 4 ⊢ ((y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}) ↔ ((y ⊆ A ⋀ ((A ∖ y) ≼ ω ⋁ y = ∅)) ⋀ (z ⊆ A ⋀ ((A ∖ z) ≼ ω ⋁ z = ∅))))
100	62	inex1 2706	. . . . 5 ⊢ (y ∩ z) ∈ V
101		sseq1 2072	. . . . . 6 ⊢ (x = (y ∩ z) → (x ⊆ A ↔ (y ∩ z) ⊆ A))
102		difeq2 2144	. . . . . . . 8 ⊢ (x = (y ∩ z) → (A ∖ x) = (A ∖ (y ∩ z)))
103	102	breq1d 2619	. . . . . . 7 ⊢ (x = (y ∩ z) → ((A ∖ x) ≼ ω ↔ (A ∖ (y ∩ z)) ≼ ω))
104		eqeq1 1473	. . . . . . 7 ⊢ (x = (y ∩ z) → (x = ∅ ↔ (y ∩ z) = ∅))
105	103, 104	orbi12d 625	. . . . . 6 ⊢ (x = (y ∩ z) → (((A ∖ x) ≼ ω ⋁ x = ∅) ↔ ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅)))
106	101, 105	anbi12d 626	. . . . 5 ⊢ (x = (y ∩ z) → ((x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅)) ↔ ((y ∩ z) ⊆ A ⋀ ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅))))
107	100, 106	elab 1888	. . . 4 ⊢ ((y ∩ z) ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ↔ ((y ∩ z) ⊆ A ⋀ ((A ∖ (y ∩ z)) ≼ ω ⋁ (y ∩ z) = ∅)))
108	91, 99, 107	3imtr4 219	. . 3 ⊢ ((y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ⋀ z ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}) → (y ∩ z) ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))})
109	108	rgen2a 1691	. 2 ⊢ ∀y ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}∀z ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} (y ∩ z) ∈ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))}
110	5, 72, 109	mpbir2an 728	1 ⊢ {x∣(x ⊆ A ⋀ ((A ∖ x) ≼ ω ⋁ x = ∅))} ∈ Top

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222   ⋀ wa 223  ∀wal 951   = wceq 953   ∈ wcel 955  {cab 1456  ∀wral 1637  ∃wrex 1638  {crab 1640  Vcvv 1802   ∖ cdif 2034   ∪ cun 2035   ∩ cin 2036   ⊆ wss 2037  ∅c0 2270  {csn 2399  ∪cuni 2493   class class class wbr 2609  ωcom 3121   ≼ cdom 4349  Topctop 7530

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-rep 2683  ax-sep 2693  ax-nul 2700  ax-pow 2732  ax-pr 2769  ax-un 2857  ax-reg 4565  ax-inf2 4597  ax-ac 4716

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-nel 1580  df-ral 1641  df-rex 1642  df-reu 1643  df-rab 1644  df-v 1803  df-sbc 1932  df-csb 1992  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-pss 2045  df-nul 2271  df-if 2352  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-int 2524  df-iun 2558  df-iin 2559  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-lim 2943  df-suc 2944  df-om 3122  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-f 3184  df-f1 3185  df-fo 3186  df-f1o 3187  df-fv 3188  df-iso 3189  df-rdg 3917  df-opr 3950  df-oprab 3951  df-1st 4063  df-2nd 4064  df-1o 4117  df-2o 4118  df-oadd 4119  df-omul 4120  df-er 4245  df-ec 4247  df-qs 4250  df-en 4351  df-dom 4352  df-sdom 4353  df-r1 4615  df-rank 4616  df-card 4788  df-ni 4972  df-pli 4973  df-mi 4974  df-lti 4975  df-plpq 5007  df-mpq 5008  df-enq 5009  df-nq 5010  df-plq 5011  df-mq 5012  df-rq 5013  df-ltq 5014  df-1q 5015  df-np 5058  df-1p 5059  df-plp 5060  df-mp 5061  df-ltp 5062  df-plpr 5136  df-mpr 5137  df-enr 5138  df-nr 5139  df-plr 5140  df-mr 5141  df-ltr 5142  df-0r 5143  df-1r 5144  df-m1r 5145  df-c 5212  df-0 5213  df-1 5214  df-i 5215  df-r 5216  df-plus 5217  df-mul 5218  df-lt 5219  df-sub 5328  df-neg 5330  df-pnf 5459  df-mnf 5460  df-xr 5461  df-ltxr 5462  df-le 5463  df-n 5873  df-2 5917  df-n0 6047  df-z 6083  df-seq1 6245  df-exp 6501  df-top 7534

Copyright terms: Public domain