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

Theorem indexdom 37358
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 𝐴, and which is dominated by the set 𝐴. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
indexdom ((𝐴𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑐((𝑐𝐴𝑐𝐵) ∧ (∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
Distinct variable groups:   𝐴,𝑐,𝑥,𝑦   𝐵,𝑐,𝑥,𝑦   𝜑,𝑐
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑀(𝑥,𝑦,𝑐)

Proof of Theorem indexdom
Dummy variable 𝑓 is distinct from all other variables.
StepHypRef Expression
1 nfsbc1v 3793 . . 3 𝑦[(𝑓𝑥) / 𝑦]𝜑
2 sbceq1a 3784 . . 3 (𝑦 = (𝑓𝑥) → (𝜑[(𝑓𝑥) / 𝑦]𝜑))
31, 2ac6gf 37356 . 2 ((𝐴𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑))
4 fdm 6732 . . . . . . 7 (𝑓:𝐴𝐵 → dom 𝑓 = 𝐴)
5 vex 3465 . . . . . . . 8 𝑓 ∈ V
65dmex 7917 . . . . . . 7 dom 𝑓 ∈ V
74, 6eqeltrrdi 2834 . . . . . 6 (𝑓:𝐴𝐵𝐴 ∈ V)
8 ffn 6723 . . . . . 6 (𝑓:𝐴𝐵𝑓 Fn 𝐴)
9 fnrndomg 10566 . . . . . 6 (𝐴 ∈ V → (𝑓 Fn 𝐴 → ran 𝑓𝐴))
107, 8, 9sylc 65 . . . . 5 (𝑓:𝐴𝐵 → ran 𝑓𝐴)
1110adantr 479 . . . 4 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → ran 𝑓𝐴)
12 frn 6730 . . . . 5 (𝑓:𝐴𝐵 → ran 𝑓𝐵)
1312adantr 479 . . . 4 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → ran 𝑓𝐵)
14 nfv 1909 . . . . . 6 𝑥 𝑓:𝐴𝐵
15 nfra1 3271 . . . . . 6 𝑥𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑
1614, 15nfan 1894 . . . . 5 𝑥(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑)
17 ffun 6726 . . . . . . . . . 10 (𝑓:𝐴𝐵 → Fun 𝑓)
1817adantr 479 . . . . . . . . 9 ((𝑓:𝐴𝐵𝑥𝐴) → Fun 𝑓)
194eleq2d 2811 . . . . . . . . . 10 (𝑓:𝐴𝐵 → (𝑥 ∈ dom 𝑓𝑥𝐴))
2019biimpar 476 . . . . . . . . 9 ((𝑓:𝐴𝐵𝑥𝐴) → 𝑥 ∈ dom 𝑓)
21 fvelrn 7085 . . . . . . . . 9 ((Fun 𝑓𝑥 ∈ dom 𝑓) → (𝑓𝑥) ∈ ran 𝑓)
2218, 20, 21syl2anc 582 . . . . . . . 8 ((𝑓:𝐴𝐵𝑥𝐴) → (𝑓𝑥) ∈ ran 𝑓)
2322adantlr 713 . . . . . . 7 (((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) ∧ 𝑥𝐴) → (𝑓𝑥) ∈ ran 𝑓)
24 rspa 3235 . . . . . . . 8 ((∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑𝑥𝐴) → [(𝑓𝑥) / 𝑦]𝜑)
2524adantll 712 . . . . . . 7 (((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) ∧ 𝑥𝐴) → [(𝑓𝑥) / 𝑦]𝜑)
26 rspesbca 3871 . . . . . . 7 (((𝑓𝑥) ∈ ran 𝑓[(𝑓𝑥) / 𝑦]𝜑) → ∃𝑦 ∈ ran 𝑓𝜑)
2723, 25, 26syl2anc 582 . . . . . 6 (((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) ∧ 𝑥𝐴) → ∃𝑦 ∈ ran 𝑓𝜑)
2827ex 411 . . . . 5 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → (𝑥𝐴 → ∃𝑦 ∈ ran 𝑓𝜑))
2916, 28ralrimi 3244 . . . 4 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → ∀𝑥𝐴𝑦 ∈ ran 𝑓𝜑)
30 nfv 1909 . . . . . 6 𝑦 𝑓:𝐴𝐵
31 nfcv 2891 . . . . . . 7 𝑦𝐴
3231, 1nfralw 3298 . . . . . 6 𝑦𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑
3330, 32nfan 1894 . . . . 5 𝑦(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑)
34 fvelrnb 6958 . . . . . . . 8 (𝑓 Fn 𝐴 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥𝐴 (𝑓𝑥) = 𝑦))
358, 34syl 17 . . . . . . 7 (𝑓:𝐴𝐵 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥𝐴 (𝑓𝑥) = 𝑦))
3635adantr 479 . . . . . 6 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥𝐴 (𝑓𝑥) = 𝑦))
37 rsp 3234 . . . . . . . . 9 (∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑 → (𝑥𝐴[(𝑓𝑥) / 𝑦]𝜑))
3837adantl 480 . . . . . . . 8 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → (𝑥𝐴[(𝑓𝑥) / 𝑦]𝜑))
392eqcoms 2733 . . . . . . . . 9 ((𝑓𝑥) = 𝑦 → (𝜑[(𝑓𝑥) / 𝑦]𝜑))
4039biimprcd 249 . . . . . . . 8 ([(𝑓𝑥) / 𝑦]𝜑 → ((𝑓𝑥) = 𝑦𝜑))
4138, 40syl6 35 . . . . . . 7 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → (𝑥𝐴 → ((𝑓𝑥) = 𝑦𝜑)))
4216, 41reximdai 3248 . . . . . 6 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → (∃𝑥𝐴 (𝑓𝑥) = 𝑦 → ∃𝑥𝐴 𝜑))
4336, 42sylbid 239 . . . . 5 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 → ∃𝑥𝐴 𝜑))
4433, 43ralrimi 3244 . . . 4 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → ∀𝑦 ∈ ran 𝑓𝑥𝐴 𝜑)
455rnex 7918 . . . . 5 ran 𝑓 ∈ V
46 breq1 5152 . . . . . . 7 (𝑐 = ran 𝑓 → (𝑐𝐴 ↔ ran 𝑓𝐴))
47 sseq1 4002 . . . . . . 7 (𝑐 = ran 𝑓 → (𝑐𝐵 ↔ ran 𝑓𝐵))
4846, 47anbi12d 630 . . . . . 6 (𝑐 = ran 𝑓 → ((𝑐𝐴𝑐𝐵) ↔ (ran 𝑓𝐴 ∧ ran 𝑓𝐵)))
49 rexeq 3310 . . . . . . . 8 (𝑐 = ran 𝑓 → (∃𝑦𝑐 𝜑 ↔ ∃𝑦 ∈ ran 𝑓𝜑))
5049ralbidv 3167 . . . . . . 7 (𝑐 = ran 𝑓 → (∀𝑥𝐴𝑦𝑐 𝜑 ↔ ∀𝑥𝐴𝑦 ∈ ran 𝑓𝜑))
51 raleq 3311 . . . . . . 7 (𝑐 = ran 𝑓 → (∀𝑦𝑐𝑥𝐴 𝜑 ↔ ∀𝑦 ∈ ran 𝑓𝑥𝐴 𝜑))
5250, 51anbi12d 630 . . . . . 6 (𝑐 = ran 𝑓 → ((∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑) ↔ (∀𝑥𝐴𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓𝑥𝐴 𝜑)))
5348, 52anbi12d 630 . . . . 5 (𝑐 = ran 𝑓 → (((𝑐𝐴𝑐𝐵) ∧ (∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)) ↔ ((ran 𝑓𝐴 ∧ ran 𝑓𝐵) ∧ (∀𝑥𝐴𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓𝑥𝐴 𝜑))))
5445, 53spcev 3590 . . . 4 (((ran 𝑓𝐴 ∧ ran 𝑓𝐵) ∧ (∀𝑥𝐴𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓𝑥𝐴 𝜑)) → ∃𝑐((𝑐𝐴𝑐𝐵) ∧ (∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
5511, 13, 29, 44, 54syl22anc 837 . . 3 ((𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐𝐴𝑐𝐵) ∧ (∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
5655exlimiv 1925 . 2 (∃𝑓(𝑓:𝐴𝐵 ∧ ∀𝑥𝐴 [(𝑓𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐𝐴𝑐𝐵) ∧ (∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
573, 56syl 17 1 ((𝐴𝑀 ∧ ∀𝑥𝐴𝑦𝐵 𝜑) → ∃𝑐((𝑐𝐴𝑐𝐵) ∧ (∀𝑥𝐴𝑦𝑐 𝜑 ∧ ∀𝑦𝑐𝑥𝐴 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394   = wceq 1533  wex 1773  wcel 2098  wral 3050  wrex 3059  Vcvv 3461  [wsbc 3773  wss 3944   class class class wbr 5149  dom cdm 5678  ran crn 5679  Fun wfun 6543   Fn wfn 6544  wf 6545  cfv 6549  cdom 8962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-reg 9622  ax-inf2 9671  ax-ac2 10493
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-er 8725  df-map 8847  df-en 8965  df-dom 8966  df-r1 9794  df-rank 9795  df-card 9969  df-acn 9972  df-ac 10146
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator