Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  indexa Structured version   Visualization version   GIF version

Theorem indexa 32698
 Description: If for every element of an indexing set 𝐴 there exists a corresponding element of another set 𝐵, then there exists a subset of 𝐵 consisting only of those elements which are indexed by 𝐴. Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
indexa ((𝐵𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑐   𝑥,𝐵,𝑦,𝑐   𝜑,𝑐
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑀(𝑥,𝑦,𝑐)

Proof of Theorem indexa
Dummy variables 𝑧 𝑤 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rabexg 4739 . 2 (𝐵𝑀 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2 ssrab2 3650 . . . 4 {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
32a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4 nfv 1830 . . . . 5 𝑦 𝑥𝐴
5 nfre1 2988 . . . . 5 𝑦𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6 sbceq2a 3414 . . . . . . . . . . . . . . 15 (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑𝜑))
76rspcev 3282 . . . . . . . . . . . . . 14 ((𝑥𝐴𝜑) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
87ancoms 468 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
98anim2i 591 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝜑𝑥𝐴)) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
109ancoms 468 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1110anasss 677 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1211ancoms 468 . . . . . . . . 9 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
13 sbceq2a 3414 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑𝜑))
1413sbcbidv 3457 . . . . . . . . . . 11 (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑[𝑤 / 𝑥]𝜑))
1514rexbidv 3034 . . . . . . . . . 10 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1615elrab 3331 . . . . . . . . 9 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1712, 16sylibr 223 . . . . . . . 8 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑})
18 sbceq2a 3414 . . . . . . . . 9 (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑𝜑))
1918rspcev 3282 . . . . . . . 8 ((𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
2017, 19sylancom 698 . . . . . . 7 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
21 nfcv 2751 . . . . . . . 8 𝑣{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
22 nfcv 2751 . . . . . . . . . 10 𝑦𝐴
23 nfcv 2751 . . . . . . . . . . 11 𝑦𝑤
24 nfsbc1v 3422 . . . . . . . . . . 11 𝑦[𝑧 / 𝑦]𝜑
2523, 24nfsbc 3424 . . . . . . . . . 10 𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
2622, 25nfrex 2990 . . . . . . . . 9 𝑦𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
27 nfcv 2751 . . . . . . . . 9 𝑦𝐵
2826, 27nfrab 3100 . . . . . . . 8 𝑦{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
29 nfsbc1v 3422 . . . . . . . 8 𝑦[𝑣 / 𝑦]𝜑
30 nfv 1830 . . . . . . . 8 𝑣𝜑
3121, 28, 29, 30, 18cbvrexf 3142 . . . . . . 7 (∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3220, 31sylib 207 . . . . . 6 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3332exp31 628 . . . . 5 (𝑥𝐴 → (𝑦𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
344, 5, 33rexlimd 3008 . . . 4 (𝑥𝐴 → (∃𝑦𝐵 𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
3534ralimia 2934 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
36 nfsbc1v 3422 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
37 nfv 1830 . . . . . . . . 9 𝑤𝜑
3836, 37, 6cbvrex 3144 . . . . . . . 8 (∃𝑤𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥𝐴 𝜑)
3915, 38syl6bb 275 . . . . . . 7 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥𝐴 𝜑))
4039elrab 3331 . . . . . 6 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
4140simprbi 479 . . . . 5 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥𝐴 𝜑)
4241rgen 2906 . . . 4 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑
4342a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)
443, 35, 433jca 1235 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 → ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
45 sseq1 3589 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐𝐵 ↔ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
46 nfcv 2751 . . . . . . . . 9 𝑥𝐴
47 nfsbc1v 3422 . . . . . . . . 9 𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
4846, 47nfrex 2990 . . . . . . . 8 𝑥𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
49 nfcv 2751 . . . . . . . 8 𝑥𝐵
5048, 49nfrab 3100 . . . . . . 7 𝑥{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
5150nfeq2 2766 . . . . . 6 𝑥 𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
52 nfcv 2751 . . . . . . 7 𝑦𝑐
5352, 28rexeqf 3112 . . . . . 6 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5451, 53ralbid 2966 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥𝐴𝑦𝑐 𝜑 ↔ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5552, 28raleqf 3111 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦𝑐𝑥𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
5645, 54, 553anbi123d 1391 . . . 4 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑) ↔ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)))
5756spcegv 3267 . . 3 ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
5857imp 444 . 2 (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
591, 44, 58syl2an 493 1 ((𝐵𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173  [wsbc 3402   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-in 3547  df-ss 3554 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator