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

Theorem indexa 33658
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 4844 . 2 (𝐵𝑀 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2 ssrab2 3720 . . . 4 {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
32a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4 nfv 1883 . . . . 5 𝑦 𝑥𝐴
5 nfre1 3034 . . . . 5 𝑦𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6 sbceq2a 3480 . . . . . . . . . . . . . . 15 (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑𝜑))
76rspcev 3340 . . . . . . . . . . . . . 14 ((𝑥𝐴𝜑) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
87ancoms 468 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
98anim2i 592 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝜑𝑥𝐴)) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
109ancoms 468 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1110anasss 680 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1211ancoms 468 . . . . . . . . 9 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
13 sbceq2a 3480 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑𝜑))
1413sbcbidv 3523 . . . . . . . . . . 11 (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑[𝑤 / 𝑥]𝜑))
1514rexbidv 3081 . . . . . . . . . 10 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1615elrab 3396 . . . . . . . . 9 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1712, 16sylibr 224 . . . . . . . 8 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑})
18 sbceq2a 3480 . . . . . . . . 9 (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑𝜑))
1918rspcev 3340 . . . . . . . 8 ((𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
2017, 19sylancom 702 . . . . . . 7 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
21 nfcv 2793 . . . . . . . 8 𝑣{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
22 nfcv 2793 . . . . . . . . . 10 𝑦𝐴
23 nfcv 2793 . . . . . . . . . . 11 𝑦𝑤
24 nfsbc1v 3488 . . . . . . . . . . 11 𝑦[𝑧 / 𝑦]𝜑
2523, 24nfsbc 3490 . . . . . . . . . 10 𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
2622, 25nfrex 3036 . . . . . . . . 9 𝑦𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
27 nfcv 2793 . . . . . . . . 9 𝑦𝐵
2826, 27nfrab 3153 . . . . . . . 8 𝑦{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
29 nfsbc1v 3488 . . . . . . . 8 𝑦[𝑣 / 𝑦]𝜑
30 nfv 1883 . . . . . . . 8 𝑣𝜑
3121, 28, 29, 30, 18cbvrexf 3196 . . . . . . 7 (∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3220, 31sylib 208 . . . . . 6 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3332exp31 629 . . . . 5 (𝑥𝐴 → (𝑦𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
344, 5, 33rexlimd 3055 . . . 4 (𝑥𝐴 → (∃𝑦𝐵 𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
3534ralimia 2979 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
36 nfsbc1v 3488 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
37 nfv 1883 . . . . . . . . 9 𝑤𝜑
3836, 37, 6cbvrex 3198 . . . . . . . 8 (∃𝑤𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥𝐴 𝜑)
3915, 38syl6bb 276 . . . . . . 7 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥𝐴 𝜑))
4039elrab 3396 . . . . . 6 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
4140simprbi 479 . . . . 5 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥𝐴 𝜑)
4241rgen 2951 . . . 4 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑
4342a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)
443, 35, 433jca 1261 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 → ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
45 sseq1 3659 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐𝐵 ↔ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
46 nfcv 2793 . . . . . . . . 9 𝑥𝐴
47 nfsbc1v 3488 . . . . . . . . 9 𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
4846, 47nfrex 3036 . . . . . . . 8 𝑥𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
49 nfcv 2793 . . . . . . . 8 𝑥𝐵
5048, 49nfrab 3153 . . . . . . 7 𝑥{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
5150nfeq2 2809 . . . . . 6 𝑥 𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
52 nfcv 2793 . . . . . . 7 𝑦𝑐
5352, 28rexeqf 3165 . . . . . 6 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5451, 53ralbid 3012 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥𝐴𝑦𝑐 𝜑 ↔ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5552, 28raleqf 3164 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦𝑐𝑥𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
5645, 54, 553anbi123d 1439 . . . 4 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑) ↔ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)))
5756spcegv 3325 . . 3 ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
5857imp 444 . 2 (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
591, 44, 58syl2an 493 1 ((𝐵𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054   = wceq 1523  wex 1744  wcel 2030  wral 2941  wrex 2942  {crab 2945  Vcvv 3231  [wsbc 3468  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-in 3614  df-ss 3621
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator