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 33160
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 4772 . 2 (𝐵𝑀 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2 ssrab2 3666 . . . 4 {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
32a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4 nfv 1840 . . . . 5 𝑦 𝑥𝐴
5 nfre1 2999 . . . . 5 𝑦𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6 sbceq2a 3429 . . . . . . . . . . . . . . 15 (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑𝜑))
76rspcev 3295 . . . . . . . . . . . . . 14 ((𝑥𝐴𝜑) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
87ancoms 469 . . . . . . . . . . . . 13 ((𝜑𝑥𝐴) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
98anim2i 592 . . . . . . . . . . . 12 ((𝑦𝐵 ∧ (𝜑𝑥𝐴)) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
109ancoms 469 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1110anasss 678 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1211ancoms 469 . . . . . . . . 9 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
13 sbceq2a 3429 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑𝜑))
1413sbcbidv 3472 . . . . . . . . . . 11 (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑[𝑤 / 𝑥]𝜑))
1514rexbidv 3045 . . . . . . . . . 10 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1615elrab 3346 . . . . . . . . 9 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1712, 16sylibr 224 . . . . . . . 8 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑})
18 sbceq2a 3429 . . . . . . . . 9 (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑𝜑))
1918rspcev 3295 . . . . . . . 8 ((𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
2017, 19sylancom 700 . . . . . . 7 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
21 nfcv 2761 . . . . . . . 8 𝑣{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
22 nfcv 2761 . . . . . . . . . 10 𝑦𝐴
23 nfcv 2761 . . . . . . . . . . 11 𝑦𝑤
24 nfsbc1v 3437 . . . . . . . . . . 11 𝑦[𝑧 / 𝑦]𝜑
2523, 24nfsbc 3439 . . . . . . . . . 10 𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
2622, 25nfrex 3001 . . . . . . . . 9 𝑦𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
27 nfcv 2761 . . . . . . . . 9 𝑦𝐵
2826, 27nfrab 3112 . . . . . . . 8 𝑦{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
29 nfsbc1v 3437 . . . . . . . 8 𝑦[𝑣 / 𝑦]𝜑
30 nfv 1840 . . . . . . . 8 𝑣𝜑
3121, 28, 29, 30, 18cbvrexf 3154 . . . . . . 7 (∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3220, 31sylib 208 . . . . . 6 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3332exp31 629 . . . . 5 (𝑥𝐴 → (𝑦𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
344, 5, 33rexlimd 3019 . . . 4 (𝑥𝐴 → (∃𝑦𝐵 𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
3534ralimia 2945 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
36 nfsbc1v 3437 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
37 nfv 1840 . . . . . . . . 9 𝑤𝜑
3836, 37, 6cbvrex 3156 . . . . . . . 8 (∃𝑤𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥𝐴 𝜑)
3915, 38syl6bb 276 . . . . . . 7 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥𝐴 𝜑))
4039elrab 3346 . . . . . 6 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
4140simprbi 480 . . . . 5 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥𝐴 𝜑)
4241rgen 2917 . . . 4 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑
4342a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)
443, 35, 433jca 1240 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 → ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
45 sseq1 3605 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐𝐵 ↔ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
46 nfcv 2761 . . . . . . . . 9 𝑥𝐴
47 nfsbc1v 3437 . . . . . . . . 9 𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
4846, 47nfrex 3001 . . . . . . . 8 𝑥𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
49 nfcv 2761 . . . . . . . 8 𝑥𝐵
5048, 49nfrab 3112 . . . . . . 7 𝑥{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
5150nfeq2 2776 . . . . . 6 𝑥 𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
52 nfcv 2761 . . . . . . 7 𝑦𝑐
5352, 28rexeqf 3124 . . . . . 6 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5451, 53ralbid 2977 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥𝐴𝑦𝑐 𝜑 ↔ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5552, 28raleqf 3123 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦𝑐𝑥𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
5645, 54, 553anbi123d 1396 . . . 4 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑) ↔ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)))
5756spcegv 3280 . . 3 ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
5857imp 445 . 2 (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
591, 44, 58syl2an 494 1 ((𝐵𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wral 2907  wrex 2908  {crab 2911  Vcvv 3186  [wsbc 3417  wss 3555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-in 3562  df-ss 3569
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator