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

Metamath Proof Explorer

Theorem wunint

Description: A weak universe is closed under nonempty intersections. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses wununi.1 ⊢ φ → U ∈ WUni
wununi.2 ⊢ φ → A ∈ U
Assertion wunint ⊢ φ ∧ A ≠ ∅ → ⋂ A ∈ U

Proof

Step Hyp Ref Expression
1 wununi.1 ⊢ φ → U ∈ WUni
2 wununi.2 ⊢ φ → A ∈ U
3 1 adantr ⊢ φ ∧ A ≠ ∅ → U ∈ WUni
4 1 2 wununi ⊢ φ → ⋃ A ∈ U
5 4 adantr ⊢ φ ∧ A ≠ ∅ → ⋃ A ∈ U
6 intssuni ⊢ A ≠ ∅ → ⋂ A ⊆ ⋃ A
7 6 adantl ⊢ φ ∧ A ≠ ∅ → ⋂ A ⊆ ⋃ A
8 3 5 7 wunss ⊢ φ ∧ A ≠ ∅ → ⋂ A ∈ U