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 34566
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 5130 . 2 (𝐵𝑀 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2 ssrab2 3981 . . . 4 {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
32a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4 nfv 1892 . . . . 5 𝑦 𝑥𝐴
5 nfre1 3269 . . . . 5 𝑦𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6 sbceq2a 3721 . . . . . . . . . . . . . 14 (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑𝜑))
76rspcev 3559 . . . . . . . . . . . . 13 ((𝑥𝐴𝜑) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
87ancoms 459 . . . . . . . . . . . 12 ((𝜑𝑥𝐴) → ∃𝑤𝐴 [𝑤 / 𝑥]𝜑)
98anim1ci 615 . . . . . . . . . . 11 (((𝜑𝑥𝐴) ∧ 𝑦𝐵) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
109anasss 467 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1110ancoms 459 . . . . . . . . 9 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
12 sbceq2a 3721 . . . . . . . . . . . 12 (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑𝜑))
1312sbcbidv 3759 . . . . . . . . . . 11 (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑[𝑤 / 𝑥]𝜑))
1413rexbidv 3260 . . . . . . . . . 10 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1514elrab 3619 . . . . . . . . 9 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑤𝐴 [𝑤 / 𝑥]𝜑))
1611, 15sylibr 235 . . . . . . . 8 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑})
17 sbceq2a 3721 . . . . . . . . 9 (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑𝜑))
1817rspcev 3559 . . . . . . . 8 ((𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
1916, 18sylancom 588 . . . . . . 7 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
20 nfcv 2949 . . . . . . . 8 𝑣{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
21 nfcv 2949 . . . . . . . . . 10 𝑦𝐴
22 nfcv 2949 . . . . . . . . . . 11 𝑦𝑤
23 nfsbc1v 3729 . . . . . . . . . . 11 𝑦[𝑧 / 𝑦]𝜑
2422, 23nfsbc 3731 . . . . . . . . . 10 𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
2521, 24nfrex 3271 . . . . . . . . 9 𝑦𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
26 nfcv 2949 . . . . . . . . 9 𝑦𝐵
2725, 26nfrab 3345 . . . . . . . 8 𝑦{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
28 nfsbc1v 3729 . . . . . . . 8 𝑦[𝑣 / 𝑦]𝜑
29 nfv 1892 . . . . . . . 8 𝑣𝜑
3020, 27, 28, 29, 17cbvrexf 3398 . . . . . . 7 (∃𝑣 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3119, 30sylib 219 . . . . . 6 (((𝑥𝐴𝑦𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
3231exp31 420 . . . . 5 (𝑥𝐴 → (𝑦𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
334, 5, 32rexlimd 3278 . . . 4 (𝑥𝐴 → (∃𝑦𝐵 𝜑 → ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
3433ralimia 3125 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
35 nfsbc1v 3729 . . . . . . . . 9 𝑥[𝑤 / 𝑥]𝜑
36 nfv 1892 . . . . . . . . 9 𝑤𝜑
3735, 36, 6cbvrex 3400 . . . . . . . 8 (∃𝑤𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥𝐴 𝜑)
3814, 37syl6bb 288 . . . . . . 7 (𝑧 = 𝑦 → (∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥𝐴 𝜑))
3938elrab 3619 . . . . . 6 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦𝐵 ∧ ∃𝑥𝐴 𝜑))
4039simprbi 497 . . . . 5 (𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥𝐴 𝜑)
4140rgen 3115 . . . 4 𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑
4241a1i 11 . . 3 (∀𝑥𝐴𝑦𝐵 𝜑 → ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)
433, 34, 423jca 1121 . 2 (∀𝑥𝐴𝑦𝐵 𝜑 → ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
44 sseq1 3917 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐𝐵 ↔ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
45 nfcv 2949 . . . . . . . . 9 𝑥𝐴
46 nfsbc1v 3729 . . . . . . . . 9 𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
4745, 46nfrex 3271 . . . . . . . 8 𝑥𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
48 nfcv 2949 . . . . . . . 8 𝑥𝐵
4947, 48nfrab 3345 . . . . . . 7 𝑥{𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
5049nfeq2 2964 . . . . . 6 𝑥 𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
51 nfcv 2949 . . . . . . 7 𝑦𝑐
5251, 27rexeqf 3358 . . . . . 6 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5350, 52ralbid 3195 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥𝐴𝑦𝑐 𝜑 ↔ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
5451, 27raleqf 3357 . . . . 5 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦𝑐𝑥𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑))
5544, 53, 543anbi123d 1428 . . . 4 (𝑐 = {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑) ↔ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)))
5655spcegv 3540 . . 3 ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
5756imp 407 . 2 (({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥𝐴𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧𝐵 ∣ ∃𝑤𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥𝐴 𝜑)) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
581, 43, 57syl2an 595 1 ((𝐵𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑐(𝑐𝐵 ∧ ∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080   = wceq 1522  wex 1761  wcel 2081  wral 3105  wrex 3106  {crab 3109  Vcvv 3437  [wsbc 3709  wss 3863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5099
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3710  df-in 3870  df-ss 3878
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator