Metamath Proof Explorer

Theorem gruxp

Description: A Grothendieck universe contains binary cartesian products of its elements. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion gruxp ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A × B ∈ U

Proof

Step Hyp Ref Expression
1 gruun ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A ∪ B ∈ U
2 grupw ⊢ U ∈ Univ ∧ A ∪ B ∈ U → 𝒫 A ∪ B ∈ U
3 grupw ⊢ U ∈ Univ ∧ 𝒫 A ∪ B ∈ U → 𝒫 𝒫 A ∪ B ∈ U
4 xpsspw ⊢ A × B ⊆ 𝒫 𝒫 A ∪ B
5 gruss ⊢ U ∈ Univ ∧ 𝒫 𝒫 A ∪ B ∈ U ∧ A × B ⊆ 𝒫 𝒫 A ∪ B → A × B ∈ U
6 4 5 mp3an3 ⊢ U ∈ Univ ∧ 𝒫 𝒫 A ∪ B ∈ U → A × B ∈ U
7 3 6 syldan ⊢ U ∈ Univ ∧ 𝒫 A ∪ B ∈ U → A × B ∈ U
8 2 7 syldan ⊢ U ∈ Univ ∧ A ∪ B ∈ U → A × B ∈ U
9 8 3ad2antl1 ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U ∧ A ∪ B ∈ U → A × B ∈ U
10 1 9 mpdan ⊢ U ∈ Univ ∧ A ∈ U ∧ B ∈ U → A × B ∈ U