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

Metamath Proof Explorer

Theorem ixpexg

Description: The existence of an infinite Cartesian product. x is normally a free-variable parameter in B . Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006) (Revised by Mario Carneiro, 25-Jan-2015)

Ref Expression
Assertion ixpexg ⊢ ∀ x ∈ A B ∈ V → ⨉ x ∈ A B ∈ V

Proof

Step Hyp Ref Expression
1 uniixp ⊢ ⋃ ⨉ x ∈ A B ⊆ A × ⋃ x ∈ A B
2 iunexg ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ V → ⋃ x ∈ A B ∈ V
3 xpexg ⊢ A ∈ V ∧ ⋃ x ∈ A B ∈ V → A × ⋃ x ∈ A B ∈ V
4 2 3 syldan ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ V → A × ⋃ x ∈ A B ∈ V
5 ssexg ⊢ ⋃ ⨉ x ∈ A B ⊆ A × ⋃ x ∈ A B ∧ A × ⋃ x ∈ A B ∈ V → ⋃ ⨉ x ∈ A B ∈ V
6 1 4 5 sylancr ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ V → ⋃ ⨉ x ∈ A B ∈ V
7 uniexb ⊢ ⨉ x ∈ A B ∈ V ↔ ⋃ ⨉ x ∈ A B ∈ V
8 6 7 sylibr ⊢ A ∈ V ∧ ∀ x ∈ A B ∈ V → ⨉ x ∈ A B ∈ V
9 ixpprc ⊢ ¬ A ∈ V → ⨉ x ∈ A B = ∅
10 0ex ⊢ ∅ ∈ V
11 9 10 eqeltrdi ⊢ ¬ A ∈ V → ⨉ x ∈ A B ∈ V
12 11 adantr ⊢ ¬ A ∈ V ∧ ∀ x ∈ A B ∈ V → ⨉ x ∈ A B ∈ V
13 8 12 pm2.61ian ⊢ ∀ x ∈ A B ∈ V → ⨉ x ∈ A B ∈ V