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 ∪ 𝑈 )