Metamath Proof Explorer

Theorem ustbas

Description: Recover the base of an uniform structure U . U. ran UnifOn is to UnifOn what Top is to TopOn . (Contributed by Thierry Arnoux, 16-Nov-2017)

		Ref	Expression
	Hypothesis	ustbas.1	$⊢ X = dom ⋃ U$
	Assertion	ustbas	$⊢ U \in ⋃ ran UnifOn \leftrightarrow U \in UnifOn (X)$

Proof

Step	Hyp	Ref	Expression
1		ustbas.1	$⊢ X = dom ⋃ U$
2		ustfn	$⊢ UnifOn Fn V$
3		fnfun	$⊢ UnifOn Fn V \to Fun UnifOn$
4		elunirn	$⊢ Fun UnifOn \to (U \in ⋃ ran UnifOn \leftrightarrow \exists x \in dom UnifOn U \in UnifOn (x))$
5	2 3 4	mp2b	$⊢ U \in ⋃ ran UnifOn \leftrightarrow \exists x \in dom UnifOn U \in UnifOn (x)$
6		ustbas2	$⊢ U \in UnifOn (x) \to x = dom ⋃ U$
7	6 1	eqtr4di	$⊢ U \in UnifOn (x) \to x = X$
8	7	fveq2d	$⊢ U \in UnifOn (x) \to UnifOn (x) = UnifOn (X)$
9	8	eleq2d	$⊢ U \in UnifOn (x) \to (U \in UnifOn (x) \leftrightarrow U \in UnifOn (X))$
10	9	ibi	$⊢ U \in UnifOn (x) \to U \in UnifOn (X)$
11	10	rexlimivw	$⊢ \exists x \in dom UnifOn U \in UnifOn (x) \to U \in UnifOn (X)$
12	5 11	sylbi	$⊢ U \in ⋃ ran UnifOn \to U \in UnifOn (X)$
13		elfvunirn	$⊢ U \in UnifOn (X) \to U \in ⋃ ran UnifOn$
14	12 13	impbii	$⊢ U \in ⋃ ran UnifOn \leftrightarrow U \in UnifOn (X)$