pthaus

Description: The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	pthaus	$⊢ (A \in V \land F : A ⟶ Haus) \to \prod_{𝑡} (F) \in Haus$

Proof

Step	Hyp	Ref	Expression
1		haustop	$⊢ x \in Haus \to x \in Top$
2	1	ssriv	$⊢ Haus \subseteq Top$
3		fss	$⊢ (F : A ⟶ Haus \land Haus \subseteq Top) \to F : A ⟶ Top$
4	2 3	mpan2	$⊢ F : A ⟶ Haus \to F : A ⟶ Top$
5		pttop	$⊢ (A \in V \land F : A ⟶ Top) \to \prod_{𝑡} (F) \in Top$
6	4 5	sylan2	$⊢ (A \in V \land F : A ⟶ Haus) \to \prod_{𝑡} (F) \in Top$
7		simprl	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to x \in ⋃ \prod_{𝑡} (F)$
8		eqid	$⊢ \prod_{𝑡} (F) = \prod_{𝑡} (F)$
9	8	ptuni	$⊢ (A \in V \land F : A ⟶ Top) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ \prod_{𝑡} (F)$
10	4 9	sylan2	$⊢ (A \in V \land F : A ⟶ Haus) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ \prod_{𝑡} (F)$
11	10	adantr	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \underset{k \in A}{⨉} ⋃ F (k) = ⋃ \prod_{𝑡} (F)$
12	7 11	eleqtrrd	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to x \in \underset{k \in A}{⨉} ⋃ F (k)$
13		ixpfn	$⊢ x \in \underset{k \in A}{⨉} ⋃ F (k) \to x Fn A$
14	12 13	syl	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to x Fn A$
15		simprr	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to y \in ⋃ \prod_{𝑡} (F)$
16	15 11	eleqtrrd	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to y \in \underset{k \in A}{⨉} ⋃ F (k)$
17		ixpfn	$⊢ y \in \underset{k \in A}{⨉} ⋃ F (k) \to y Fn A$
18	16 17	syl	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to y Fn A$
19		eqfnfv	$⊢ (x Fn A \land y Fn A) \to (x = y \leftrightarrow \forall k \in A x (k) = y (k))$
20	14 18 19	syl2anc	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to (x = y \leftrightarrow \forall k \in A x (k) = y (k))$
21	20	necon3abid	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to (x \neq y \leftrightarrow \neg \forall k \in A x (k) = y (k))$
22		rexnal	$⊢ \exists k \in A \neg x (k) = y (k) \leftrightarrow \neg \forall k \in A x (k) = y (k)$
23		df-ne	$⊢ x (k) \neq y (k) \leftrightarrow \neg x (k) = y (k)$
24		simpllr	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to F : A ⟶ Haus$
25		simprl	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to k \in A$
26	24 25	ffvelrnd	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to F (k) \in Haus$
27		vex	$⊢ x \in V$
28	27	elixp	$⊢ x \in \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow (x Fn A \land \forall k \in A x (k) \in ⋃ F (k))$
29	28	simprbi	$⊢ x \in \underset{k \in A}{⨉} ⋃ F (k) \to \forall k \in A x (k) \in ⋃ F (k)$
30	12 29	syl	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \forall k \in A x (k) \in ⋃ F (k)$
31	30	r19.21bi	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land k \in A) \to x (k) \in ⋃ F (k)$
32	31	adantrr	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to x (k) \in ⋃ F (k)$
33		vex	$⊢ y \in V$
34	33	elixp	$⊢ y \in \underset{k \in A}{⨉} ⋃ F (k) \leftrightarrow (y Fn A \land \forall k \in A y (k) \in ⋃ F (k))$
35	34	simprbi	$⊢ y \in \underset{k \in A}{⨉} ⋃ F (k) \to \forall k \in A y (k) \in ⋃ F (k)$
36	16 35	syl	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to \forall k \in A y (k) \in ⋃ F (k)$
37	36	r19.21bi	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land k \in A) \to y (k) \in ⋃ F (k)$
38	37	adantrr	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to y (k) \in ⋃ F (k)$
39		simprr	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to x (k) \neq y (k)$
40		eqid	$⊢ ⋃ F (k) = ⋃ F (k)$
41	40	hausnei	$⊢ (F (k) \in Haus \land (x (k) \in ⋃ F (k) \land y (k) \in ⋃ F (k) \land x (k) \neq y (k))) \to \exists m \in F (k) \exists n \in F (k) (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset)$
42	26 32 38 39 41	syl13anc	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to \exists m \in F (k) \exists n \in F (k) (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset)$
43		simp-4l	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to A \in V$
44	4	ad4antlr	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to F : A ⟶ Top$
45	25	adantr	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to k \in A$
46		eqid	$⊢ ⋃ \prod_{𝑡} (F) = ⋃ \prod_{𝑡} (F)$
47	46 8	ptpjcn	$⊢ (A \in V \land F : A ⟶ Top \land k \in A) \to (z \in ⋃ \prod_{𝑡} (F) ⟼ z (k)) \in (\prod_{𝑡} (F) Cn F (k))$
48	43 44 45 47	syl3anc	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to (z \in ⋃ \prod_{𝑡} (F) ⟼ z (k)) \in (\prod_{𝑡} (F) Cn F (k))$
49		simprll	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to m \in F (k)$
50		eqid	$⊢ (z \in ⋃ \prod_{𝑡} (F) ⟼ z (k)) = (z \in ⋃ \prod_{𝑡} (F) ⟼ z (k))$
51	50	mptpreima	$⊢ {(z \in ⋃ \prod_{𝑡} (F) ⟼ z (k))}^{-1} [m] = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\}$
52		cnima	$⊢ ((z \in ⋃ \prod_{𝑡} (F) ⟼ z (k)) \in (\prod_{𝑡} (F) Cn F (k)) \land m \in F (k)) \to {(z \in ⋃ \prod_{𝑡} (F) ⟼ z (k))}^{-1} [m] \in \prod_{𝑡} (F)$
53	51 52	eqeltrrid	$⊢ ((z \in ⋃ \prod_{𝑡} (F) ⟼ z (k)) \in (\prod_{𝑡} (F) Cn F (k)) \land m \in F (k)) \to \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \in \prod_{𝑡} (F)$
54	48 49 53	syl2anc	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \in \prod_{𝑡} (F)$
55		simprlr	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to n \in F (k)$
56	50	mptpreima	$⊢ {(z \in ⋃ \prod_{𝑡} (F) ⟼ z (k))}^{-1} [n] = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\}$
57		cnima	$⊢ ((z \in ⋃ \prod_{𝑡} (F) ⟼ z (k)) \in (\prod_{𝑡} (F) Cn F (k)) \land n \in F (k)) \to {(z \in ⋃ \prod_{𝑡} (F) ⟼ z (k))}^{-1} [n] \in \prod_{𝑡} (F)$
58	56 57	eqeltrrid	$⊢ ((z \in ⋃ \prod_{𝑡} (F) ⟼ z (k)) \in (\prod_{𝑡} (F) Cn F (k)) \land n \in F (k)) \to \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \in \prod_{𝑡} (F)$
59	48 55 58	syl2anc	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \in \prod_{𝑡} (F)$
60		fveq1	$⊢ z = x \to z (k) = x (k)$
61	60	eleq1d	$⊢ z = x \to (z (k) \in m \leftrightarrow x (k) \in m)$
62	7	ad2antrr	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to x \in ⋃ \prod_{𝑡} (F)$
63		simprr1	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to x (k) \in m$
64	61 62 63	elrabd	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to x \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\}$
65		fveq1	$⊢ z = y \to z (k) = y (k)$
66	65	eleq1d	$⊢ z = y \to (z (k) \in n \leftrightarrow y (k) \in n)$
67	15	ad2antrr	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to y \in ⋃ \prod_{𝑡} (F)$
68		simprr2	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to y (k) \in n$
69	66 67 68	elrabd	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to y \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\}$
70		inrab	$⊢ \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} = \{z \in ⋃ \prod_{𝑡} (F) \| (z (k) \in m \land z (k) \in n)\}$
71		simprr3	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to m \cap n = \emptyset$
72		inelcm	$⊢ (z (k) \in m \land z (k) \in n) \to m \cap n \neq \emptyset$
73	72	necon2bi	$⊢ m \cap n = \emptyset \to \neg (z (k) \in m \land z (k) \in n)$
74	71 73	syl	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to \neg (z (k) \in m \land z (k) \in n)$
75	74	ralrimivw	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to \forall z \in ⋃ \prod_{𝑡} (F) \neg (z (k) \in m \land z (k) \in n)$
76		rabeq0	$⊢ \{z \in ⋃ \prod_{𝑡} (F) \| (z (k) \in m \land z (k) \in n)\} = \emptyset \leftrightarrow \forall z \in ⋃ \prod_{𝑡} (F) \neg (z (k) \in m \land z (k) \in n)$
77	75 76	sylibr	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to \{z \in ⋃ \prod_{𝑡} (F) \| (z (k) \in m \land z (k) \in n)\} = \emptyset$
78	70 77	eqtrid	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} = \emptyset$
79		eleq2	$⊢ u = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \to (x \in u \leftrightarrow x \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\})$
80		ineq1	$⊢ u = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \to u \cap v = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap v$
81	80	eqeq1d	$⊢ u = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \to (u \cap v = \emptyset \leftrightarrow \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap v = \emptyset)$
82	79 81	3anbi13d	$⊢ u = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \to ((x \in u \land y \in v \land u \cap v = \emptyset) \leftrightarrow (x \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \land y \in v \land \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap v = \emptyset))$
83		eleq2	$⊢ v = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \to (y \in v \leftrightarrow y \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\})$
84		ineq2	$⊢ v = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \to \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap v = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\}$
85	84	eqeq1d	$⊢ v = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \to (\{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap v = \emptyset \leftrightarrow \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} = \emptyset)$
86	83 85	3anbi23d	$⊢ v = \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \to ((x \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \land y \in v \land \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap v = \emptyset) \leftrightarrow (x \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \land y \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \land \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} = \emptyset))$
87	82 86	rspc2ev	$⊢ (\{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \in \prod_{𝑡} (F) \land \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \in \prod_{𝑡} (F) \land (x \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \land y \in \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} \land \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in m\} \cap \{z \in ⋃ \prod_{𝑡} (F) \| z (k) \in n\} = \emptyset)) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset)$
88	54 59 64 69 78 87	syl113anc	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land ((m \in F (k) \land n \in F (k)) \land (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset))) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset)$
89	88	expr	$⊢ ((((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \land (m \in F (k) \land n \in F (k))) \to ((x (k) \in m \land y (k) \in n \land m \cap n = \emptyset) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset))$
90	89	rexlimdvva	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to (\exists m \in F (k) \exists n \in F (k) (x (k) \in m \land y (k) \in n \land m \cap n = \emptyset) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset))$
91	42 90	mpd	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land (k \in A \land x (k) \neq y (k))) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset)$
92	91	expr	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land k \in A) \to (x (k) \neq y (k) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset))$
93	23 92	syl5bir	$⊢ (((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \land k \in A) \to (\neg x (k) = y (k) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset))$
94	93	rexlimdva	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to (\exists k \in A \neg x (k) = y (k) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset))$
95	22 94	syl5bir	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to (\neg \forall k \in A x (k) = y (k) \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset))$
96	21 95	sylbid	$⊢ ((A \in V \land F : A ⟶ Haus) \land (x \in ⋃ \prod_{𝑡} (F) \land y \in ⋃ \prod_{𝑡} (F))) \to (x \neq y \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset))$
97	96	ralrimivva	$⊢ (A \in V \land F : A ⟶ Haus) \to \forall x \in ⋃ \prod_{𝑡} (F) \forall y \in ⋃ \prod_{𝑡} (F) (x \neq y \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset))$
98	46	ishaus	$⊢ \prod_{𝑡} (F) \in Haus \leftrightarrow (\prod_{𝑡} (F) \in Top \land \forall x \in ⋃ \prod_{𝑡} (F) \forall y \in ⋃ \prod_{𝑡} (F) (x \neq y \to \exists u \in \prod_{𝑡} (F) \exists v \in \prod_{𝑡} (F) (x \in u \land y \in v \land u \cap v = \emptyset)))$
99	6 97 98	sylanbrc	$⊢ (A \in V \land F : A ⟶ Haus) \to \prod_{𝑡} (F) \in Haus$

Metamath Proof Explorer

Theorem pthaus

Proof