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

Theorem indexa 35487
 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 5206 . 2 (𝐵𝑀 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2 ssrab2 3987 . . . 4 {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
32a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4 nfv 1916 . . . . 5 𝑦 𝑥𝐴
5 nfre1 3231 . . . . 5 𝑦𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6 sbceq2a 3711 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑𝜑))
76rspcev 3544 . . . . . . . . . . . . 13 ((𝑥𝐴𝜑) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
87ancoms 462 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
98anim1ci 618 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
109anasss 470 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1110ancoms 462 . . . . . . . . 9 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
12 sbceq2a 3711 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑𝜑))
1312sbcbidv 3754 . . . . . . . . . . 11 (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑[𝑤 / 𝑥]𝜑))
1413rexbidv 3222 . . . . . . . . . 10 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1514elrab 3605 . . . . . . . . 9 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1611, 15sylibr 237 . . . . . . . 8 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑})
17 sbceq2a 3711 . . . . . . . . 9 (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑𝜑))
1817rspcev 3544 . . . . . . . 8 ((𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
1916, 18sylancom 591 . . . . . . 7 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
20 nfcv 2920 . . . . . . . 8 𝑣{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
21 nfcv 2920 . . . . . . . . . 10 𝑦𝐴
22 nfcv 2920 . . . . . . . . . . 11 𝑦𝑤
23 nfsbc1v 3719 . . . . . . . . . . 11 𝑦[𝑧 / 𝑦]𝜑
2422, 23nfsbcw 3721 . . . . . . . . . 10 𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
2521, 24nfrex 3234 . . . . . . . . 9 𝑦𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
26 nfcv 2920 . . . . . . . . 9 𝑦𝐵
2725, 26nfrabw 3304 . . . . . . . 8 𝑦{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
28 nfsbc1v 3719 . . . . . . . 8 𝑦[𝑣 / 𝑦]𝜑
29 nfv 1916 . . . . . . . 8 𝑣𝜑
3020, 27, 28, 29, 17cbvrexfw 3350 . . . . . . 7 (∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3119, 30sylib 221 . . . . . 6 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3231exp31 423 . . . . 5 (𝑥𝐴 → (𝑦𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
334, 5, 32rexlimd 3242 . . . 4 (𝑥𝐴 → (∃𝑦𝐵 𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
3433ralimia 3091 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
35 nfsbc1v 3719 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
36 nfv 1916 . . . . . . . . 9 𝑤𝜑
3735, 36, 6cbvrexw 3354 . . . . . . . 8 (∃𝑤𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥𝐴 𝜑)
3814, 37bitrdi 290 . . . . . . 7 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥𝐴 𝜑))
3938elrab 3605 . . . . . 6 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
4039simprbi 500 . . . . 5 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥𝐴 𝜑)
4140rgen 3081 . . . 4 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑
4241a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)
433, 34, 423jca 1126 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 → ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
44 sseq1 3920 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐𝐵 ↔ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
45 nfcv 2920 . . . . . . . . 9 𝑥𝐴
46 nfsbc1v 3719 . . . . . . . . 9 𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
4745, 46nfrex 3234 . . . . . . . 8 𝑥𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
48 nfcv 2920 . . . . . . . 8 𝑥𝐵
4947, 48nfrabw 3304 . . . . . . 7 𝑥{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
5049nfeq2 2937 . . . . . 6 𝑥 𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
51 nfcv 2920 . . . . . . 7 𝑦𝑐
5251, 27rexeqf 3317 . . . . . 6 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5350, 52ralbid 3160 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥𝐴𝑦𝑐 𝜑 ↔ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5451, 27raleqf 3316 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦𝑐𝑥𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
5544, 53, 543anbi123d 1434 . . . 4 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑) ↔ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)))
5655spcegv 3518 . . 3 ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
5756imp 410 . 2 (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
581, 43, 57syl2an 598 1 ((𝐵𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1085   = wceq 1539  ∃wex 1782   ∈ wcel 2112  ∀wral 3071  ∃wrex 3072  {crab 3075  Vcvv 3410  [wsbc 3699   ⊆ wss 3861 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3700  df-in 3868  df-ss 3878 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator