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	$⊢ \forall x \in A B \in V \to \underset{x \in A}{⨉} B \in V$

Proof

Step	Hyp	Ref	Expression
1		uniixp	$⊢ ⋃ \underset{x \in A}{⨉} B \subseteq A \times ⋃_{x \in A} B$
2		iunexg	$⊢ (A \in V \land \forall x \in A B \in V) \to ⋃_{x \in A} B \in V$
3		xpexg	$⊢ (A \in V \land ⋃_{x \in A} B \in V) \to A \times ⋃_{x \in A} B \in V$
4	2 3	syldan	$⊢ (A \in V \land \forall x \in A B \in V) \to A \times ⋃_{x \in A} B \in V$
5		ssexg	$⊢ (⋃ \underset{x \in A}{⨉} B \subseteq A \times ⋃_{x \in A} B \land A \times ⋃_{x \in A} B \in V) \to ⋃ \underset{x \in A}{⨉} B \in V$
6	1 4 5	sylancr	$⊢ (A \in V \land \forall x \in A B \in V) \to ⋃ \underset{x \in A}{⨉} B \in V$
7		uniexb	$⊢ \underset{x \in A}{⨉} B \in V \leftrightarrow ⋃ \underset{x \in A}{⨉} B \in V$
8	6 7	sylibr	$⊢ (A \in V \land \forall x \in A B \in V) \to \underset{x \in A}{⨉} B \in V$
9		ixpprc	$⊢ \neg A \in V \to \underset{x \in A}{⨉} B = \emptyset$
10		0ex	$⊢ \emptyset \in V$
11	9 10	eqeltrdi	$⊢ \neg A \in V \to \underset{x \in A}{⨉} B \in V$
12	11	adantr	$⊢ (\neg A \in V \land \forall x \in A B \in V) \to \underset{x \in A}{⨉} B \in V$
13	8 12	pm2.61ian	$⊢ \forall x \in A B \in V \to \underset{x \in A}{⨉} B \in V$