Theorem indexdom 38181

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.

Step	Hyp	Ref	Expression
1		nfsbc1v 3759	. . 3 ⊢ Ⅎ𝑦[(𝑓‘𝑥) / 𝑦]𝜑
2		sbceq1a 3750	. . 3 ⊢ (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑))
3	1, 2	ac6gf 38179	. 2 ⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑))
4		fdm 6690	. . . . . . 7 ⊢ (𝑓:𝐴⟶𝐵 → dom 𝑓 = 𝐴)
5		vex 3452	. . . . . . . 8 ⊢ 𝑓 ∈ V
6	5	dmex 7879	. . . . . . 7 ⊢ dom 𝑓 ∈ V
7	4, 6	eqeltrrdi 2865	. . . . . 6 ⊢ (𝑓:𝐴⟶𝐵 → 𝐴 ∈ V)
8		ffn 6680	. . . . . 6 ⊢ (𝑓:𝐴⟶𝐵 → 𝑓 Fn 𝐴)
9		fnrndomg 10483	. . . . . 6 ⊢ (𝐴 ∈ V → (𝑓 Fn 𝐴 → ran 𝑓 ≼ 𝐴))
10	7, 8, 9	sylc 65	. . . . 5 ⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ≼ 𝐴)
11	10	adantr 483	. . . 4 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ran 𝑓 ≼ 𝐴)
12		frn 6688	. . . . 5 ⊢ (𝑓:𝐴⟶𝐵 → ran 𝑓 ⊆ 𝐵)
13	12	adantr 483	. . . 4 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ran 𝑓 ⊆ 𝐵)
14		nfv 1928	. . . . . 6 ⊢ Ⅎ𝑥 𝑓:𝐴⟶𝐵
15		nfra1 3280	. . . . . 6 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑
16	14, 15	nfan 1913	. . . . 5 ⊢ Ⅎ𝑥(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)
17		ffun 6683	. . . . . . . . . 10 ⊢ (𝑓:𝐴⟶𝐵 → Fun 𝑓)
18	17	adantr 483	. . . . . . . . 9 ⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → Fun 𝑓)
19	4	eleq2d 2842	. . . . . . . . . 10 ⊢ (𝑓:𝐴⟶𝐵 → (𝑥 ∈ dom 𝑓 ↔ 𝑥 ∈ 𝐴))
20	19	biimpar 480	. . . . . . . . 9 ⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝑓)
21		fvelrn 7046	. . . . . . . . 9 ⊢ ((Fun 𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
22	18, 20, 21	syl2anc 592	. . . . . . . 8 ⊢ ((𝑓:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓)
23	22	adantlr 723	. . . . . . 7 ⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → (𝑓‘𝑥) ∈ ran 𝑓)
24		rspa 3245	. . . . . . . 8 ⊢ ((∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 ∧ 𝑥 ∈ 𝐴) → [(𝑓‘𝑥) / 𝑦]𝜑)
25	24	adantll 722	. . . . . . 7 ⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → [(𝑓‘𝑥) / 𝑦]𝜑)
26		rspesbca 3829	. . . . . . 7 ⊢ (((𝑓‘𝑥) ∈ ran 𝑓 ∧ [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑦 ∈ ran 𝑓𝜑)
27	23, 25, 26	syl2anc 592	. . . . . 6 ⊢ (((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ran 𝑓𝜑)
28	27	ex 415	. . . . 5 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → ∃𝑦 ∈ ran 𝑓𝜑))
29	16, 28	ralrimi 3254	. . . 4 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑)
30		nfv 1928	. . . . . 6 ⊢ Ⅎ𝑦 𝑓:𝐴⟶𝐵
31		nfcv 2918	. . . . . . 7 ⊢ Ⅎ𝑦𝐴
32	31, 1	nfralw 3303	. . . . . 6 ⊢ Ⅎ𝑦∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑
33	30, 32	nfan 1913	. . . . 5 ⊢ Ⅎ𝑦(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑)
34		fvelrnb 6916	. . . . . . . 8 ⊢ (𝑓 Fn 𝐴 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦))
35	8, 34	syl 17	. . . . . . 7 ⊢ (𝑓:𝐴⟶𝐵 → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦))
36	35	adantr 483	. . . . . 6 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 ↔ ∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦))
37		rsp 3244	. . . . . . . . 9 ⊢ (∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑 → (𝑥 ∈ 𝐴 → [(𝑓‘𝑥) / 𝑦]𝜑))
38	37	adantl 484	. . . . . . . 8 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → [(𝑓‘𝑥) / 𝑦]𝜑))
39	2	eqcoms 2764	. . . . . . . . 9 ⊢ ((𝑓‘𝑥) = 𝑦 → (𝜑 ↔ [(𝑓‘𝑥) / 𝑦]𝜑))
40	39	biimprcd 252	. . . . . . . 8 ⊢ ([(𝑓‘𝑥) / 𝑦]𝜑 → ((𝑓‘𝑥) = 𝑦 → 𝜑))
41	38, 40	syl6 35	. . . . . . 7 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑥 ∈ 𝐴 → ((𝑓‘𝑥) = 𝑦 → 𝜑)))
42	16, 41	reximdai 3258	. . . . . 6 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (∃𝑥 ∈ 𝐴 (𝑓‘𝑥) = 𝑦 → ∃𝑥 ∈ 𝐴 𝜑))
43	36, 42	sylbid 242	. . . . 5 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → (𝑦 ∈ ran 𝑓 → ∃𝑥 ∈ 𝐴 𝜑))
44	33, 43	ralrimi 3254	. . . 4 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)
45	5	rnex 7880	. . . . 5 ⊢ ran 𝑓 ∈ V
46		breq1 5097	. . . . . . 7 ⊢ (𝑐 = ran 𝑓 → (𝑐 ≼ 𝐴 ↔ ran 𝑓 ≼ 𝐴))
47		sseq1 3956	. . . . . . 7 ⊢ (𝑐 = ran 𝑓 → (𝑐 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵))
48	46, 47	anbi12d 640	. . . . . 6 ⊢ (𝑐 = ran 𝑓 → ((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ↔ (ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵)))
49		rexeq 3310	. . . . . . . 8 ⊢ (𝑐 = ran 𝑓 → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ ran 𝑓𝜑))
50	49	ralbidv 3179	. . . . . . 7 ⊢ (𝑐 = ran 𝑓 → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑))
51		raleq 3311	. . . . . . 7 ⊢ (𝑐 = ran 𝑓 → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑))
52	50, 51	anbi12d 640	. . . . . 6 ⊢ (𝑐 = ran 𝑓 → ((∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)))
53	48, 52	anbi12d 640	. . . . 5 ⊢ (𝑐 = ran 𝑓 → (((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)) ↔ ((ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑))))
54	45, 53	spcev 3560	. . . 4 ⊢ (((ran 𝑓 ≼ 𝐴 ∧ ran 𝑓 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ ran 𝑓𝜑 ∧ ∀𝑦 ∈ ran 𝑓∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)))
55	11, 13, 29, 44, 54	syl22anc 847	. . 3 ⊢ ((𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)))
56	55	exlimiv 1944	. 2 ⊢ (∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 [(𝑓‘𝑥) / 𝑦]𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)))
57	3, 56	syl 17	1 ⊢ ((𝐴 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐((𝑐 ≼ 𝐴 ∧ 𝑐 ⊆ 𝐵) ∧ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1554  ∃wex 1793   ∈ wcel 2136  ∀wral 3070  ∃wrex 3080  Vcvv 3448  [wsbc 3739   ⊆ wss 3899   class class class wbr 5094  dom cdm 5640  ran crn 5641  Fun wfun 6504   Fn wfn 6505  ⟶wf 6506  ‘cfv 6510   ≼ cdom 8914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-rep 5221  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-reg 9530  ax-inf2 9586  ax-ac2 10410

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-ral 3071  df-rex 3081  df-rmo 3361  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-int 4900  df-iun 4945  df-iin 4946  df-br 5095  df-opab 5157  df-mpt 5176  df-tr 5202  df-id 5535  df-eprel 5540  df-po 5548  df-so 5549  df-fr 5593  df-se 5594  df-we 5595  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-isom 6519  df-riota 7342  df-ov 7388  df-oprab 7389  df-mpo 7390  df-om 7836  df-1st 7959  df-2nd 7960  df-frecs 8250  df-wrecs 8281  df-recs 8330  df-rdg 8369  df-er 8666  df-map 8798  df-en 8917  df-dom 8918  df-r1 9712  df-rank 9713  df-card 9887  df-acn 9890  df-ac 10062

This theorem is referenced by: (None)