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 𝑥 ∈ 𝐴 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		uniixp	⊢ ∪ X 𝑥 ∈ 𝐴 𝐵 ⊆ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 )
2		iunexg	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V )
3		xpexg	⊢ ( ( 𝐴 ∈ V ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V ) → ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ V )
4	2 3	syldan	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ V )
5		ssexg	⊢ ( ( ∪ X 𝑥 ∈ 𝐴 𝐵 ⊆ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵 ) ∈ V ) → ∪ X 𝑥 ∈ 𝐴 𝐵 ∈ V )
6	1 4 5	sylancr	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → ∪ X 𝑥 ∈ 𝐴 𝐵 ∈ V )
7		uniexb	⊢ ( X 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∪ X 𝑥 ∈ 𝐴 𝐵 ∈ V )
8	6 7	sylibr	⊢ ( ( 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → X 𝑥 ∈ 𝐴 𝐵 ∈ V )
9		ixpprc	⊢ ( ¬ 𝐴 ∈ V → X 𝑥 ∈ 𝐴 𝐵 = ∅ )
10		0ex	⊢ ∅ ∈ V
11	9 10	eqeltrdi	⊢ ( ¬ 𝐴 ∈ V → X 𝑥 ∈ 𝐴 𝐵 ∈ V )
12	11	adantr	⊢ ( ( ¬ 𝐴 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 ) → X 𝑥 ∈ 𝐴 𝐵 ∈ V )
13	8 12	pm2.61ian	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X 𝑥 ∈ 𝐴 𝐵 ∈ V )