Metamath Proof Explorer

Theorem baspartn

Description: A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion baspartn ( ( 𝑃 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑃 ∈ TopBases )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑥 ∈ 𝑃 → 𝑥 ∈ 𝑃 )
2 pwidg ⊢ ( 𝑥 ∈ 𝑃 → 𝑥 ∈ 𝒫 𝑥 )
3 1 2 elind ⊢ ( 𝑥 ∈ 𝑃 → 𝑥 ∈ ( 𝑃 ∩ 𝒫 𝑥 ) )
4 elssuni ⊢ ( 𝑥 ∈ ( 𝑃 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ∪ ( 𝑃 ∩ 𝒫 𝑥 ) )
5 3 4 syl ⊢ ( 𝑥 ∈ 𝑃 → 𝑥 ⊆ ∪ ( 𝑃 ∩ 𝒫 𝑥 ) )
6 inidm ⊢ ( 𝑥 ∩ 𝑥 ) = 𝑥
7 ineq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∩ 𝑥 ) = ( 𝑥 ∩ 𝑦 ) )
8 6 7 eqtr3id ⊢ ( 𝑥 = 𝑦 → 𝑥 = ( 𝑥 ∩ 𝑦 ) )
9 8 pweqd ⊢ ( 𝑥 = 𝑦 → 𝒫 𝑥 = 𝒫 ( 𝑥 ∩ 𝑦 ) )
10 9 ineq2d ⊢ ( 𝑥 = 𝑦 → ( 𝑃 ∩ 𝒫 𝑥 ) = ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
11 10 unieqd ⊢ ( 𝑥 = 𝑦 → ∪ ( 𝑃 ∩ 𝒫 𝑥 ) = ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
12 8 11 sseq12d ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ∪ ( 𝑃 ∩ 𝒫 𝑥 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
13 5 12 syl5ibcom ⊢ ( 𝑥 ∈ 𝑃 → ( 𝑥 = 𝑦 → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
14 0ss ⊢ ∅ ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) )
15 sseq1 ⊢ ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ↔ ∅ ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
16 14 15 mpbiri ⊢ ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
17 16 a1i ⊢ ( 𝑥 ∈ 𝑃 → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
18 13 17 jaod ⊢ ( 𝑥 ∈ 𝑃 → ( ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
19 18 ralimdv ⊢ ( 𝑥 ∈ 𝑃 → ( ∀ 𝑦 ∈ 𝑃 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ∀ 𝑦 ∈ 𝑃 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
20 19 ralimia ⊢ ( ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
21 20 adantl ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) )
22 isbasisg ⊢ ( 𝑃 ∈ 𝑉 → ( 𝑃 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
23 22 adantr ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝑃 ∈ TopBases ↔ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 ∩ 𝑦 ) ⊆ ∪ ( 𝑃 ∩ 𝒫 ( 𝑥 ∩ 𝑦 ) ) ) )
24 21 23 mpbird ⊢ ( ( 𝑃 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑃 ∈ TopBases )