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

Metamath Proof Explorer

Theorem isust

Description: The predicate " U is a uniform structure with base X ". (Contributed by Thierry Arnoux, 15-Nov-2017) (Revised by AV, 17-Sep-2021)

Ref Expression
Assertion isust ( 𝑋 ∈ 𝑉 → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ustval ⊢ ( 𝑋 ∈ 𝑉 → ( UnifOn ‘ 𝑋 ) = { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } )
2 1 eleq2d ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ 𝑈 ∈ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ) )
3 simp1 ⊢ ( ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
4 sqxpexg ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑋 × 𝑋 ) ∈ V )
5 4 pwexd ⊢ ( 𝑋 ∈ 𝑉 → 𝒫 ( 𝑋 × 𝑋 ) ∈ V )
6 5 adantr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ) → 𝒫 ( 𝑋 × 𝑋 ) ∈ V )
7 simpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ) → 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
8 6 7 ssexd ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ) → 𝑈 ∈ V )
9 8 ex ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) → 𝑈 ∈ V ) )
10 3 9 syl5 ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → 𝑈 ∈ V ) )
11 sseq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ↔ 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ) )
12 eleq2 ⊢ ( 𝑢 = 𝑈 → ( ( 𝑋 × 𝑋 ) ∈ 𝑢 ↔ ( 𝑋 × 𝑋 ) ∈ 𝑈 ) )
13 eleq2 ⊢ ( 𝑢 = 𝑈 → ( 𝑤 ∈ 𝑢 ↔ 𝑤 ∈ 𝑈 ) )
14 13 imbi2d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ↔ ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ) )
15 14 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ↔ ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ) )
16 eleq2 ⊢ ( 𝑢 = 𝑈 → ( ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ↔ ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ) )
17 16 raleqbi1dv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ↔ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ) )
18 eleq2 ⊢ ( 𝑢 = 𝑈 → ( ◡ 𝑣 ∈ 𝑢 ↔ ◡ 𝑣 ∈ 𝑈 ) )
19 rexeq ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ↔ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) )
20 18 19 3anbi23d ⊢ ( 𝑢 = 𝑈 → ( ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ↔ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) )
21 15 17 20 3anbi123d ⊢ ( 𝑢 = 𝑈 → ( ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ↔ ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) )
22 21 raleqbi1dv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ↔ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) )
23 11 12 22 3anbi123d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
24 23 elab3g ⊢ ( ( ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) → 𝑈 ∈ V ) → ( 𝑈 ∈ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
25 10 24 syl ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑈 ∈ { 𝑢 ∣ ( 𝑢 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) } ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
26 2 25 bitrd ⊢ ( 𝑋 ∈ 𝑉 → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )