ustfilxp

Description: A uniform structure on a nonempty base is a filter. Remark 3 of BourbakiTop1 p. II.2. (Contributed by Thierry Arnoux, 15-Nov-2017) (Proof shortened by Peter Mazsa, 2-Oct-2022)

		Ref	Expression
	Assertion	ustfilxp	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to U \in Fil (X \times X)$

Proof

Step	Hyp	Ref	Expression
1		elfvex	$⊢ U \in UnifOn (X) \to X \in V$
2		isust	$⊢ X \in V \to (U \in UnifOn (X) \leftrightarrow (U \subseteq 𝒫 (X \times X) \land X \times X \in U \land \forall v \in U (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v))))$
3	1 2	syl	$⊢ U \in UnifOn (X) \to (U \in UnifOn (X) \leftrightarrow (U \subseteq 𝒫 (X \times X) \land X \times X \in U \land \forall v \in U (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v))))$
4	3	ibi	$⊢ U \in UnifOn (X) \to (U \subseteq 𝒫 (X \times X) \land X \times X \in U \land \forall v \in U (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v)))$
5	4	adantl	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to (U \subseteq 𝒫 (X \times X) \land X \times X \in U \land \forall v \in U (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v)))$
6	5	simp1d	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to U \subseteq 𝒫 (X \times X)$
7	5	simp2d	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to X \times X \in U$
8	7	ne0d	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to U \neq \emptyset$
9	5	simp3d	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to \forall v \in U (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v))$
10	9	r19.21bi	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to (\forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \land \forall w \in U v \cap w \in U \land ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v))$
11	10	simp3d	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to ({I ↾}_{X} \subseteq v \land v^{-1} \in U \land \exists w \in U w \circ w \subseteq v)$
12	11	simp1d	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to {I ↾}_{X} \subseteq v$
13		opelidres	$⊢ w \in V \to (⟨w, w⟩ \in ({I ↾}_{X}) \leftrightarrow w \in X)$
14	13	elv	$⊢ ⟨w, w⟩ \in ({I ↾}_{X}) \leftrightarrow w \in X$
15	14	biimpri	$⊢ w \in X \to ⟨w, w⟩ \in ({I ↾}_{X})$
16	15	rgen	$⊢ \forall w \in X ⟨w, w⟩ \in ({I ↾}_{X})$
17		r19.2z	$⊢ (X \neq \emptyset \land \forall w \in X ⟨w, w⟩ \in ({I ↾}_{X})) \to \exists w \in X ⟨w, w⟩ \in ({I ↾}_{X})$
18	16 17	mpan2	$⊢ X \neq \emptyset \to \exists w \in X ⟨w, w⟩ \in ({I ↾}_{X})$
19	18	ad2antrr	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to \exists w \in X ⟨w, w⟩ \in ({I ↾}_{X})$
20		ne0i	$⊢ ⟨w, w⟩ \in ({I ↾}_{X}) \to {I ↾}_{X} \neq \emptyset$
21	20	rexlimivw	$⊢ \exists w \in X ⟨w, w⟩ \in ({I ↾}_{X}) \to {I ↾}_{X} \neq \emptyset$
22	19 21	syl	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to {I ↾}_{X} \neq \emptyset$
23		ssn0	$⊢ ({I ↾}_{X} \subseteq v \land {I ↾}_{X} \neq \emptyset) \to v \neq \emptyset$
24	12 22 23	syl2anc	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to v \neq \emptyset$
25	24	nelrdva	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to \neg \emptyset \in U$
26		df-nel	$⊢ \emptyset \notin U \leftrightarrow \neg \emptyset \in U$
27	25 26	sylibr	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to \emptyset \notin U$
28	10	simp2d	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to \forall w \in U v \cap w \in U$
29	28	r19.21bi	$⊢ (((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \land w \in U) \to v \cap w \in U$
30		vex	$⊢ w \in V$
31	30	inex2	$⊢ v \cap w \in V$
32	31	pwid	$⊢ v \cap w \in 𝒫 (v \cap w)$
33	32	a1i	$⊢ (((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \land w \in U) \to v \cap w \in 𝒫 (v \cap w)$
34	29 33	elind	$⊢ (((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \land w \in U) \to v \cap w \in (U \cap 𝒫 (v \cap w))$
35	34	ne0d	$⊢ (((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \land w \in U) \to U \cap 𝒫 (v \cap w) \neq \emptyset$
36	35	ralrimiva	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to \forall w \in U U \cap 𝒫 (v \cap w) \neq \emptyset$
37	36	ralrimiva	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to \forall v \in U \forall w \in U U \cap 𝒫 (v \cap w) \neq \emptyset$
38	8 27 37	3jca	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to (U \neq \emptyset \land \emptyset \notin U \land \forall v \in U \forall w \in U U \cap 𝒫 (v \cap w) \neq \emptyset)$
39	1 1	xpexd	$⊢ U \in UnifOn (X) \to X \times X \in V$
40		isfbas	$⊢ X \times X \in V \to (U \in fBas (X \times X) \leftrightarrow (U \subseteq 𝒫 (X \times X) \land (U \neq \emptyset \land \emptyset \notin U \land \forall v \in U \forall w \in U U \cap 𝒫 (v \cap w) \neq \emptyset)))$
41	39 40	syl	$⊢ U \in UnifOn (X) \to (U \in fBas (X \times X) \leftrightarrow (U \subseteq 𝒫 (X \times X) \land (U \neq \emptyset \land \emptyset \notin U \land \forall v \in U \forall w \in U U \cap 𝒫 (v \cap w) \neq \emptyset)))$
42	41	adantl	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to (U \in fBas (X \times X) \leftrightarrow (U \subseteq 𝒫 (X \times X) \land (U \neq \emptyset \land \emptyset \notin U \land \forall v \in U \forall w \in U U \cap 𝒫 (v \cap w) \neq \emptyset)))$
43	6 38 42	mpbir2and	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to U \in fBas (X \times X)$
44		n0	$⊢ U \cap 𝒫 w \neq \emptyset \leftrightarrow \exists v v \in (U \cap 𝒫 w)$
45		elin	$⊢ v \in (U \cap 𝒫 w) \leftrightarrow (v \in U \land v \in 𝒫 w)$
46		velpw	$⊢ v \in 𝒫 w \leftrightarrow v \subseteq w$
47	46	anbi2i	$⊢ (v \in U \land v \in 𝒫 w) \leftrightarrow (v \in U \land v \subseteq w)$
48	45 47	bitri	$⊢ v \in (U \cap 𝒫 w) \leftrightarrow (v \in U \land v \subseteq w)$
49	48	exbii	$⊢ \exists v v \in (U \cap 𝒫 w) \leftrightarrow \exists v (v \in U \land v \subseteq w)$
50	44 49	bitri	$⊢ U \cap 𝒫 w \neq \emptyset \leftrightarrow \exists v (v \in U \land v \subseteq w)$
51	10	simp1d	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \to \forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U)$
52	51	r19.21bi	$⊢ (((X \neq \emptyset \land U \in UnifOn (X)) \land v \in U) \land w \in 𝒫 (X \times X)) \to (v \subseteq w \to w \in U)$
53	52	an32s	$⊢ (((X \neq \emptyset \land U \in UnifOn (X)) \land w \in 𝒫 (X \times X)) \land v \in U) \to (v \subseteq w \to w \in U)$
54	53	expimpd	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land w \in 𝒫 (X \times X)) \to ((v \in U \land v \subseteq w) \to w \in U)$
55	54	exlimdv	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land w \in 𝒫 (X \times X)) \to (\exists v (v \in U \land v \subseteq w) \to w \in U)$
56	50 55	syl5bi	$⊢ ((X \neq \emptyset \land U \in UnifOn (X)) \land w \in 𝒫 (X \times X)) \to (U \cap 𝒫 w \neq \emptyset \to w \in U)$
57	56	ralrimiva	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to \forall w \in 𝒫 (X \times X) (U \cap 𝒫 w \neq \emptyset \to w \in U)$
58		isfil	$⊢ U \in Fil (X \times X) \leftrightarrow (U \in fBas (X \times X) \land \forall w \in 𝒫 (X \times X) (U \cap 𝒫 w \neq \emptyset \to w \in U))$
59	43 57 58	sylanbrc	$⊢ (X \neq \emptyset \land U \in UnifOn (X)) \to U \in Fil (X \times X)$

Metamath Proof Explorer

Theorem ustfilxp

Proof