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	⊢ 𝑋 = dom ∪ 𝑈
Assertion	ustbas	⊢ ( 𝑈 ∈ ∪ ran UnifOn ↔ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ustbas.1	⊢ 𝑋 = dom ∪ 𝑈
2		ustfn	⊢ UnifOn Fn V
3		fnfun	⊢ ( UnifOn Fn V → Fun UnifOn )
4		elunirn	⊢ ( Fun UnifOn → ( 𝑈 ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) ) )
5	2 3 4	mp2b	⊢ ( 𝑈 ∈ ∪ ran UnifOn ↔ ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) )
6		ustbas2	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → 𝑥 = dom ∪ 𝑈 )
7	6 1	eqtr4di	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → 𝑥 = 𝑋 )
8	7	fveq2d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → ( UnifOn ‘ 𝑥 ) = ( UnifOn ‘ 𝑋 ) )
9	8	eleq2d	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) ↔ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ) )
10	9	ibi	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
11	10	rexlimivw	⊢ ( ∃ 𝑥 ∈ dom UnifOn 𝑈 ∈ ( UnifOn ‘ 𝑥 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
12	5 11	sylbi	⊢ ( 𝑈 ∈ ∪ ran UnifOn → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
13		elrnust	⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn )
14	12 13	impbii	⊢ ( 𝑈 ∈ ∪ ran UnifOn ↔ 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )