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

Metamath Proof Explorer

Theorem ustbas2

Description: Second direction for ustbas . (Contributed by Thierry Arnoux, 16-Nov-2017)

Ref Expression
Assertion ustbas2 ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 )

Proof

Step Hyp Ref Expression
1 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
2 ustbasel ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) ∈ 𝑈 )
3 elssuni ⊢ ( ( 𝑋 × 𝑋 ) ∈ 𝑈 → ( 𝑋 × 𝑋 ) ⊆ ∪ 𝑈 )
4 2 3 syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) ⊆ ∪ 𝑈 )
5 elfvex ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
6 isust ⊢ ( 𝑋 ∈ V → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
7 5 6 syl ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
8 7 ibi ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) )
9 8 simp1d ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) )
10 9 unissd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ 𝑈 ⊆ ∪ 𝒫 ( 𝑋 × 𝑋 ) )
11 unipw ⊢ ∪ 𝒫 ( 𝑋 × 𝑋 ) = ( 𝑋 × 𝑋 )
12 10 11 sseqtrdi ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∪ 𝑈 ⊆ ( 𝑋 × 𝑋 ) )
13 4 12 eqssd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑋 × 𝑋 ) = ∪ 𝑈 )
14 13 dmeqd ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → dom ( 𝑋 × 𝑋 ) = dom ∪ 𝑈 )
15 1 14 eqtr3id ⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 )