Theorem ixpexg 8913

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

Assertion

Ref	Expression
ixpexg	⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ∈ V)

Distinct variable group:   𝑥,𝐴

Allowed substitution hints:   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem ixpexg

Step	Hyp	Ref	Expression
1		uniixp 8912	. . . 4 ⊢ ∪ X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵)
2		iunexg 7944	. . . . 5 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V)
3		xpexg 7731	. . . . 5 ⊢ ((𝐴 ∈ V ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ V) → (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵) ∈ V)
4	2, 3	syldan 590	. . . 4 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵) ∈ V)
5		ssexg 5314	. . . 4 ⊢ ((∪ X𝑥 ∈ 𝐴 𝐵 ⊆ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝐴 × ∪ 𝑥 ∈ 𝐴 𝐵) ∈ V) → ∪ X𝑥 ∈ 𝐴 𝐵 ∈ V)
6	1, 4, 5	sylancr 586	. . 3 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → ∪ X𝑥 ∈ 𝐴 𝐵 ∈ V)
7		uniexb 7745	. . 3 ⊢ (X𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∪ X𝑥 ∈ 𝐴 𝐵 ∈ V)
8	6, 7	sylibr 233	. 2 ⊢ ((𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → X𝑥 ∈ 𝐴 𝐵 ∈ V)
9		ixpprc 8910	. . . 4 ⊢ (¬ 𝐴 ∈ V → X𝑥 ∈ 𝐴 𝐵 = ∅)
10		0ex 5298	. . . 4 ⊢ ∅ ∈ V
11	9, 10	eqeltrdi 2833	. . 3 ⊢ (¬ 𝐴 ∈ V → X𝑥 ∈ 𝐴 𝐵 ∈ V)
12	11	adantr 480	. 2 ⊢ ((¬ 𝐴 ∈ V ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉) → X𝑥 ∈ 𝐴 𝐵 ∈ V)
13	8, 12	pm2.61ian 809	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → X𝑥 ∈ 𝐴 𝐵 ∈ V)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2098  ∀wral 3053  Vcvv 3466   ⊆ wss 3941  ∅c0 4315  ∪ cuni 4900  ∪ ciun 4988   × cxp 5665  Xcixp 8888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-fv 6542  df-ixp 8889

This theorem is referenced by:  konigthlem  10560  prdsbasex  17397  isfunc  17815  isnat  17902  natffn  17904  dmdprd  19912  dprdval  19917  elpt  23400  ptbasin2  23406  ptbasfi  23409  ptrest  36981  upixp  37091  hspval  45835  hspmbl  45855  vonioolem2  45907  vonicclem2  45910