Theorem indexa 38244

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 5298	. 2 ⊢ (𝐵 ∈ 𝑀 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2		ssrab2 4036	. . . 4 ⊢ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
3	2	a1i 11	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4		nfv 1937	. . . . 5 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
5		nfre1 3290	. . . . 5 ⊢ Ⅎ𝑦∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6		sbceq2a 3759	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑 ↔ 𝜑))
7	6	rspcev 3584	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)
8	7	ancoms 463	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)
9	8	anim1ci 627	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
10	9	anasss 471	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
11	10	ancoms 463	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
12		sbceq2a 3759	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑 ↔ 𝜑))
13	12	sbcbidv 3802	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝑤 / 𝑥]𝜑))
14	13	rexbidv 3189	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
15	14	elrab 3653	. . . . . . . . 9 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
16	11, 15	sylibr 237	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → 𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑})
17		sbceq2a 3759	. . . . . . . . 9 ⊢ (𝑣 = 𝑦 → ([𝑣 / 𝑦]𝜑 ↔ 𝜑))
18	17	rspcev 3584	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
19	16, 18	sylancom 599	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
20		nfcv 2927	. . . . . . . 8 ⊢ Ⅎ𝑣{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
21		nfcv 2927	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐴
22		nfcv 2927	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑤
23		nfsbc1v 3767	. . . . . . . . . . 11 ⊢ Ⅎ𝑦[𝑧 / 𝑦]𝜑
24	22, 23	nfsbcw 3769	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
25	21, 24	nfrexw 3313	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
26		nfcv 2927	. . . . . . . . 9 ⊢ Ⅎ𝑦𝐵
27	25, 26	nfrabw 3454	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
28		nfsbc1v 3767	. . . . . . . 8 ⊢ Ⅎ𝑦[𝑣 / 𝑦]𝜑
29		nfv 1937	. . . . . . . 8 ⊢ Ⅎ𝑣𝜑
30	20, 27, 28, 29, 17	cbvrexfw 3306	. . . . . . 7 ⊢ (∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
31	19, 30	sylib 221	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
32	31	exp31 424	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
33	4, 5, 32	rexlimd 3272	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
34	33	ralimia 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
35		nfsbc1v 3767	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
36		nfv 1937	. . . . . . . . 9 ⊢ Ⅎ𝑤𝜑
37	35, 36, 6	cbvrexw 3308	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)
38	14, 37	bitrdi 290	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑))
39	38	elrab 3653	. . . . . 6 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
40	39	simprbi 502	. . . . 5 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥 ∈ 𝐴 𝜑)
41	40	rgen 3081	. . . 4 ⊢ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑
42	41	a1i 11	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)
43	3, 34, 42	3jca 1144	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))
44		sseq1 3964	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐 ⊆ 𝐵 ↔ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
45		nfcv 2927	. . . . . . . . 9 ⊢ Ⅎ𝑥𝐴
46		nfsbc1v 3767	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
47	45, 46	nfrexw 3313	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
48		nfcv 2927	. . . . . . . 8 ⊢ Ⅎ𝑥𝐵
49	47, 48	nfrabw 3454	. . . . . . 7 ⊢ Ⅎ𝑥{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
50	49	nfeq2 2944	. . . . . 6 ⊢ Ⅎ𝑥 𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
51		nfcv 2927	. . . . . . 7 ⊢ Ⅎ𝑦𝑐
52	51, 27	rexeqf 3347	. . . . . 6 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
53	50, 52	ralbid 3278	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
54	51, 27	raleqf 3346	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))
55	44, 53, 54	3anbi123d 1460	. . . 4 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)))
56	55	spcegv 3559	. . 3 ⊢ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)))
57	56	imp 411	. 2 ⊢ (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
58	1, 43, 57	syl2an 607	1 ⊢ ((𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089  {crab 3417  Vcvv 3457  [wsbc 3747   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-in 3914  df-ss 3924  df-pw 4560

This theorem is referenced by: (None)