indexdom

Description: If for every element of an indexing set A there exists a corresponding element of another set B , then there exists a subset of B consisting only of those elements which are indexed by A , and which is dominated by the set A . (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	indexdom	$⊢ (A \in M \land \forall x \in A \exists y \in B φ) \to \exists c ((c ≼ A \land c \subseteq B) \land (\forall x \in A \exists y \in c φ \land \forall y \in c \exists x \in A φ))$

Proof

Step	Hyp	Ref	Expression
1		nfsbc1v	$⊢ Ⅎ y \underset{˙}{[} f (x) / y \underset{˙}{]} φ$
2		sbceq1a	$⊢ y = f (x) \to (φ \leftrightarrow \underset{˙}{[} f (x) / y \underset{˙}{]} φ)$
3	1 2	ac6gf	$⊢ (A \in M \land \forall x \in A \exists y \in B φ) \to \exists f (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ)$
4		fdm	$⊢ f : A ⟶ B \to dom f = A$
5		vex	$⊢ f \in V$
6	5	dmex	$⊢ dom f \in V$
7	4 6	eqeltrrdi	$⊢ f : A ⟶ B \to A \in V$
8		ffn	$⊢ f : A ⟶ B \to f Fn A$
9		fnrndomg	$⊢ A \in V \to (f Fn A \to ran f ≼ A)$
10	7 8 9	sylc	$⊢ f : A ⟶ B \to ran f ≼ A$
11	10	adantr	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to ran f ≼ A$
12		frn	$⊢ f : A ⟶ B \to ran f \subseteq B$
13	12	adantr	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to ran f \subseteq B$
14		nfv	$⊢ Ⅎ x f : A ⟶ B$
15		nfra1	$⊢ Ⅎ x \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ$
16	14 15	nfan	$⊢ Ⅎ x (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ)$
17		ffun	$⊢ f : A ⟶ B \to Fun f$
18	17	adantr	$⊢ (f : A ⟶ B \land x \in A) \to Fun f$
19	4	eleq2d	$⊢ f : A ⟶ B \to (x \in dom f \leftrightarrow x \in A)$
20	19	biimpar	$⊢ (f : A ⟶ B \land x \in A) \to x \in dom f$
21		fvelrn	$⊢ (Fun f \land x \in dom f) \to f (x) \in ran f$
22	18 20 21	syl2anc	$⊢ (f : A ⟶ B \land x \in A) \to f (x) \in ran f$
23	22	adantlr	$⊢ ((f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \land x \in A) \to f (x) \in ran f$
24		rspa	$⊢ (\forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ \land x \in A) \to \underset{˙}{[} f (x) / y \underset{˙}{]} φ$
25	24	adantll	$⊢ ((f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \land x \in A) \to \underset{˙}{[} f (x) / y \underset{˙}{]} φ$
26		rspesbca	$⊢ (f (x) \in ran f \land \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to \exists y \in ran f φ$
27	23 25 26	syl2anc	$⊢ ((f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \land x \in A) \to \exists y \in ran f φ$
28	27	ex	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to (x \in A \to \exists y \in ran f φ)$
29	16 28	ralrimi	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to \forall x \in A \exists y \in ran f φ$
30		nfv	$⊢ Ⅎ y f : A ⟶ B$
31		nfcv	$⊢ \underline{Ⅎ} y A$
32	31 1	nfralw	$⊢ Ⅎ y \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ$
33	30 32	nfan	$⊢ Ⅎ y (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ)$
34		fvelrnb	$⊢ f Fn A \to (y \in ran f \leftrightarrow \exists x \in A f (x) = y)$
35	8 34	syl	$⊢ f : A ⟶ B \to (y \in ran f \leftrightarrow \exists x \in A f (x) = y)$
36	35	adantr	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to (y \in ran f \leftrightarrow \exists x \in A f (x) = y)$
37		rsp	$⊢ \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ \to (x \in A \to \underset{˙}{[} f (x) / y \underset{˙}{]} φ)$
38	37	adantl	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to (x \in A \to \underset{˙}{[} f (x) / y \underset{˙}{]} φ)$
39	2	eqcoms	$⊢ f (x) = y \to (φ \leftrightarrow \underset{˙}{[} f (x) / y \underset{˙}{]} φ)$
40	39	biimprcd	$⊢ \underset{˙}{[} f (x) / y \underset{˙}{]} φ \to (f (x) = y \to φ)$
41	38 40	syl6	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to (x \in A \to (f (x) = y \to φ))$
42	16 41	reximdai	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to (\exists x \in A f (x) = y \to \exists x \in A φ)$
43	36 42	sylbid	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to (y \in ran f \to \exists x \in A φ)$
44	33 43	ralrimi	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to \forall y \in ran f \exists x \in A φ$
45	5	rnex	$⊢ ran f \in V$
46		breq1	$⊢ c = ran f \to (c ≼ A \leftrightarrow ran f ≼ A)$
47		sseq1	$⊢ c = ran f \to (c \subseteq B \leftrightarrow ran f \subseteq B)$
48	46 47	anbi12d	$⊢ c = ran f \to ((c ≼ A \land c \subseteq B) \leftrightarrow (ran f ≼ A \land ran f \subseteq B))$
49		rexeq	$⊢ c = ran f \to (\exists y \in c φ \leftrightarrow \exists y \in ran f φ)$
50	49	ralbidv	$⊢ c = ran f \to (\forall x \in A \exists y \in c φ \leftrightarrow \forall x \in A \exists y \in ran f φ)$
51		raleq	$⊢ c = ran f \to (\forall y \in c \exists x \in A φ \leftrightarrow \forall y \in ran f \exists x \in A φ)$
52	50 51	anbi12d	$⊢ c = ran f \to ((\forall x \in A \exists y \in c φ \land \forall y \in c \exists x \in A φ) \leftrightarrow (\forall x \in A \exists y \in ran f φ \land \forall y \in ran f \exists x \in A φ))$
53	48 52	anbi12d	$⊢ c = ran f \to (((c ≼ A \land c \subseteq B) \land (\forall x \in A \exists y \in c φ \land \forall y \in c \exists x \in A φ)) \leftrightarrow ((ran f ≼ A \land ran f \subseteq B) \land (\forall x \in A \exists y \in ran f φ \land \forall y \in ran f \exists x \in A φ)))$
54	45 53	spcev	$⊢ ((ran f ≼ A \land ran f \subseteq B) \land (\forall x \in A \exists y \in ran f φ \land \forall y \in ran f \exists x \in A φ)) \to \exists c ((c ≼ A \land c \subseteq B) \land (\forall x \in A \exists y \in c φ \land \forall y \in c \exists x \in A φ))$
55	11 13 29 44 54	syl22anc	$⊢ (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to \exists c ((c ≼ A \land c \subseteq B) \land (\forall x \in A \exists y \in c φ \land \forall y \in c \exists x \in A φ))$
56	55	exlimiv	$⊢ \exists f (f : A ⟶ B \land \forall x \in A \underset{˙}{[} f (x) / y \underset{˙}{]} φ) \to \exists c ((c ≼ A \land c \subseteq B) \land (\forall x \in A \exists y \in c φ \land \forall y \in c \exists x \in A φ))$
57	3 56	syl	$⊢ (A \in M \land \forall x \in A \exists y \in B φ) \to \exists c ((c ≼ A \land c \subseteq B) \land (\forall x \in A \exists y \in c φ \land \forall y \in c \exists x \in A φ))$

Metamath Proof Explorer

Theorem indexdom

Proof