Metamath Proof Explorer

Theorem ustbas2

Description: Second direction for ustbas . (Contributed by Thierry Arnoux, 16-Nov-2017)

		Ref	Expression
	Assertion	ustbas2	$⊢ U \in UnifOn (X) \to X = dom ⋃ U$

Proof

Step	Hyp	Ref	Expression
1		dmxpid	$⊢ dom (X \times X) = X$
2		ustbasel	$⊢ U \in UnifOn (X) \to X \times X \in U$
3		elssuni	$⊢ X \times X \in U \to X \times X \subseteq ⋃ U$
4	2 3	syl	$⊢ U \in UnifOn (X) \to X \times X \subseteq ⋃ U$
5		elfvex	$⊢ U \in UnifOn (X) \to X \in V$
6		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))))$
7	5 6	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))))$
8	7	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)))$
9	8	simp1d	$⊢ U \in UnifOn (X) \to U \subseteq 𝒫 (X \times X)$
10	9	unissd	$⊢ U \in UnifOn (X) \to ⋃ U \subseteq ⋃ 𝒫 (X \times X)$
11		unipw	$⊢ ⋃ 𝒫 (X \times X) = X \times X$
12	10 11	sseqtrdi	$⊢ U \in UnifOn (X) \to ⋃ U \subseteq X \times X$
13	4 12	eqssd	$⊢ U \in UnifOn (X) \to X \times X = ⋃ U$
14	13	dmeqd	$⊢ U \in UnifOn (X) \to dom (X \times X) = dom ⋃ U$
15	1 14	eqtr3id	$⊢ U \in UnifOn (X) \to X = dom ⋃ U$