This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ussid

Description: In case the base of the UnifSt element of the uniform space is the base of its element structure, then UnifSt does not restrict it further. (Contributed by Thierry Arnoux, 4-Dec-2017)

		Ref	Expression
	Hypotheses	ussval.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
		ussval.2	⊢ 𝑈 = ( UnifSet ‘ 𝑊 )
	Assertion	ussid	⊢ ( ( 𝐵 × 𝐵 ) = ∪ 𝑈 → 𝑈 = ( UnifSt ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		ussval.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		ussval.2	⊢ 𝑈 = ( UnifSet ‘ 𝑊 )
3		oveq2	⊢ ( ( 𝐵 × 𝐵 ) = ∪ 𝑈 → ( 𝑈 ↾_t ( 𝐵 × 𝐵 ) ) = ( 𝑈 ↾_t ∪ 𝑈 ) )
4		id	⊢ ( ( 𝐵 × 𝐵 ) = ∪ 𝑈 → ( 𝐵 × 𝐵 ) = ∪ 𝑈 )
5	1	fvexi	⊢ 𝐵 ∈ V
6	5 5	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
7	4 6	eqeltrrdi	⊢ ( ( 𝐵 × 𝐵 ) = ∪ 𝑈 → ∪ 𝑈 ∈ V )
8		uniexb	⊢ ( 𝑈 ∈ V ↔ ∪ 𝑈 ∈ V )
9	7 8	sylibr	⊢ ( ( 𝐵 × 𝐵 ) = ∪ 𝑈 → 𝑈 ∈ V )
10		eqid	⊢ ∪ 𝑈 = ∪ 𝑈
11	10	restid	⊢ ( 𝑈 ∈ V → ( 𝑈 ↾_t ∪ 𝑈 ) = 𝑈 )
12	9 11	syl	⊢ ( ( 𝐵 × 𝐵 ) = ∪ 𝑈 → ( 𝑈 ↾_t ∪ 𝑈 ) = 𝑈 )
13	3 12	eqtr2d	⊢ ( ( 𝐵 × 𝐵 ) = ∪ 𝑈 → 𝑈 = ( 𝑈 ↾_t ( 𝐵 × 𝐵 ) ) )
14	1 2	ussval	⊢ ( 𝑈 ↾_t ( 𝐵 × 𝐵 ) ) = ( UnifSt ‘ 𝑊 )
15	13 14	eqtrdi	⊢ ( ( 𝐵 × 𝐵 ) = ∪ 𝑈 → 𝑈 = ( UnifSt ‘ 𝑊 ) )