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

Metamath Proof Explorer

Theorem wunpr

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

Ref Expression
Hypotheses wununi.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
wununi.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
wunpr.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
Assertion wunpr ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 wununi.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
2 wununi.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3 wunpr.3 ⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
4 iswun ⊢ ( 𝑈 ∈ WUni → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )
5 4 ibi ⊢ ( 𝑈 ∈ WUni → ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) )
6 5 simp3d ⊢ ( 𝑈 ∈ WUni → ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) )
7 simp3 ⊢ ( ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 )
8 7 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 )
9 1 6 8 3syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 )
10 preq1 ⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝑦 } = { 𝐴 , 𝑦 } )
11 10 eleq1d ⊢ ( 𝑥 = 𝐴 → ( { 𝑥 , 𝑦 } ∈ 𝑈 ↔ { 𝐴 , 𝑦 } ∈ 𝑈 ) )
12 preq2 ⊢ ( 𝑦 = 𝐵 → { 𝐴 , 𝑦 } = { 𝐴 , 𝐵 } )
13 12 eleq1d ⊢ ( 𝑦 = 𝐵 → ( { 𝐴 , 𝑦 } ∈ 𝑈 ↔ { 𝐴 , 𝐵 } ∈ 𝑈 ) )
14 11 13 rspc2va ⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → { 𝐴 , 𝐵 } ∈ 𝑈 )
15 2 3 9 14 syl21anc ⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )