2ndcdisj

Description: Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015) (Proof shortened by Mario Carneiro, 9-Apr-2015) (Revised by NM, 17-Jun-2017)

		Ref	Expression
	Assertion	2ndcdisj	$⊢ (J \in 2^{nd} 𝜔 \land \forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω$

Proof

Step	Hyp	Ref	Expression
1		is2ndc	$⊢ J \in 2^{nd} 𝜔 \leftrightarrow \exists b \in TopBases (b ≼ ω \land topGen (b) = J)$
2		omex	$⊢ ω \in V$
3	2	brdom	$⊢ b ≼ ω \leftrightarrow \exists f f : b \underset{1-1}{⟶} ω$
4		ssrab2	$⊢ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \subseteq ran f$
5		f1f	$⊢ f : b \underset{1-1}{⟶} ω \to f : b ⟶ ω$
6	5	frnd	$⊢ f : b \underset{1-1}{⟶} ω \to ran f \subseteq ω$
7	6	adantl	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to ran f \subseteq ω$
8	4 7	sstrid	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \subseteq ω$
9	8	adantr	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \to \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \subseteq ω$
10		eldifsn	$⊢ B \in (topGen (b) ∖ \{\emptyset\}) \leftrightarrow (B \in topGen (b) \land B \neq \emptyset)$
11		n0	$⊢ B \neq \emptyset \leftrightarrow \exists y y \in B$
12		tg2	$⊢ (B \in topGen (b) \land y \in B) \to \exists z \in b (y \in z \land z \subseteq B)$
13		omsson	$⊢ ω \subseteq On$
14	8 13	sstrdi	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \subseteq On$
15	14	ad2antrr	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \subseteq On$
16		f1fn	$⊢ f : b \underset{1-1}{⟶} ω \to f Fn b$
17	16	ad3antlr	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to f Fn b$
18		simprl	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to z \in b$
19		fnfvelrn	$⊢ (f Fn b \land z \in b) \to f (z) \in ran f$
20	17 18 19	syl2anc	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to f (z) \in ran f$
21		f1f1orn	$⊢ f : b \underset{1-1}{⟶} ω \to f : b \underset{1-1 onto}{⟶} ran f$
22	21	ad3antlr	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to f : b \underset{1-1 onto}{⟶} ran f$
23		f1ocnvfv1	$⊢ (f : b \underset{1-1 onto}{⟶} ran f \land z \in b) \to f^{-1} (f (z)) = z$
24	22 18 23	syl2anc	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to f^{-1} (f (z)) = z$
25		simprrr	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to z \subseteq B$
26		velpw	$⊢ z \in 𝒫 B \leftrightarrow z \subseteq B$
27	25 26	sylibr	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to z \in 𝒫 B$
28		simprrl	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to y \in z$
29	28	ne0d	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to z \neq \emptyset$
30		eldifsn	$⊢ z \in (𝒫 B ∖ \{\emptyset\}) \leftrightarrow (z \in 𝒫 B \land z \neq \emptyset)$
31	27 29 30	sylanbrc	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to z \in (𝒫 B ∖ \{\emptyset\})$
32	24 31	eqeltrd	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to f^{-1} (f (z)) \in (𝒫 B ∖ \{\emptyset\})$
33		fveq2	$⊢ n = f (z) \to f^{-1} (n) = f^{-1} (f (z))$
34	33	eleq1d	$⊢ n = f (z) \to (f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\}) \leftrightarrow f^{-1} (f (z)) \in (𝒫 B ∖ \{\emptyset\}))$
35	34	rspcev	$⊢ (f (z) \in ran f \land f^{-1} (f (z)) \in (𝒫 B ∖ \{\emptyset\})) \to \exists n \in ran f f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})$
36	20 32 35	syl2anc	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to \exists n \in ran f f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})$
37		rabn0	$⊢ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \neq \emptyset \leftrightarrow \exists n \in ran f f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})$
38	36 37	sylibr	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \neq \emptyset$
39		onint	$⊢ (\{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \subseteq On \land \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \neq \emptyset) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}$
40	15 38 39	syl2anc	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land (z \in b \land (y \in z \land z \subseteq B))) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}$
41	40	rexlimdvaa	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \to (\exists z \in b (y \in z \land z \subseteq B) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
42	12 41	syl5	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \to ((B \in topGen (b) \land y \in B) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
43	42	expdimp	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land B \in topGen (b)) \to (y \in B \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
44	43	exlimdv	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land B \in topGen (b)) \to (\exists y y \in B \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
45	11 44	syl5bi	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \land B \in topGen (b)) \to (B \neq \emptyset \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
46	45	expimpd	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \to ((B \in topGen (b) \land B \neq \emptyset) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
47	10 46	syl5bi	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \to (B \in (topGen (b) ∖ \{\emptyset\}) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
48	47	impr	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}$
49	9 48	sseldd	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in ω$
50	49	expr	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land x \in A) \to (B \in (topGen (b) ∖ \{\emptyset\}) \to ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in ω)$
51	50	ralimdva	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \to \forall x \in A ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in ω)$
52	51	imp	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land \forall x \in A B \in (topGen (b) ∖ \{\emptyset\})) \to \forall x \in A ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in ω$
53	52	adantrr	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B)) \to \forall x \in A ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in ω$
54		eqid	$⊢ (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) = (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
55	54	fmpt	$⊢ \forall x \in A ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in ω \leftrightarrow (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) : A ⟶ ω$
56	53 55	sylib	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B)) \to (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) : A ⟶ ω$
57		neeq1	$⊢ f^{-1} (z) = if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \to (f^{-1} (z) \neq \emptyset \leftrightarrow if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \neq \emptyset)$
58		neeq1	$⊢ 1_{𝑜} = if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \to (1_{𝑜} \neq \emptyset \leftrightarrow if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \neq \emptyset)$
59		1n0	$⊢ 1_{𝑜} \neq \emptyset$
60	57 58 59	elimhyp	$⊢ if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \neq \emptyset$
61		n0	$⊢ if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \neq \emptyset \leftrightarrow \exists y y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜})$
62	60 61	mpbi	$⊢ \exists y y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜})$
63		19.29r	$⊢ (\exists y y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \land \forall y \exists^{} x \in A y \in B) \to \exists y (y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \land \exists^{} x \in A y \in B)$
64	62 63	mpan	$⊢ \forall y \exists^{} x \in A y \in B \to \exists y (y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \land \exists^{} x \in A y \in B)$
65		eleq1	$⊢ z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to (z \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \leftrightarrow ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
66	48 65	syl5ibrcom	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \to (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to z \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
67	66	imp	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to z \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}$
68		fveq2	$⊢ n = z \to f^{-1} (n) = f^{-1} (z)$
69	68	eleq1d	$⊢ n = z \to (f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\}) \leftrightarrow f^{-1} (z) \in (𝒫 B ∖ \{\emptyset\}))$
70	69	elrab	$⊢ z \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \leftrightarrow (z \in ran f \land f^{-1} (z) \in (𝒫 B ∖ \{\emptyset\}))$
71	70	simprbi	$⊢ z \in \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to f^{-1} (z) \in (𝒫 B ∖ \{\emptyset\})$
72	67 71	syl	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to f^{-1} (z) \in (𝒫 B ∖ \{\emptyset\})$
73		eldifsn	$⊢ f^{-1} (z) \in (𝒫 B ∖ \{\emptyset\}) \leftrightarrow (f^{-1} (z) \in 𝒫 B \land f^{-1} (z) \neq \emptyset)$
74	72 73	sylib	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to (f^{-1} (z) \in 𝒫 B \land f^{-1} (z) \neq \emptyset)$
75	74	simprd	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to f^{-1} (z) \neq \emptyset$
76	75	iftrued	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) = f^{-1} (z)$
77	74	simpld	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to f^{-1} (z) \in 𝒫 B$
78	77	elpwid	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to f^{-1} (z) \subseteq B$
79	76 78	eqsstrd	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \subseteq B$
80	79	sseld	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (x \in A \land B \in (topGen (b) ∖ \{\emptyset\}))) \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \to (y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \to y \in B)$
81	80	exp31	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to ((x \in A \land B \in (topGen (b) ∖ \{\emptyset\})) \to (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to (y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \to y \in B)))$
82	81	com23	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to ((x \in A \land B \in (topGen (b) ∖ \{\emptyset\})) \to (y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \to y \in B)))$
83	82	exp4a	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to (x \in A \to (B \in (topGen (b) ∖ \{\emptyset\}) \to (y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \to y \in B))))$
84	83	com25	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to (y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \to (x \in A \to (B \in (topGen (b) ∖ \{\emptyset\}) \to (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to y \in B))))$
85	84	imp31	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜})) \land x \in A) \to (B \in (topGen (b) ∖ \{\emptyset\}) \to (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to y \in B))$
86	85	ralimdva	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜})) \to (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \to \forall x \in A (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to y \in B))$
87	86	imp	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜})) \land \forall x \in A B \in (topGen (b) ∖ \{\emptyset\})) \to \forall x \in A (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to y \in B)$
88	87	an32s	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land \forall x \in A B \in (topGen (b) ∖ \{\emptyset\})) \land y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜})) \to \forall x \in A (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to y \in B)$
89		rmoim	$⊢ \forall x \in A (z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \to y \in B) \to (\exists^{} x \in A y \in B \to \exists^{} x \in A z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
90	88 89	syl	$⊢ (((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land \forall x \in A B \in (topGen (b) ∖ \{\emptyset\})) \land y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜})) \to (\exists^{} x \in A y \in B \to \exists^{} x \in A z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
91	90	expimpd	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land \forall x \in A B \in (topGen (b) ∖ \{\emptyset\})) \to ((y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \land \exists^{} x \in A y \in B) \to \exists^{} x \in A z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
92	91	exlimdv	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land \forall x \in A B \in (topGen (b) ∖ \{\emptyset\})) \to (\exists y (y \in if (f^{-1} (z) \neq \emptyset, f^{-1} (z), 1_{𝑜}) \land \exists^{} x \in A y \in B) \to \exists^{} x \in A z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
93	64 92	syl5	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land \forall x \in A B \in (topGen (b) ∖ \{\emptyset\})) \to (\forall y \exists^{} x \in A y \in B \to \exists^{} x \in A z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
94	93	impr	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{} x \in A y \in B)) \to \exists^{} x \in A z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}$
95		nfcv	$⊢ \underline{Ⅎ} x w$
96		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
97		nfcv	$⊢ \underline{Ⅎ} x z$
98	95 96 97	nfbr	$⊢ Ⅎ x w (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z$
99		nfv	$⊢ Ⅎ w (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
100		breq1	$⊢ w = x \to (w (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z \leftrightarrow x (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z)$
101		df-br	$⊢ x (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z \leftrightarrow ⟨x, z⟩ \in (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
102		df-mpt	$⊢ (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) = \{⟨x, z⟩ \| (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})\}$
103	102	eleq2i	$⊢ ⟨x, z⟩ \in (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) \leftrightarrow ⟨x, z⟩ \in \{⟨x, z⟩ \| (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})\}$
104		opabidw	$⊢ ⟨x, z⟩ \in \{⟨x, z⟩ \| (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})\} \leftrightarrow (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
105	101 103 104	3bitri	$⊢ x (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z \leftrightarrow (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
106	100 105	bitrdi	$⊢ w = x \to (w (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z \leftrightarrow (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}))$
107	98 99 106	cbvmow	$⊢ \exists^{} w w (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z \leftrightarrow \exists^{} x (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
108		df-rmo	$⊢ \exists^{} x \in A z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\} \leftrightarrow \exists^{} x (x \in A \land z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\})$
109	107 108	bitr4i	$⊢ \exists^{} w w (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z \leftrightarrow \exists^{} x \in A z = ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}$
110	94 109	sylibr	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{} x \in A y \in B)) \to \exists^{} w w (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z$
111	110	alrimiv	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{} x \in A y \in B)) \to \forall z \exists^{} w w (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z$
112		dff12	$⊢ (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) : A \underset{1-1}{⟶} ω \leftrightarrow ((x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) : A ⟶ ω \land \forall z \exists^{*} w w (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) z)$
113	56 111 112	sylanbrc	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B)) \to (x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) : A \underset{1-1}{⟶} ω$
114		f1domg	$⊢ ω \in V \to ((x \in A ⟼ ⋂ \{n \in ran f \| f^{-1} (n) \in (𝒫 B ∖ \{\emptyset\})\}) : A \underset{1-1}{⟶} ω \to A ≼ ω)$
115	2 113 114	mpsyl	$⊢ ((b \in TopBases \land f : b \underset{1-1}{⟶} ω) \land (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B)) \to A ≼ ω$
116	115	ex	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to ((\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω)$
117		difeq1	$⊢ topGen (b) = J \to topGen (b) ∖ \{\emptyset\} = J ∖ \{\emptyset\}$
118	117	eleq2d	$⊢ topGen (b) = J \to (B \in (topGen (b) ∖ \{\emptyset\}) \leftrightarrow B \in (J ∖ \{\emptyset\}))$
119	118	ralbidv	$⊢ topGen (b) = J \to (\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \leftrightarrow \forall x \in A B \in (J ∖ \{\emptyset\}))$
120	119	anbi1d	$⊢ topGen (b) = J \to ((\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{} x \in A y \in B) \leftrightarrow (\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{} x \in A y \in B))$
121	120	imbi1d	$⊢ topGen (b) = J \to (((\forall x \in A B \in (topGen (b) ∖ \{\emptyset\}) \land \forall y \exists^{} x \in A y \in B) \to A ≼ ω) \leftrightarrow ((\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{} x \in A y \in B) \to A ≼ ω))$
122	116 121	syl5ibcom	$⊢ (b \in TopBases \land f : b \underset{1-1}{⟶} ω) \to (topGen (b) = J \to ((\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω))$
123	122	ex	$⊢ b \in TopBases \to (f : b \underset{1-1}{⟶} ω \to (topGen (b) = J \to ((\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω)))$
124	123	exlimdv	$⊢ b \in TopBases \to (\exists f f : b \underset{1-1}{⟶} ω \to (topGen (b) = J \to ((\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω)))$
125	3 124	syl5bi	$⊢ b \in TopBases \to (b ≼ ω \to (topGen (b) = J \to ((\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω)))$
126	125	impd	$⊢ b \in TopBases \to ((b ≼ ω \land topGen (b) = J) \to ((\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω))$
127	126	rexlimiv	$⊢ \exists b \in TopBases (b ≼ ω \land topGen (b) = J) \to ((\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω)$
128	1 127	sylbi	$⊢ J \in 2^{nd} 𝜔 \to ((\forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω)$
129	128	3impib	$⊢ (J \in 2^{nd} 𝜔 \land \forall x \in A B \in (J ∖ \{\emptyset\}) \land \forall y \exists^{*} x \in A y \in B) \to A ≼ ω$

Metamath Proof Explorer

Theorem 2ndcdisj

Proof