Theorem indexa 37978

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 5284	. 2 ⊢ (𝐵 ∈ 𝑀 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2		ssrab2 4034	. . . 4 ⊢ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
3	2	a1i 11	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4		nfv 1916	. . . . 5 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
5		nfre1 3263	. . . . 5 ⊢ Ⅎ𝑦∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6		sbceq2a 3754	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑 ↔ 𝜑))
7	6	rspcev 3578	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)
8	7	ancoms 458	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)
9	8	anim1ci 617	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
10	9	anasss 466	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
11	10	ancoms 458	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
12		sbceq2a 3754	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑 ↔ 𝜑))
13	12	sbcbidv 3798	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝑤 / 𝑥]𝜑))
14	13	rexbidv 3162	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
15	14	elrab 3648	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
16	11, 15	sylibr 234	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑})
17		sbceq2a 3754	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑 ↔ 𝜑))
18	17	rspcev 3578	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
19	16, 18	sylancom 589	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
20		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑣{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
21		nfcv 2899	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐴
22		nfcv 2899	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑤
23		nfsbc1v 3762	. . . . . . . . . . 11 ⊢ Ⅎ𝑦[𝑧 / 𝑦]𝜑
24	22, 23	nfsbcw 3764	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
25	21, 24	nfrexw 3286	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
26		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑦𝐵
27	25, 26	nfrabw 3438	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
28		nfsbc1v 3762	. . . . . . . 8 ⊢ Ⅎ𝑦[𝑣 / 𝑦]𝜑
29		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑣𝜑
30	20, 27, 28, 29, 17	cbvrexfw 3279	. . . . . . 7 ⊢ (∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
31	19, 30	sylib 218	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
32	31	exp31 419	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
33	4, 5, 32	rexlimd 3245	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
34	33	ralimia 3072	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
35		nfsbc1v 3762	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
36		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑤𝜑
37	35, 36, 6	cbvrexw 3281	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)
38	14, 37	bitrdi 287	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑))
39	38	elrab 3648	. . . . . 6 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
40	39	simprbi 497	. . . . 5 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥 ∈ 𝐴 𝜑)
41	40	rgen 3054	. . . 4 ⊢ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑
42	41	a1i 11	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)
43	3, 34, 42	3jca 1129	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))
44		sseq1 3961	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐 ⊆ 𝐵 ↔ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
45		nfcv 2899	. . . . . . . . 9 ⊢ Ⅎ𝑥𝐴
46		nfsbc1v 3762	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
47	45, 46	nfrexw 3286	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
48		nfcv 2899	. . . . . . . 8 ⊢ Ⅎ𝑥𝐵
49	47, 48	nfrabw 3438	. . . . . . 7 ⊢ Ⅎ𝑥{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
50	49	nfeq2 2917	. . . . . 6 ⊢ Ⅎ𝑥 𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
51		nfcv 2899	. . . . . . 7 ⊢ Ⅎ𝑦𝑐
52	51, 27	rexeqf 3328	. . . . . 6 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
53	50, 52	ralbid 3251	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
54	51, 27	raleqf 3327	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))
55	44, 53, 54	3anbi123d 1439	. . . 4 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)))
56	55	spcegv 3553	. . 3 ⊢ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)))
57	56	imp 406	. 2 ⊢ (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
58	1, 43, 57	syl2an 597	1 ⊢ ((𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  {crab 3401  Vcvv 3442  [wsbc 3742   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-in 3910  df-ss 3920  df-pw 4558

This theorem is referenced by: (None)