hauspwpwf1

Description: Lemma for hauspwpwdom . Points in the closure of a set in a Hausdorff space are characterized by the open neighborhoods they extend into the generating set. (Contributed by Mario Carneiro, 28-Jul-2015)

	Ref	Expression
Hypotheses	hauspwpwf1.x	$⊢ X = ⋃ J$
	hauspwpwf1.f	$⊢ F = (x \in cls (J) (A) ⟼ \{a \| \exists j \in J (x \in j \land a = j \cap A)\})$
Assertion	hauspwpwf1	$⊢ (J \in Haus \land A \subseteq X) \to F : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A$

Proof

Step	Hyp	Ref	Expression
1		hauspwpwf1.x	$⊢ X = ⋃ J$
2		hauspwpwf1.f	$⊢ F = (x \in cls (J) (A) ⟼ \{a \| \exists j \in J (x \in j \land a = j \cap A)\})$
3		inss2	$⊢ j \cap A \subseteq A$
4		vex	$⊢ j \in V$
5	4	inex1	$⊢ j \cap A \in V$
6	5	elpw	$⊢ j \cap A \in 𝒫 A \leftrightarrow j \cap A \subseteq A$
7	3 6	mpbir	$⊢ j \cap A \in 𝒫 A$
8		eleq1	$⊢ a = j \cap A \to (a \in 𝒫 A \leftrightarrow j \cap A \in 𝒫 A)$
9	7 8	mpbiri	$⊢ a = j \cap A \to a \in 𝒫 A$
10	9	adantl	$⊢ (x \in j \land a = j \cap A) \to a \in 𝒫 A$
11	10	rexlimivw	$⊢ \exists j \in J (x \in j \land a = j \cap A) \to a \in 𝒫 A$
12	11	abssi	$⊢ \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \subseteq 𝒫 A$
13		haustop	$⊢ J \in Haus \to J \in Top$
14	1	topopn	$⊢ J \in Top \to X \in J$
15	13 14	syl	$⊢ J \in Haus \to X \in J$
16		ssexg	$⊢ (A \subseteq X \land X \in J) \to A \in V$
17	15 16	sylan2	$⊢ (A \subseteq X \land J \in Haus) \to A \in V$
18	17	ancoms	$⊢ (J \in Haus \land A \subseteq X) \to A \in V$
19		pwexg	$⊢ A \in V \to 𝒫 A \in V$
20		elpw2g	$⊢ 𝒫 A \in V \to (\{a \| \exists j \in J (x \in j \land a = j \cap A)\} \in 𝒫 𝒫 A \leftrightarrow \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \subseteq 𝒫 A)$
21	18 19 20	3syl	$⊢ (J \in Haus \land A \subseteq X) \to (\{a \| \exists j \in J (x \in j \land a = j \cap A)\} \in 𝒫 𝒫 A \leftrightarrow \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \subseteq 𝒫 A)$
22	12 21	mpbiri	$⊢ (J \in Haus \land A \subseteq X) \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \in 𝒫 𝒫 A$
23	22	a1d	$⊢ (J \in Haus \land A \subseteq X) \to (x \in cls (J) (A) \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \in 𝒫 𝒫 A)$
24		simplll	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to J \in Haus$
25	1	clsss3	$⊢ (J \in Top \land A \subseteq X) \to cls (J) (A) \subseteq X$
26	13 25	sylan	$⊢ (J \in Haus \land A \subseteq X) \to cls (J) (A) \subseteq X$
27	26	ad2antrr	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to cls (J) (A) \subseteq X$
28		simplrl	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to x \in cls (J) (A)$
29	27 28	sseldd	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to x \in X$
30		simplrr	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to y \in cls (J) (A)$
31	27 30	sseldd	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to y \in X$
32		simpr	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to x \neq y$
33	1	hausnei	$⊢ (J \in Haus \land (x \in X \land y \in X \land x \neq y)) \to \exists k \in J \exists l \in J (x \in k \land y \in l \land k \cap l = \emptyset)$
34	24 29 31 32 33	syl13anc	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to \exists k \in J \exists l \in J (x \in k \land y \in l \land k \cap l = \emptyset)$
35		simprll	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \to k \in J$
36		simprr1	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \to x \in k$
37		eqidd	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \to k \cap A = k \cap A$
38		elequ2	$⊢ j = k \to (x \in j \leftrightarrow x \in k)$
39		ineq1	$⊢ j = k \to j \cap A = k \cap A$
40	39	eqeq2d	$⊢ j = k \to (k \cap A = j \cap A \leftrightarrow k \cap A = k \cap A)$
41	38 40	anbi12d	$⊢ j = k \to ((x \in j \land k \cap A = j \cap A) \leftrightarrow (x \in k \land k \cap A = k \cap A))$
42	41	rspcev	$⊢ (k \in J \land (x \in k \land k \cap A = k \cap A)) \to \exists j \in J (x \in j \land k \cap A = j \cap A)$
43	35 36 37 42	syl12anc	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \to \exists j \in J (x \in j \land k \cap A = j \cap A)$
44		vex	$⊢ k \in V$
45	44	inex1	$⊢ k \cap A \in V$
46		eqeq1	$⊢ a = k \cap A \to (a = j \cap A \leftrightarrow k \cap A = j \cap A)$
47	46	anbi2d	$⊢ a = k \cap A \to ((x \in j \land a = j \cap A) \leftrightarrow (x \in j \land k \cap A = j \cap A))$
48	47	rexbidv	$⊢ a = k \cap A \to (\exists j \in J (x \in j \land a = j \cap A) \leftrightarrow \exists j \in J (x \in j \land k \cap A = j \cap A))$
49	45 48	elab	$⊢ k \cap A \in \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \leftrightarrow \exists j \in J (x \in j \land k \cap A = j \cap A)$
50	43 49	sylibr	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \to k \cap A \in \{a \| \exists j \in J (x \in j \land a = j \cap A)\}$
51	13	ad2antrr	$⊢ ((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \to J \in Top$
52	51	ad3antrrr	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to J \in Top$
53		simplr	$⊢ ((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \to A \subseteq X$
54	53	ad3antrrr	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to A \subseteq X$
55		simprr	$⊢ ((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \to y \in cls (J) (A)$
56	55	ad3antrrr	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to y \in cls (J) (A)$
57		simplr	$⊢ ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset)) \to l \in J$
58	57	ad2antlr	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to l \in J$
59		simprl	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to j \in J$
60		inopn	$⊢ (J \in Top \land l \in J \land j \in J) \to l \cap j \in J$
61	52 58 59 60	syl3anc	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to l \cap j \in J$
62		simpr2	$⊢ ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset)) \to y \in l$
63	62	ad2antlr	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to y \in l$
64		simprr	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to y \in j$
65	63 64	elind	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to y \in (l \cap j)$
66	1	clsndisj	$⊢ ((J \in Top \land A \subseteq X \land y \in cls (J) (A)) \land (l \cap j \in J \land y \in (l \cap j))) \to (l \cap j) \cap A \neq \emptyset$
67	52 54 56 61 65 66	syl32anc	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to (l \cap j) \cap A \neq \emptyset$
68		n0	$⊢ (l \cap j) \cap A \neq \emptyset \leftrightarrow \exists z z \in ((l \cap j) \cap A)$
69	67 68	sylib	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to \exists z z \in ((l \cap j) \cap A)$
70		elin	$⊢ z \in ((l \cap j) \cap A) \leftrightarrow (z \in (l \cap j) \land z \in A)$
71		elin	$⊢ z \in (l \cap j) \leftrightarrow (z \in l \land z \in j)$
72	71	anbi1i	$⊢ (z \in (l \cap j) \land z \in A) \leftrightarrow ((z \in l \land z \in j) \land z \in A)$
73	70 72	bitri	$⊢ z \in ((l \cap j) \cap A) \leftrightarrow ((z \in l \land z \in j) \land z \in A)$
74		elin	$⊢ z \in (j \cap A) \leftrightarrow (z \in j \land z \in A)$
75	74	biimpri	$⊢ (z \in j \land z \in A) \to z \in (j \cap A)$
76	75	adantll	$⊢ ((z \in l \land z \in j) \land z \in A) \to z \in (j \cap A)$
77	76	ad2antll	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land ((j \in J \land y \in j) \land ((z \in l \land z \in j) \land z \in A))) \to z \in (j \cap A)$
78		simpll	$⊢ ((z \in l \land z \in j) \land z \in A) \to z \in l$
79	78	ad2antll	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land ((j \in J \land y \in j) \land ((z \in l \land z \in j) \land z \in A))) \to z \in l$
80		simpr3	$⊢ ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset)) \to k \cap l = \emptyset$
81	80	ad2antlr	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land ((j \in J \land y \in j) \land ((z \in l \land z \in j) \land z \in A))) \to k \cap l = \emptyset$
82		minel	$⊢ (z \in l \land k \cap l = \emptyset) \to \neg z \in k$
83		elinel1	$⊢ z \in (k \cap A) \to z \in k$
84	82 83	nsyl	$⊢ (z \in l \land k \cap l = \emptyset) \to \neg z \in (k \cap A)$
85	79 81 84	syl2anc	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land ((j \in J \land y \in j) \land ((z \in l \land z \in j) \land z \in A))) \to \neg z \in (k \cap A)$
86		nelneq2	$⊢ (z \in (j \cap A) \land \neg z \in (k \cap A)) \to \neg j \cap A = k \cap A$
87	77 85 86	syl2anc	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land ((j \in J \land y \in j) \land ((z \in l \land z \in j) \land z \in A))) \to \neg j \cap A = k \cap A$
88		eqcom	$⊢ j \cap A = k \cap A \leftrightarrow k \cap A = j \cap A$
89	87 88	sylnib	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land ((j \in J \land y \in j) \land ((z \in l \land z \in j) \land z \in A))) \to \neg k \cap A = j \cap A$
90	89	expr	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to (((z \in l \land z \in j) \land z \in A) \to \neg k \cap A = j \cap A)$
91	73 90	syl5bi	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to (z \in ((l \cap j) \cap A) \to \neg k \cap A = j \cap A)$
92	91	exlimdv	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to (\exists z z \in ((l \cap j) \cap A) \to \neg k \cap A = j \cap A)$
93	69 92	mpd	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land (j \in J \land y \in j)) \to \neg k \cap A = j \cap A$
94	93	anassrs	$⊢ ((((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land j \in J) \land y \in j) \to \neg k \cap A = j \cap A$
95		nan	$⊢ ((((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land j \in J) \to \neg (y \in j \land k \cap A = j \cap A)) \leftrightarrow (((((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land j \in J) \land y \in j) \to \neg k \cap A = j \cap A)$
96	94 95	mpbir	$⊢ (((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \land j \in J) \to \neg (y \in j \land k \cap A = j \cap A)$
97	96	nrexdv	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \to \neg \exists j \in J (y \in j \land k \cap A = j \cap A)$
98	46	anbi2d	$⊢ a = k \cap A \to ((y \in j \land a = j \cap A) \leftrightarrow (y \in j \land k \cap A = j \cap A))$
99	98	rexbidv	$⊢ a = k \cap A \to (\exists j \in J (y \in j \land a = j \cap A) \leftrightarrow \exists j \in J (y \in j \land k \cap A = j \cap A))$
100	45 99	elab	$⊢ k \cap A \in \{a \| \exists j \in J (y \in j \land a = j \cap A)\} \leftrightarrow \exists j \in J (y \in j \land k \cap A = j \cap A)$
101	97 100	sylnibr	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \to \neg k \cap A \in \{a \| \exists j \in J (y \in j \land a = j \cap A)\}$
102		nelne1	$⊢ (k \cap A \in \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \land \neg k \cap A \in \{a \| \exists j \in J (y \in j \land a = j \cap A)\}) \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \neq \{a \| \exists j \in J (y \in j \land a = j \cap A)\}$
103	50 101 102	syl2anc	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land ((k \in J \land l \in J) \land (x \in k \land y \in l \land k \cap l = \emptyset))) \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \neq \{a \| \exists j \in J (y \in j \land a = j \cap A)\}$
104	103	expr	$⊢ ((((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \land (k \in J \land l \in J)) \to ((x \in k \land y \in l \land k \cap l = \emptyset) \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \neq \{a \| \exists j \in J (y \in j \land a = j \cap A)\})$
105	104	rexlimdvva	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to (\exists k \in J \exists l \in J (x \in k \land y \in l \land k \cap l = \emptyset) \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \neq \{a \| \exists j \in J (y \in j \land a = j \cap A)\})$
106	34 105	mpd	$⊢ (((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \land x \neq y) \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \neq \{a \| \exists j \in J (y \in j \land a = j \cap A)\}$
107	106	ex	$⊢ ((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \to (x \neq y \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} \neq \{a \| \exists j \in J (y \in j \land a = j \cap A)\})$
108	107	necon4d	$⊢ ((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \to (\{a \| \exists j \in J (x \in j \land a = j \cap A)\} = \{a \| \exists j \in J (y \in j \land a = j \cap A)\} \to x = y)$
109		eleq1	$⊢ x = y \to (x \in j \leftrightarrow y \in j)$
110	109	anbi1d	$⊢ x = y \to ((x \in j \land a = j \cap A) \leftrightarrow (y \in j \land a = j \cap A))$
111	110	rexbidv	$⊢ x = y \to (\exists j \in J (x \in j \land a = j \cap A) \leftrightarrow \exists j \in J (y \in j \land a = j \cap A))$
112	111	abbidv	$⊢ x = y \to \{a \| \exists j \in J (x \in j \land a = j \cap A)\} = \{a \| \exists j \in J (y \in j \land a = j \cap A)\}$
113	108 112	impbid1	$⊢ ((J \in Haus \land A \subseteq X) \land (x \in cls (J) (A) \land y \in cls (J) (A))) \to (\{a \| \exists j \in J (x \in j \land a = j \cap A)\} = \{a \| \exists j \in J (y \in j \land a = j \cap A)\} \leftrightarrow x = y)$
114	113	ex	$⊢ (J \in Haus \land A \subseteq X) \to ((x \in cls (J) (A) \land y \in cls (J) (A)) \to (\{a \| \exists j \in J (x \in j \land a = j \cap A)\} = \{a \| \exists j \in J (y \in j \land a = j \cap A)\} \leftrightarrow x = y))$
115	23 114	dom2lem	$⊢ (J \in Haus \land A \subseteq X) \to (x \in cls (J) (A) ⟼ \{a \| \exists j \in J (x \in j \land a = j \cap A)\}) : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A$
116		f1eq1	$⊢ F = (x \in cls (J) (A) ⟼ \{a \| \exists j \in J (x \in j \land a = j \cap A)\}) \to (F : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A \leftrightarrow (x \in cls (J) (A) ⟼ \{a \| \exists j \in J (x \in j \land a = j \cap A)\}) : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A)$
117	2 116	ax-mp	$⊢ F : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A \leftrightarrow (x \in cls (J) (A) ⟼ \{a \| \exists j \in J (x \in j \land a = j \cap A)\}) : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A$
118	115 117	sylibr	$⊢ (J \in Haus \land A \subseteq X) \to F : cls (J) (A) \underset{1-1}{⟶} 𝒫 𝒫 A$

Metamath Proof Explorer

Theorem hauspwpwf1

Proof