Theorem indexa 37740

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.

Step	Hyp	Ref	Expression
1		rabexg 5337	. 2 ⊢ (𝐵 ∈ 𝑀 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2		ssrab2 4080	. . . 4 ⊢ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
3	2	a1i 11	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4		nfv 1914	. . . . 5 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
5		nfre1 3285	. . . . 5 ⊢ Ⅎ𝑦∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6		sbceq2a 3800	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑 ↔ 𝜑))
7	6	rspcev 3622	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)
8	7	ancoms 458	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)
9	8	anim1ci 616	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
10	9	anasss 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
11	10	ancoms 458	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
12		sbceq2a 3800	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑 ↔ 𝜑))
13	12	sbcbidv 3845	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝑤 / 𝑥]𝜑))
14	13	rexbidv 3179	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
15	14	elrab 3692	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
16	11, 15	sylibr 234	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑})
17		sbceq2a 3800	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑 ↔ 𝜑))
18	17	rspcev 3622	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
19	16, 18	sylancom 588	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
20		nfcv 2905	. . . . . . . 8 ⊢ Ⅎ𝑣{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
21		nfcv 2905	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐴
22		nfcv 2905	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑤
23		nfsbc1v 3808	. . . . . . . . . . 11 ⊢ Ⅎ𝑦[𝑧 / 𝑦]𝜑
24	22, 23	nfsbcw 3810	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
25	21, 24	nfrexw 3313	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
26		nfcv 2905	. . . . . . . . 9 ⊢ Ⅎ𝑦𝐵
27	25, 26	nfrabw 3475	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
28		nfsbc1v 3808	. . . . . . . 8 ⊢ Ⅎ𝑦[𝑣 / 𝑦]𝜑
29		nfv 1914	. . . . . . . 8 ⊢ Ⅎ𝑣𝜑
30	20, 27, 28, 29, 17	cbvrexfw 3305	. . . . . . 7 ⊢ (∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
31	19, 30	sylib 218	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
32	31	exp31 419	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
33	4, 5, 32	rexlimd 3266	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
34	33	ralimia 3080	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
35		nfsbc1v 3808	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
36		nfv 1914	. . . . . . . . 9 ⊢ Ⅎ𝑤𝜑
37	35, 36, 6	cbvrexw 3307	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)
38	14, 37	bitrdi 287	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑))
39	38	elrab 3692	. . . . . 6 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
40	39	simprbi 496	. . . . 5 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥 ∈ 𝐴 𝜑)
41	40	rgen 3063	. . . 4 ⊢ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑
42	41	a1i 11	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)
43	3, 34, 42	3jca 1129	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))
44		sseq1 4009	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐 ⊆ 𝐵 ↔ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
45		nfcv 2905	. . . . . . . . 9 ⊢ Ⅎ𝑥𝐴
46		nfsbc1v 3808	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
47	45, 46	nfrexw 3313	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
48		nfcv 2905	. . . . . . . 8 ⊢ Ⅎ𝑥𝐵
49	47, 48	nfrabw 3475	. . . . . . 7 ⊢ Ⅎ𝑥{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
50	49	nfeq2 2923	. . . . . 6 ⊢ Ⅎ𝑥 𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
51		nfcv 2905	. . . . . . 7 ⊢ Ⅎ𝑦𝑐
52	51, 27	rexeqf 3354	. . . . . 6 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
53	50, 52	ralbid 3273	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
54	51, 27	raleqf 3353	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))
55	44, 53, 54	3anbi123d 1438	. . . 4 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)))
56	55	spcegv 3597	. . 3 ⊢ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)))
57	56	imp 406	. 2 ⊢ (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
58	1, 43, 57	syl2an 596	1 ⊢ ((𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070  {crab 3436  Vcvv 3480  [wsbc 3788   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-in 3958  df-ss 3968  df-pw 4602

This theorem is referenced by: (None)