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 ⊢ φ → U ∈ WUni
wununi.2 ⊢ φ → A ∈ U
wunpr.3 ⊢ φ → B ∈ U
Assertion wunpr ⊢ φ → A B ∈ U

Proof

Step Hyp Ref Expression
1 wununi.1 ⊢ φ → U ∈ WUni
2 wununi.2 ⊢ φ → A ∈ U
3 wunpr.3 ⊢ φ → B ∈ U
4 iswun ⊢ U ∈ WUni → U ∈ WUni ↔ Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
5 4 ibi ⊢ U ∈ WUni → Tr ⁡ U ∧ U ≠ ∅ ∧ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
6 5 simp3d ⊢ U ∈ WUni → ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U
7 simp3 ⊢ ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U → ∀ y ∈ U x y ∈ U
8 7 ralimi ⊢ ∀ x ∈ U ⋃ x ∈ U ∧ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U → ∀ x ∈ U ∀ y ∈ U x y ∈ U
9 1 6 8 3syl ⊢ φ → ∀ x ∈ U ∀ y ∈ U x y ∈ U
10 preq1 ⊢ x = A → x y = A y
11 10 eleq1d ⊢ x = A → x y ∈ U ↔ A y ∈ U
12 preq2 ⊢ y = B → A y = A B
13 12 eleq1d ⊢ y = B → A y ∈ U ↔ A B ∈ U
14 11 13 rspc2va ⊢ A ∈ U ∧ B ∈ U ∧ ∀ x ∈ U ∀ y ∈ U x y ∈ U → A B ∈ U
15 2 3 9 14 syl21anc ⊢ φ → A B ∈ U