Metamath Proof Explorer

Theorem indexa

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 . 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)

Ref Expression
Assertion indexa ( ( 𝐵 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step Hyp Ref Expression
1 rabexg ⊢ ( 𝐵 ∈ 𝑀 → { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∈ V )
2 ssrab2 ⊢ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ⊆ 𝐵
3 2 a1i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ⊆ 𝐵 )
4 nfv ⊢ Ⅎ 𝑦 𝑥 ∈ 𝐴
5 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑
6 sbceq2a ⊢ ( 𝑤 = 𝑥 → ( [ 𝑤 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
7 6 rspcev ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] 𝜑 )
8 7 ancoms ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] 𝜑 )
9 8 anim1ci ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] 𝜑 ) )
10 9 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] 𝜑 ) )
11 10 ancoms ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) → ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] 𝜑 ) )
12 sbceq2a ⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
13 12 sbcbidv ⊢ ( 𝑧 = 𝑦 → ( [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑥 ] 𝜑 ) )
14 13 rexbidv ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] 𝜑 ) )
15 14 elrab ⊢ ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] 𝜑 ) )
16 11 15 sylibr ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) → 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } )
17 sbceq2a ⊢ ( 𝑣 = 𝑦 → ( [ 𝑣 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
18 17 rspcev ⊢ ( ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∧ 𝜑 ) → ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } [ 𝑣 / 𝑦 ] 𝜑 )
19 16 18 sylancom ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) → ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } [ 𝑣 / 𝑦 ] 𝜑 )
20 nfcv ⊢ Ⅎ 𝑣 { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 }
21 nfcv ⊢ Ⅎ 𝑦 𝐴
22 nfcv ⊢ Ⅎ 𝑦 𝑤
23 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝜑
24 22 23 nfsbcw ⊢ Ⅎ 𝑦 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑
25 21 24 nfrexw ⊢ Ⅎ 𝑦 ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑
26 nfcv ⊢ Ⅎ 𝑦 𝐵
27 25 26 nfrabw ⊢ Ⅎ 𝑦 { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 }
28 nfsbc1v ⊢ Ⅎ 𝑦 [ 𝑣 / 𝑦 ] 𝜑
29 nfv ⊢ Ⅎ 𝑣 𝜑
30 20 27 28 29 17 cbvrexfw ⊢ ( ∃ 𝑣 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 )
31 19 30 sylib ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝜑 ) → ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 )
32 31 exp31 ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → ( 𝜑 → ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 ) ) )
33 4 5 32 rexlimd ⊢ ( 𝑥 ∈ 𝐴 → ( ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 ) )
34 33 ralimia ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 )
35 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] 𝜑
36 nfv ⊢ Ⅎ 𝑤 𝜑
37 35 36 6 cbvrexw ⊢ ( ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝜑 )
38 14 37 bitrdi ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
39 38 elrab ⊢ ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ↔ ( 𝑦 ∈ 𝐵 ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
40 39 simprbi ⊢ ( 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } → ∃ 𝑥 ∈ 𝐴 𝜑 )
41 40 rgen ⊢ ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∃ 𝑥 ∈ 𝐴 𝜑
42 41 a1i ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∃ 𝑥 ∈ 𝐴 𝜑 )
43 3 34 42 3jca ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 ∧ ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∃ 𝑥 ∈ 𝐴 𝜑 ) )
44 sseq1 ⊢ ( 𝑐 = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } → ( 𝑐 ⊆ 𝐵 ↔ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ⊆ 𝐵 ) )
45 nfcv ⊢ Ⅎ 𝑥 𝐴
46 nfsbc1v ⊢ Ⅎ 𝑥 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑
47 45 46 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑
48 nfcv ⊢ Ⅎ 𝑥 𝐵
49 47 48 nfrabw ⊢ Ⅎ 𝑥 { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 }
50 49 nfeq2 ⊢ Ⅎ 𝑥 𝑐 = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 }
51 nfcv ⊢ Ⅎ 𝑦 𝑐
52 51 27 rexeqf ⊢ ( 𝑐 = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } → ( ∃ 𝑦 ∈ 𝑐 𝜑 ↔ ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 ) )
53 50 52 ralbid ⊢ ( 𝑐 = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 ) )
54 51 27 raleqf ⊢ ( 𝑐 = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } → ( ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∃ 𝑥 ∈ 𝐴 𝜑 ) )
55 44 53 54 3anbi123d ⊢ ( 𝑐 = { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } → ( ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ↔ ( { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 ∧ ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
56 55 spcegv ⊢ ( { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∈ V → ( ( { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 ∧ ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
57 56 imp ⊢ ( ( { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∈ V ∧ ( { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } 𝜑 ∧ ∀ 𝑦 ∈ { 𝑧 ∈ 𝐵 ∣ ∃ 𝑤 ∈ 𝐴 [ 𝑤 / 𝑥 ] [ 𝑧 / 𝑦 ] 𝜑 } ∃ 𝑥 ∈ 𝐴 𝜑 ) ) → ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) )
58 1 43 57 syl2an ⊢ ( ( 𝐵 ∈ 𝑀 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑐 ( 𝑐 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑐 𝜑 ∧ ∀ 𝑦 ∈ 𝑐 ∃ 𝑥 ∈ 𝐴 𝜑 ) )