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

Metamath Proof Explorer

Theorem wununi

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

Ref Expression
Hypotheses wununi.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
wununi.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
Assertion wununi ( 𝜑 → ∪ 𝐴 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 wununi.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
2 wununi.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3 unieq ⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 )
4 3 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ∪ 𝑥 ∈ 𝑈 ↔ ∪ 𝐴 ∈ 𝑈 ) )
5 iswun ⊢ ( 𝑈 ∈ WUni → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )
6 5 ibi ⊢ ( 𝑈 ∈ WUni → ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) )
7 6 simp3d ⊢ ( 𝑈 ∈ WUni → ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) )
8 simp1 ⊢ ( ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝑈 )
9 8 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑈 ∪ 𝑥 ∈ 𝑈 )
10 1 7 9 3syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ∪ 𝑥 ∈ 𝑈 )
11 4 10 2 rspcdva ⊢ ( 𝜑 → ∪ 𝐴 ∈ 𝑈 )