Theorem ustfn

Description: The defined uniform structure as a function. (Contributed by Thierry Arnoux, 15-Nov-2017)

	Ref	Expression
Assertion	ustfn	⊢ UnifOn Fn V

Proof

Step	Hyp	Ref	Expression
1		velpw	⊢ ( 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) ↔ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) )
2	1	abbii	⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } = { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) }
3		abid2	⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } = 𝒫 𝒫 ( 𝑥 × 𝑥 )
4		vex	⊢ 𝑥 ∈ V
5	4 4	xpex	⊢ ( 𝑥 × 𝑥 ) ∈ V
6	5	pwex	⊢ 𝒫 ( 𝑥 × 𝑥 ) ∈ V
7	6	pwex	⊢ 𝒫 𝒫 ( 𝑥 × 𝑥 ) ∈ V
8	3 7	eqeltri	⊢ { 𝑢 ∣ 𝑢 ∈ 𝒫 𝒫 ( 𝑥 × 𝑥 ) } ∈ V
9	2 8	eqeltrri	⊢ { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) } ∈ V
10		simp1	⊢ ( ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) )
11	10	ss2abi	⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ⊆ { 𝑢 ∣ 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) }
12	9 11	ssexi	⊢ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ∈ V
13		df-ust	⊢ UnifOn = ( 𝑥 ∈ V ↦ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑥 × 𝑥 ) ∧ ( 𝑥 × 𝑥 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑥 × 𝑥 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑥 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )
14	12 13	fnmpti	⊢ UnifOn Fn V