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

Metamath Proof Explorer

Theorem xpexgALT

Description: Alternate proof of xpexg requiring Replacement ( ax-rep ) but not Power Set ( ax-pow ). (Contributed by Mario Carneiro, 20-May-2013) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	xpexgALT	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		iunid	⊢ ∪ 𝑦 ∈ 𝐵 { 𝑦 } = 𝐵
2	1	xpeq2i	⊢ ( 𝐴 × ∪ 𝑦 ∈ 𝐵 { 𝑦 } ) = ( 𝐴 × 𝐵 )
3		xpiundi	⊢ ( 𝐴 × ∪ 𝑦 ∈ 𝐵 { 𝑦 } ) = ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } )
4	2 3	eqtr3i	⊢ ( 𝐴 × 𝐵 ) = ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } )
5		id	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ 𝑊 )
6		fconstmpt	⊢ ( 𝐴 × { 𝑦 } ) = ( 𝑥 ∈ 𝐴 ↦ 𝑦 )
7		mptexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝑥 ∈ 𝐴 ↦ 𝑦 ) ∈ V )
8	6 7	eqeltrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × { 𝑦 } ) ∈ V )
9	8	ralrimivw	⊢ ( 𝐴 ∈ 𝑉 → ∀ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∈ V )
10		iunexg	⊢ ( ( 𝐵 ∈ 𝑊 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∈ V ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∈ V )
11	5 9 10	syl2anr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ∈ V )
12	4 11	eqeltrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 × 𝐵 ) ∈ V )