ustssel

Description: A uniform structure is upward closed. Condition F_I of BourbakiTop1 p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017) (Proof shortened by AV, 17-Sep-2021)

		Ref	Expression
	Assertion	ustssel	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to (V \subseteq W \to W \in U)$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to U \in UnifOn (X)$
2	1	elfvexd	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to X \in V$
3		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))))$
4	2 3	syl	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times 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))))$
5	1 4	mpbid	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times 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	simp3d	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times 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))$
7		simp1	$⊢ (\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)) \to \forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U)$
8	7	ralimi	$⊢ \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)) \to \forall v \in U \forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U)$
9	6 8	syl	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to \forall v \in U \forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U)$
10		simp2	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to V \in U$
11	2 2	xpexd	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to X \times X \in V$
12		simp3	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to W \subseteq X \times X$
13	11 12	sselpwd	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to W \in 𝒫 (X \times X)$
14		sseq1	$⊢ v = V \to (v \subseteq w \leftrightarrow V \subseteq w)$
15	14	imbi1d	$⊢ v = V \to ((v \subseteq w \to w \in U) \leftrightarrow (V \subseteq w \to w \in U))$
16		sseq2	$⊢ w = W \to (V \subseteq w \leftrightarrow V \subseteq W)$
17		eleq1	$⊢ w = W \to (w \in U \leftrightarrow W \in U)$
18	16 17	imbi12d	$⊢ w = W \to ((V \subseteq w \to w \in U) \leftrightarrow (V \subseteq W \to W \in U))$
19	15 18	rspc2v	$⊢ (V \in U \land W \in 𝒫 (X \times X)) \to (\forall v \in U \forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \to (V \subseteq W \to W \in U))$
20	10 13 19	syl2anc	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to (\forall v \in U \forall w \in 𝒫 (X \times X) (v \subseteq w \to w \in U) \to (V \subseteq W \to W \in U))$
21	9 20	mpd	$⊢ (U \in UnifOn (X) \land V \in U \land W \subseteq X \times X) \to (V \subseteq W \to W \in U)$

Metamath Proof Explorer

Theorem ustssel

Proof