isusp

Description: The predicate W is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017)

	Ref	Expression
Hypotheses	isusp.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
	isusp.2	⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
	isusp.3	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion	isusp	⊢ ( 𝑊 ∈ UnifSp ↔ ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐽 = ( unifTop ‘ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isusp.1	⊢ 𝐵 = ( Base ‘ 𝑊 )
2		isusp.2	⊢ 𝑈 = ( UnifSt ‘ 𝑊 )
3		isusp.3	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
4		elex	⊢ ( 𝑊 ∈ UnifSp → 𝑊 ∈ V )
5		0nep0	⊢ ∅ ≠ { ∅ }
6		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( Base ‘ 𝑊 ) = ∅ )
7	1 6	eqtrid	⊢ ( ¬ 𝑊 ∈ V → 𝐵 = ∅ )
8	7	fveq2d	⊢ ( ¬ 𝑊 ∈ V → ( UnifOn ‘ 𝐵 ) = ( UnifOn ‘ ∅ ) )
9		ust0	⊢ ( UnifOn ‘ ∅ ) = { { ∅ } }
10	8 9	eqtrdi	⊢ ( ¬ 𝑊 ∈ V → ( UnifOn ‘ 𝐵 ) = { { ∅ } } )
11	10	eleq2d	⊢ ( ¬ 𝑊 ∈ V → ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ↔ 𝑈 ∈ { { ∅ } } ) )
12	2	fvexi	⊢ 𝑈 ∈ V
13	12	elsn	⊢ ( 𝑈 ∈ { { ∅ } } ↔ 𝑈 = { ∅ } )
14	11 13	bitrdi	⊢ ( ¬ 𝑊 ∈ V → ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ↔ 𝑈 = { ∅ } ) )
15		fvprc	⊢ ( ¬ 𝑊 ∈ V → ( UnifSt ‘ 𝑊 ) = ∅ )
16	2 15	eqtrid	⊢ ( ¬ 𝑊 ∈ V → 𝑈 = ∅ )
17	16	eqeq1d	⊢ ( ¬ 𝑊 ∈ V → ( 𝑈 = { ∅ } ↔ ∅ = { ∅ } ) )
18	14 17	bitrd	⊢ ( ¬ 𝑊 ∈ V → ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ↔ ∅ = { ∅ } ) )
19	18	necon3bbid	⊢ ( ¬ 𝑊 ∈ V → ( ¬ 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ↔ ∅ ≠ { ∅ } ) )
20	5 19	mpbiri	⊢ ( ¬ 𝑊 ∈ V → ¬ 𝑈 ∈ ( UnifOn ‘ 𝐵 ) )
21	20	con4i	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) → 𝑊 ∈ V )
22	21	adantr	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐽 = ( unifTop ‘ 𝑈 ) ) → 𝑊 ∈ V )
23		fveq2	⊢ ( 𝑤 = 𝑊 → ( UnifSt ‘ 𝑤 ) = ( UnifSt ‘ 𝑊 ) )
24	23 2	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( UnifSt ‘ 𝑤 ) = 𝑈 )
25		fveq2	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑊 ) )
26	25 1	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( Base ‘ 𝑤 ) = 𝐵 )
27	26	fveq2d	⊢ ( 𝑤 = 𝑊 → ( UnifOn ‘ ( Base ‘ 𝑤 ) ) = ( UnifOn ‘ 𝐵 ) )
28	24 27	eleq12d	⊢ ( 𝑤 = 𝑊 → ( ( UnifSt ‘ 𝑤 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑤 ) ) ↔ 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ) )
29		fveq2	⊢ ( 𝑤 = 𝑊 → ( TopOpen ‘ 𝑤 ) = ( TopOpen ‘ 𝑊 ) )
30	29 3	eqtr4di	⊢ ( 𝑤 = 𝑊 → ( TopOpen ‘ 𝑤 ) = 𝐽 )
31	24	fveq2d	⊢ ( 𝑤 = 𝑊 → ( unifTop ‘ ( UnifSt ‘ 𝑤 ) ) = ( unifTop ‘ 𝑈 ) )
32	30 31	eqeq12d	⊢ ( 𝑤 = 𝑊 → ( ( TopOpen ‘ 𝑤 ) = ( unifTop ‘ ( UnifSt ‘ 𝑤 ) ) ↔ 𝐽 = ( unifTop ‘ 𝑈 ) ) )
33	28 32	anbi12d	⊢ ( 𝑤 = 𝑊 → ( ( ( UnifSt ‘ 𝑤 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑤 ) ) ∧ ( TopOpen ‘ 𝑤 ) = ( unifTop ‘ ( UnifSt ‘ 𝑤 ) ) ) ↔ ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐽 = ( unifTop ‘ 𝑈 ) ) ) )
34		df-usp	⊢ UnifSp = { 𝑤 ∣ ( ( UnifSt ‘ 𝑤 ) ∈ ( UnifOn ‘ ( Base ‘ 𝑤 ) ) ∧ ( TopOpen ‘ 𝑤 ) = ( unifTop ‘ ( UnifSt ‘ 𝑤 ) ) ) }
35	33 34	elab2g	⊢ ( 𝑊 ∈ V → ( 𝑊 ∈ UnifSp ↔ ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐽 = ( unifTop ‘ 𝑈 ) ) ) )
36	4 22 35	pm5.21nii	⊢ ( 𝑊 ∈ UnifSp ↔ ( 𝑈 ∈ ( UnifOn ‘ 𝐵 ) ∧ 𝐽 = ( unifTop ‘ 𝑈 ) ) )

Metamath Proof Explorer

Theorem isusp

Proof