Theorem indexa 38425

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 5313	. 2 ⊢ (𝐵 ∈ 𝑀 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V)
2		ssrab2 4037	. . . 4 ⊢ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵
3	2	a1i 11	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵)
4		nfv 1947	. . . . 5 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
5		nfre1 3293	. . . . 5 ⊢ Ⅎ𝑦∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑
6		sbceq2a 3759	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑥 → ([𝑤 / 𝑥]𝜑 ↔ 𝜑))
7	6	rspcev 3584	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)
8	7	ancoms 464	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑)
9	8	anim1ci 628	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
10	9	anasss 472	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
11	10	ancoms 464	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → (𝑦 ∈ 𝐵 ∧ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑))
12		sbceq2a 3759	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑦]𝜑 ↔ 𝜑))
13	12	sbcbidv 3802	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → ([𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ [𝑤 / 𝑥]𝜑))
14	13	rexbidv 3192	. . . . . . . . . 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 600	. . . . . . 7 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑)
20		nfcv 2928	. . . . . . . 8 ⊢ Ⅎ𝑣{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
21		nfcv 2928	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐴
22		nfcv 2928	. . . . . . . . . . 11 ⊢ Ⅎ𝑦𝑤
23		nfsbc1v 3767	. . . . . . . . . . 11 ⊢ Ⅎ𝑦[𝑧 / 𝑦]𝜑
24	22, 23	nfsbcw 3769	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
25	21, 24	nfrexw 3316	. . . . . . . . 9 ⊢ Ⅎ𝑦∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
26		nfcv 2928	. . . . . . . . 9 ⊢ Ⅎ𝑦𝐵
27	25, 26	nfrabw 3455	. . . . . . . 8 ⊢ Ⅎ𝑦{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
28		nfsbc1v 3767	. . . . . . . 8 ⊢ Ⅎ𝑦[𝑣 / 𝑦]𝜑
29		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑣𝜑
30	20, 27, 28, 29, 17	cbvrexfw 3309	. . . . . . 7 ⊢ (∃𝑣 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}[𝑣 / 𝑦]𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
31	19, 30	sylib 221	. . . . . 6 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝜑) → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
32	31	exp31 425	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → (𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)))
33	4, 5, 32	rexlimd 3275	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∃𝑦 ∈ 𝐵 𝜑 → ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
34	33	ralimia 3102	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑)
35		nfsbc1v 3767	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝜑
36		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑤𝜑
37	35, 36, 6	cbvrexw 3311	. . . . . . . 8 ⊢ (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑)
38	14, 37	bitrdi 290	. . . . . . 7 ⊢ (𝑧 = 𝑦 → (∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜑))
39	38	elrab 3653	. . . . . 6 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥 ∈ 𝐴 𝜑))
40	39	simprbi 503	. . . . 5 ⊢ (𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ∃𝑥 ∈ 𝐴 𝜑)
41	40	rgen 3084	. . . 4 ⊢ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑
42	41	a1i 11	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)
43	3, 34, 42	3jca 1146	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 → ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))
44		sseq1 3965	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (𝑐 ⊆ 𝐵 ↔ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵))
45		nfcv 2928	. . . . . . . . 9 ⊢ Ⅎ𝑥𝐴
46		nfsbc1v 3767	. . . . . . . . 9 ⊢ Ⅎ𝑥[𝑤 / 𝑥][𝑧 / 𝑦]𝜑
47	45, 46	nfrexw 3316	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑
48		nfcv 2928	. . . . . . . 8 ⊢ Ⅎ𝑥𝐵
49	47, 48	nfrabw 3455	. . . . . . 7 ⊢ Ⅎ𝑥{𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
50	49	nfeq2 2945	. . . . . 6 ⊢ Ⅎ𝑥 𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}
51		nfcv 2928	. . . . . . 7 ⊢ Ⅎ𝑦𝑐
52	51, 27	rexeqf 3349	. . . . . 6 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∃𝑦 ∈ 𝑐 𝜑 ↔ ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
53	50, 52	ralbid 3281	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑))
54	51, 27	raleqf 3348	. . . . 5 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → (∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑))
55	44, 53, 54	3anbi123d 1464	. . . 4 ⊢ (𝑐 = {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} → ((𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑) ↔ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)))
56	55	spcegv 3559	. . 3 ⊢ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V → (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑)))
57	56	imp 412	. 2 ⊢ (({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ∈ V ∧ ({𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑} ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}𝜑 ∧ ∀𝑦 ∈ {𝑧 ∈ 𝐵 ∣ ∃𝑤 ∈ 𝐴 [𝑤 / 𝑥][𝑧 / 𝑦]𝜑}∃𝑥 ∈ 𝐴 𝜑)) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))
58	1, 43, 57	syl2an 608	1 ⊢ ((𝐵 ∈ 𝑀 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑) → ∃𝑐(𝑐 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑐 𝜑 ∧ ∀𝑦 ∈ 𝑐 ∃𝑥 ∈ 𝐴 𝜑))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092  {crab 3419  Vcvv 3458  [wsbc 3747   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-in 3915  df-ss 3925  df-pw 4569

This theorem is used by: (None)